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.
翻译:确保信息按因果顺序发送的协议是分布式系统无处不在的构件。例如,关键价值商店可以使用因果命令发送的信息以确保因果一致性,而复制的数据结构则取决于是否存在一个基本的因果命令的电文层。一个因果传送协议确保,在向一个程序发送信息时,向该程序发送的任何因果之前的电文已经发出。虽然因果传送协议被广泛使用,但核实这些协议的正确性不那么常见,而由机器核查的关于可执行执行的证明则要少得多。我们在哈斯凯尔实施了标准的因果广播协议,并使用Haskell液体溶液溶剂辅助的核查系统来表达和机械地证明,信息绝不会被发送到一个违反因果性秩序的进程中。我们使用精细的种类表达这种属性,并证明我们在执行过程中持有这种属性,利用Haskell液体作为SMT解剂的解决方案的根基,使证据部分自动化,并使用其手动的用于休息的标语特征。我们随后将经过核实的因果广播实施工作作为分布式关键价值储存的基础。