Verified Causal Broadcast with Liquid Haskell
12/10/2022
Speaker
Abstract
Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, key-value stores can use causally ordered message delivery to ensure causal consistency, and replicated data structures rely on the existence of an underlying causally-ordered messaging layer. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of the correctness of those protocols is less common, much less machine-checked proofs about executable implementations.We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell's underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store.
Bio
Lindsey Kuper is an Assistant Professor at the University of California, Santa Cruz. Her research takes a programming-languages-based approach to building provably correct and practically deployable distributed software systems. She is a co-founder of !!Con (bangbangcon.com), the conference of ten-minute talks on the joy, excitement, and surprise of computing. She is the recipient of the NSF CAREER Award (2022) and a Google Faculty Research Award (2019), and received her Ph.D. in computer science in 2015 from Indiana University.