Ensuring Correct Distributed Writes to Delta Lake in Rust with Formal Verification
Ensuring Correct Distributed Writes to Delta Lake in Rust with Formal Verification
Databricks Data + AI Summit 2022
Rust guarantees zero memory access bug once a program compiles. However, one can still introduce logical bugs in the implementation.
In this talk, I will first give a high level overview on common formal verification methods used in distributed system designs and implementations. Then I will talk about our experiences with using TLA+ and Stateright to formally model delta-rs' multi-writer S3 backend implementation. The end result of combining both Rust and formal verification is we end up with an efficient native Delta Lake implementation that is both memory safe and logical bug free!
#AI #Data #Databricks #DeltaLake #Lakehouse #MLOps
