DistAI is a tool to automatically infer inductive invariants to prove the correctness of distributed protocols. It takes a simulation-learning-refinement workflow. Given a protocol, DistAI first repeatedly simulate the protocol using randomized instances. This gives a collection of simulation traces (i.e., samples). Then DistAI applies an enumeration-based learning procedure to find invariants that hold true on all the samples. Finally, DistAI uses Ivy, a theorem prover built on top of Z3 SMT solver, to refine the invariants using counterexamples until validated.
You can build DistAI from source using the installation guide install.txt
. Native installation gives the most accurate runtime numbers.
Alternatively, one can use our docker image with the guide docker_usage.md
. This image also includes I4 and FOL-IC3, the two systems DistAI compared with in the evaluation.
Given the name of a distributed protocol, python main.py PROTOCOL
simulates the protocol, learn the invariants and refine them. The proved protocol with correct invariants will be written to outputs/PROTOCOL/PROTOCOL_inv.ivy
python main.py two_phase_commit
In src-py/
, we can use python translate.py PROTOCOL
to generate the simulation script in Python from the Ivy source.
It accepts a conditional argument --min_size
for the minimum instance size (i.e., initial template size). If omitted, DistAI will infer the minimum size from the protocol.
python translate.py distributed_lock --min_size="node=2 epoch=2"
The simulation script is written to auto_samplers/
. From there, run python PROTOCOL.py
to simulate the protocol.
python database_chain_replication.py
The samples are written to traces/
, and a configuration file is generated in configs/
. Then, in src-c/
,
run ./main PROTOCOL [MAX_RETRY]
to learn and infer the invariants. MAX_RETRY
is a conditional argument indicating how many times the solver should retry (i.e., incrementing max-literal) before giving up.
./main blockchain 1
The proved protocol with correct inductive invariants attached is written to outputs/PROTOCOL/PROTOCOL_inv.ivy
. From there, one can use
ivy_check PROTOCOL_inv.ivy
to validate its correctness.
To use DistAI on a new distributed protocol, simply add the Ivy file at protocols/NEW_PROTOCOL/NEW_PROTOCOL.ivy
, and make an empty directory outputs/NEW_PROTOCOL/
. Then run python main.py NEW_PROTOCOL
Note that to simulate the protocol, DistAI parses the Ivy file from scratch instead of using the Ivy compiler. The parser/translator does not support full grammar of Ivy 1.7. We are working to extend it. If you have questions please let us know.
Run python tradeoff_figure.py
. The output figure is saved at tradeoff.png
-
protocols/: The 14 distributed protocols in Ivy. The mapping between protocol names in the paper and acronyms in this repository is given below.
protocol name acronym async lock server multi_lock_server chord ring maintenance chord database replication database_chain_replication decentralized lock decentralized_lock distributed lock distributed_lock hashed sharding shard leader election leader learning switch switch lock server lock_server Paxos paxos permissioned blockchain blockchain Ricart-Agrawala Ricart-Agrawala simple consensus consensus two-phase commit two_phase_commit -
src-py/: The python source codes for protocol simulation
- translate.py: parse an Ivy file and emits a Python simulation script
- translate_helper.py: provides functionality for translate.py
- ivy_parser.py: parse an Ivy expression and generates a syntax tree, used by translate.py
-
src-c/: The C++ source codes for invariant enumeration and refinement
- main.cpp: the top-level handler
- basics.h/cpp: define types and data structures (e.g., how an invariant is represented)
- preprocessing.h/cpp: reads and process the trace file and configuration file
- Solver.h/cpp: the core of DistAI. Implements template projection, invariant enumeration, and invariant projection
- InvRefiner.h/cpp: interact with Ivy to refine the invariants using counterexamples
- Helper.h/cpp: provides functionality for other files