Home

Awesome

CRDT-TLA

Specifying and Verifying CRDT Protocols using TLA+

Specification

Conflict-free Replicated Data Types (CRDT) are replicated data types that encapsulate the mechanisms for resolving concurrent conflicts. They guarantee strong eventual consistency among replicas in distributed systems, which requires replicas that have executed the same set of updates be in the same state. However, CRDT protocols are subtle and it is difficult to ensure their correctness.

This project leverages model checking to verify the correctness of CRDT protocols. Specifically, we propose a reusable framework for modelling 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.

Papers

See paper-crdt-TLA+.

TLA+ module description

The following figure shows the relationship between the key modules in the project:

The solid line from module A to module B indicates that A extends B,

The dashed line from module A to module B indicates that A instantiates B.

<img src="https://raw.githubusercontent.com/JYwellin/CRDT-TLA/master/fig/modules.png" width="480" height="360"/><br/>

layermodulefunction
specificationCorrectnessthe specification of SEC and EV
specificationOpCorrectnessthe specification of SEC and EV for op-based CRDT
specificationStateCorrectnessthe specification of SEC and EV for state-based CRDT
layermodulefunction
protocolOpCounterthe specification of op-based counter
protocolStateCounterthe specification of state-based counter
protocolOpAWSetthe specification of op-based AWSet
protocolStateAWSetthe specification of state-based AWSet
layermodulefunction
interfaceCRDTInterfaceprovide a unified interface for two types of CRDT
layermodulefunction
communicationSystemModelthe specification of system model
communicationBasicNetworkthe specification of basic network
communicationReliableNetworkthe specification of reliable network
communicationCausalNetworkthe specification of casual network
communicationReliableCausalNetworkthe specification of reliable causal network

How to run?

  1. Run separately.

Create and run TLC models in the usual way.

  1. Run in batch (Recommended).

We write scripts to automatically conduct a batch of experiments; seeJYwellin/crdt-experiments.