This is a formal specification of the Ceph consensus algorithm (that is based on Paxos).
The specification is based on the following source file: https://github.com/ceph/ceph/blob/master/src/mon/Paxos.cc.
The specification is written in the TLA+ language https://lamport.azurewebsites.net/tla/tla.html.
A detailed description of the model can be found at: description.md.
Results of the model can be found at: results.
An interactive explorer can be found at: animation.
Some of the useful things that can be done with this model are:
- Prove safety and liveness properties of the implemented algorithm. Test new versions of the algorithm to see if properties still hold.
- Make interactive visualizations of the algorithm and see how the variables change.
- Analyse statistics of the state machine generated from the algorithm.
- Debug the algorithm. Search behaviours that lead to certain configurations and study what can happen from there.
The specification is in the src folder and the main file is the src/ceph.tla. The file src/ceph.cfg has a description of a model with 3 monitors.
The folder src/ceph.toolbox has some default settings used by the toolbox.
-
Get tla2tools.jar from https://github.com/tlaplus/tlaplus/releases and CommunityModules.jar from https://github.com/tlaplus/CommunityModules/releases. Alternatively there is a copy of the files in the tools folder.
-
Some available tools (https://lamport.azurewebsites.net/tla/standalone-tools.html):
-
Syntax checker:
java -cp tla2tools.jar tla2sany.SANY ceph.tla -
Model checker:
java -DTLA-Library=CommunityModules.jar -cp tla2tools.jar tlc2.TLC -workers 4 ceph.tla -
Interactive TLA+ REPL (version 1.8 or above):
java -cp tla2tools.jar tlc2.REPL
Alternatively, you can use the Dockerfile to create a container with the TLA+ tools.
The container comes with alias to run the tools, respectively: tla-sany, tla-tlc, tla-trace and tla-repl.
-
Create the container:
docker build -t tla . -
Run the container and mount src folder:
docker run --rm -v $PWD/src:/src -it tla
The toolbox can be downloaded from https://github.com/tlaplus/tlaplus/releases. The main file to load in the toolbox is ceph.tla in the src folder.
Apalache is a symbolic model checker for TLA+, as an alternative to TLC. Apalache translates the specification to a set of logical constraints that are solved using Microsoft's Z3. Apalache also comes with a type checker named snowcat (https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html).
The snowcat type checker can infer and check the types of the expressions in a specification. Both the specification in apalache-version and src have type annotations that can be checked with the following command:
apalache typecheck ceph.tla
In the folder apalache-version there is a specification that was adapted to be able to run using apalache. However, in the current version, the specification takes to long to run in apalache.
To run the model checker you can use the following command:
apalache --cinit=InitConst check ceph.tla