Verified Causal Broadcast with Liquid Haskell
Verified Causal Broadcast with Liquid Haskell
复制标题
使用 Liquid Haskell 验证因果广播
DOI：
10.1145/3587216.3587222
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Kuper, Lindsey
中科院分区：
文献类型：
--
作者：
Redmond, Patrick;Shen, Gan;Vazou, Niki;Kuper, Lindsey
确保消息按因果顺序传递的协议是分布式系统的普遍存在的构建块。例如，分布式数据存储系统可以使用因果有序消息传递来确保因果一致性，CRDT可以依赖于底层因果有序消息传递层的存在来简化其实现。因果传递协议确保当消息被传递到进程时，发送到同一进程的任何因果在先消息已经被传递到该进程。虽然因果传递协议被广泛使用，但对其正确性的验证不太常见，我们在Haskell中实现了一个标准的因果广播协议，并使用了Liquid Haskell求解器，辅助验证系统，用于表达和机械地证明消息永远不会以违反因果关系的顺序传递到进程。我们表示此属性使用细化类型，并证明它持有我们的实现，利用液体Haskell的底层SMT求解器自动化部分证明，并使用其手动定理证明功能的休息。然后，我们将我们验证过的因果广播实现作为分布式键值存储的基础。
Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. 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 their correctness 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.
登录
查看更多内容
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Shin;Conor McBride;Stephanie Weirich
通讯作者：
Stephanie Weirich
DOI：
10.1016/0020-0190(91)90008-6
发表时间：
1991-10
期刊：
Inf. Process. Lett.
影响因子：
--
作者：
M. Raynal;A. Schiper;S. Toueg
通讯作者：
M. Raynal;A. Schiper;S. Toueg
使用 Servant 的类型级 Web API：特定领域通用编程的练习
DOI：
--
发表时间：
2015
期刊：
WGP@ICFP
影响因子：
--
作者：
Alp Mestanogullari;Sönke Hahn;Julian K. Arni;Andres Löh
通讯作者：
Andres Löh
高效广播协议在异步分布式系统中的使用
DOI：
--
发表时间：
1988
期刊：
影响因子：
--
作者：
Frank B. Schmuck
通讯作者：
Frank B. Schmuck
Agda 中的依赖类型编程
DOI：
--
发表时间：
2009
期刊：
ACM SIGPLAN International Workshop on Types In Languages Design And Implementation
影响因子：
--
作者：
U. Norell
通讯作者：
U. Norell