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.

How to run？

1. Run separately.

Create and run TLC models in the usual way.

2. Run in batch (Recommended).

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