Paper Info
Title
Abstraction for conflict-free replicated data types
Abstract
ABSTRACTStrong eventual consistency (SEC) has been used as a classic notion of correctness for Conflict-Free Replicated Data Types (CRDTs). However, it does not give proper abstractions of functionality, thus is not helpful for modular verification of client programs using CRDTs. We propose a new correctness formulation for CRDTs, called Abstract Converging Consistency (ACC), to specify both data consistency and functional correctness. ACC gives abstract atomic specifications (as an abstraction) to CRDT operations, and establishes consistency between the concrete execution traces and the execution using the abstract atomic operations. The abstraction allows us to verify the CRDT implementation and its client programs separately, resulting in more modular and elegant proofs than monolithic approaches for whole program verification. We give a generic proof method to verify ACC of CRDT implementations, and a rely-guarantee style program logic to verify client programs. Our Abstraction theorem shows that ACC is equivalent to contextual refinement, linking the verification of CRDT implementations and clients together to derive functional correctness of whole programs.
Year
DOI
Venue
2021
10.1145/3453483.3454067
PLDI
Keywords
DocType
Citations 
Replicated Data Types, Eventual Consistency, Contextual Refinement, Program Logic, Modular Verification
Conference
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Hongjin Liang1875.88
Xinyu Feng244330.52