Specifying And Verifying Weak Consistency Protocols Using TLA+

To achieve high availability and high fault tolerance,distributed systems usually use data replication technology to store different copies of data on different physical nodes.According to the CAP theorem,no distributed systems can meet the three characteristics of(strong)consistency,availability,and partition tolerance at the same time.Therefore,distributed systems must balance availability and consistency in the presence of network partitions.Many distributed systems choose to provide weaker consistency.In this paper,we study two classic weak consistency protocols in two kinds of systems:· Strong eventual consistency protocols for Conflict-free Replicated Data Types(CRDT):CRDT are replicated data types that encapsulate the mechanisms for resolving conflicts between concurrent operations.They guarantee strong eventual consistency among replicas in distributed systems,which requires replicas that have executed the same set of updates to be in the same state.CRDT protocols are subtle and it is difficult to ensure their correctness.· Tunable consistency protocol implemented by MongoDB: MongoDB is an opensource No SQL database.It has features such as high availability,high efficiency,and high scalability.To address the consistency problem due to the data replication technology,MongoDB provides tunable consistency through different read Concern and write Concern levels.In this paper,we aim to specify and verify these two kinds of protocols,using TLA+ and TLC model checker,respectively.Specifically,we make the following contributions:· We propose a reusable framework for modeling and verifying CRDT protocols.The framework consists of four layers,i.e.,the communication layer,the interface layer,the protocol layer,and the specification layer.The communication layer models the communication among replicas and implements a variety of communication networks.The interface layer provides a uniform interface for existing CRDT protocols,including both the operation-based protocols and the state-based ones.In the protocol layer,users can choose the appropriate underlying communication network required by a specific protocol.The specification layer specifies strong eventual consistency and the eventual visibility property(i.e.,all updates are eventually delivered by all replicas)that every CRDT protocol should satisfy.We implement this framework using a formal specification language called TLA+.We also demonstrate how to model CRDT protocols in this framework and how to verify their correctness via the model checking tool called TLC,taking Add-Wins Set as an example.· We study the tunable consistency protocols in MongoDB.First,we give the pseudocode of the tunable consistency protocols with different levels of read Concern and write Concern,including the hybrid logic clock,data snapshot,client operations,server operations,log replication,heartbeat,and commit point update.Second,we formally specify the protocols in TLA+.Finally,we sort out the consistency levels that MongoDB's tunable consistency protocol satisfies under different combinations of parameters,and use TLC model checker to verify them,taking monotonic read consistency as an example.