Implementation and case studies of Disel, a separation-style logic for compositional verification of distributed systems.
- Coq 8.6 (available from https://coq.inria.fr/download)
- Mathematical Components 1.6.1 (http://math-comp.github.io/math-comp/)
If Coq is not installed such that its binaries like coqc
and
coq_makefile
are in the PATH
, then the COQBIN
environment variable
must be set to point to the directory containing such binaries. For
example:
export COQBIN=/home/user/coq/bin/
Next, run make clean; make
from the root folder. This will build all
the libraries and will check all the proofs.
-
Heaps
-- A theory of partial finite heaps; -
Core
-- Disel implementation, metatheory and inference rules (Section 3); -
Examples
-- Case studies implemented in Disel-
Calculator
-- the calculator system (Section 2); -
Greeter
-- a toy "Hello Wrold"-like protocol, where participants can only exchange greetings with each other; -
TwoPhaseCommit
-- Two Phase Commit protocol implementation (Section 4).
-
-
shims
-- DiSeL runtime system-
Note that in order to run the examples, you need OCaml installed. We tested with OCaml version 4.02.3, but others may work as well.
-
Run
make CalculatorMain.d.byte
to build the Calculator application usingextraction/calculator
as the build directory. (Note that all the proofs will be checked as well.) Then run./scripts/calculator.sh
to execute the system in three processes on the local machine. -
Run
make TPCMain.d.byte
from the root folder to build the Two-Phase Commit application. Then run./scripts/tpc.sh
to execute the system in four processes on the local machine.
-