Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalisation instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved to verification experts and is extremely time consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a high-level programming language with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala or JavaScript). VeriFx also provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 35 CRDTs and reproduce a study on the correctness of OT functions.
翻译:分布式系统采用薄弱的一致性,以确保高可用性和低延迟性,但由于冲突而难以保证国家趋同。专家们仔细设计类似于相继数据类型并嵌入确保趋同的冲突解决机制的复制数据类型(RDTs),设计RDT具有挑战性,因为其正确性取决于细微之处,如同时操作的排序。目前,研究人员手工核查RDTs,或者通过纸质证明,或者使用证据助理进行。不幸的是,纸质证明受到推理缺陷和机械化证明的制约,核查正规化而不是现实世界的实施。此外,书面机械化证明只留给核查专家,而且极其耗时。为了简化RDTs的设计、执行和核查,我们建议VeriFx,这是具有自动验证能力的高级编程语言。VeriFx允许程序员在功能收藏时使用RDTs, 表达自动核查的正确性属性。经过验证的RDTs可以转换成主流语言(目前为Scala或JavaSript)。VS, 也提供图书馆实施和核查这些无冲突复制数据的正常性功能。