Disel - Distributed Separation Logic
Implementation and case studies of Disel, a separation-style logic for compositional verification of distributed systems.
This code accompanies the paper entitled Programming and Proving with Distributed Protocols by Ilya Sergey, James R. Wilcox, and Zachary Tatlock, in the POPL 2018 proceedings.
Building the Project
- Coq 8.7 or later
- Mathematical Components 1.6.2 or later (
- FCSL PCM library 1.0.0 or later
- OCaml 4.05.0 or later (to compile and run the extracted applications)
If Coq is not installed such that its binaries like
coq_makefile are in the
PATH, then the
COQBIN environment variable
must be set to point to the directory containing such binaries. For
To build the whole project, including examples, simply run
in the root directory of the repository. For a faster build, use
several parallel make jobs, e.g.,
make -j 4.
Installation via OPAM
The latest release of the framework components of the project may be installed into Coq's
user-contrib directory via OPAM
for easy use in other developments; this will automatically install all
Make sure OPAM is installed and use the following commands:
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-disel
As an alternative, a VM for a previous version has been provided for your convenience and is described below.
Core-- Disel implementation, metatheory and inference rules;
Examples-- Case studies implemented in Disel
Calculator-- the calculator system;
Greeter-- a toy "Hello World"-like protocol, where participants can only exchange greetings with each other;
TwoPhaseCommit-- Two Phase Commit protocol implementation;
Query-- querying protocol and its composition with Two Phase Commit via hooks;
shims-- DiSeL runtime system
Please download the virtual machine, import it into VirtualBox, and boot the machine. This VM image has been tested with VirtualBox versions 5.1.24 and 5.1.28 with Oracle VM VirtualBox Extension Pack. Versions 4.X are known not to work with this image.
If prompted for login information, both the username and password are "popl" (without quotes).
For your convenience, all necessary software, including Coq 8.6 and
ssreflect have been installed, and a checkout of Disel is present in
~/disel. Additionally, emacs and Proof General are installed so that
you can browse the sources.
We recommend checking the proofs using the provided Makefile and running the two extracted applications. Additionally, you might be interested to compare the definitions and theorems from some parts of the paper to their formalizations in Coq.
Checking the proofs can be accomplished by opening a terminal and running
cd ~/disel make clean; make -j 4
You may see lots of warnings about notations and "nothing to inject"; these are expected. Success is indicated by the build terminating without printing "error".
Extracting and running the example applications is described below.
Code corresponding to the paper
The following describes how the paper corresponds to the code:
- The Calculator (Section 2)
- The directory
Examples/Calculatorcontains the relevant files.
- The protocol is defined in
CalculatorProtocol.v, including the state space, coherence predicate, and four transitions described in Figure 2. Note that the coherence predicate is stronger than the one given in the paper: it incorporates Inv_1 from Section 2.3. This is discussed further below.
- The program that implements blocking receive of server requests from
Section 2.2 is defined in
- The simple server from Section 2.3, as well as the batching and memoizing
servers from Figure 3 are implemented in
SimpleCalculatorServers.v. They are all implemented in terms of the higher-order
server_loopfunction. The invariant Inv1 from Section 2.3 is incorporated into the protocol itself, as part of the coherence predicate.
- The simple client from Section 2.4 is implemented in
CalculatorClientLib.v. The invariant Inv2 is proved as a separate inductive invariant using the WithInv rule in
CalculatorInvariant.v. It is used to prove the clients satisfy their specifications.
- The delegating server is in
DelegatingCalculatorServer.v. It again uses the invariant Inv2.
- A runnable example using extraction to OCaml is given in
SimpleCalculatorApp.v. It consists of one client and two servers, one of which delegates to the other. Instructions for how to run the example are given below under "Extracting and Running Disel Programs".
- The directory
- The Logic and its Soundness (Section 3)
- The definitions from Figure 6 in Section 3.1 are given in
- The primitives of Disel language is defined in
Core/Actions.v(defines send/receive wrappers as in Definitions 3.2 and 3.3).
Core/HoareTriples.vdefine traces, modal predicates (
alwaysis the formalization of post-safety from Definition 3.6). Definition 3.7 from the paper corresponds to
Core/HoareTriples.v. The Theorem 3.8 follows from the soundness of the shallow embedding into Coq: any well-typed program has a specification ascribed to it.
- Inference rules are represented by lemmas named
Core/InferenceRules.v. For example,
bind_ruleis an implementation of
Bindfrom Figure 8.
- The definitions from Figure 6 in Section 3.1 are given in
- Two-Phase Commit and Querying (Section 4)
- The relevant directory is
- The protocol as described in Section 4.1 is implemented in
- The implementations of the coordinator (described in 4.2) and the participant
- The strengthened invariant from 4.3 is stated in
TwoPhaseInductiveInv.vand proved to be preserved by all transitions in
- A runnable example is in
SimpleTPCApp.v. Instructions for how to run it are given below under "Extracting and Running Disel Programs".
- The querying protocol from Section 4.4 is implemented in the directory
- The relevant directory is
We encourage you to explore Disel further by extending one of the examples or trying your own. For example, you could build an application that uses the calculator to evaluate arithmetic expressions and prove its correctness. As a more involved example, you could define a new protocol for leader election in a ring and prove that at most one node becomes leader. To get started, we recommend following the Calculator example and modifying it as necessary.
Extracting and Running Disel Programs
As described in Section 5.1, Disel programs can be extracted to OCaml and run. You can build the two examples as follows.
make CalculatorMain.d.byteto build the calculator application. The extracted code will be placed in
extraction/calculator. (Note that all the proofs will be checked as well.) Then run
~/disel/scripts/calculator.shto execute the system in three processes locally. The system will make several requests to a delegating calculator to add up some numbers. (See the definition of
Examples/Calculator/SimpleCalculatorApp.v.) A log of messages from the client perspective is printed to the console. Logs of the servers are available in the files
server1.log(the delegating server) and
server3.log(the server that actually computes).
Each log contains a debugging info about the state of each node and the messages it sends and receives. For example, the first message sent by the client is logged as
sending msg in protocol 1 with tag = 0, contents = [1; 2] to 1
Tag 0 indicates a request in the Calculator protocol. Contents
indicate the arguments to the function being calculated (in this case,
addition). The message is sent to node 1, which is the delegating server.
The client then receives a response logged as
got msg in protocol 1 with tag = 1, contents = [3; 1; 2] from 1
Tag 1 indicates a response. The contents mean that the answer to
1 + 2 is
Several more rounds of messages are exchanged. The final line summarizes the entire execution.
client got result list [([1; 2], 3); ([3; 4], 7); ([5; 6], 11); ([7; 8], 15); ([9; 10], 19)]
make TPCMain.d.bytefrom the root folder to build the Two-Phase Commit application. Then run
./scripts/tpc.shto execute the system in four processes on the local machine. The system will achieve consensus on several values. (See the definition of
Examples/TwoPhaseCommit/SimpleTPCApp.v.) Each participant votes on whether to commit the value or abort it. (See the definitions of
choice_seq3.) A log of messages from the coordinator's point of view is printed to the console. Participant logs are available in
The protocol executes a sequence of four rounds, since there are four elements in
data_seq. Each round consists of two phases. The first messages sent by the coordinator are prepare messages which request votes about the first data item. They are logged as
sending msg in protocol 0 with tag = 0, contents = [0; 1; 2] to 1 sending msg in protocol 0 with tag = 0, contents = [0; 1; 2] to 2 sending msg in protocol 0 with tag = 0, contents = [0; 1; 2] to 3
Tag 0 indicates a prepare message. The contents indicate the index of the
current request (0, since this is the first data item) and the actual data
to commit (in this case,
[1; 2], as specified in
data_seq). A separate
prepare message is sent to each participant.
The participants respond with votes, which are logged as follows
got msg in protocol 0 with tag = 1, contents =  from 1 got msg in protocol 0 with tag = 1, contents =  from 3 got msg in protocol 0 with tag = 1, contents =  from 2
Tag 1 indicates a Yes vote. The messages are ordered nondeterministically based on the operating system's and network's scheduling decisions.
Since all participants voted yes, the coordinator proceeds to commit the data by sending Commit messages (tag 3) to all participants.
sending msg in protocol 0 with tag = 3, contents =  to 1 sending msg in protocol 0 with tag = 3, contents =  to 2 sending msg in protocol 0 with tag = 3, contents =  to 3
Participants acknowledge the commit with AckCommit messages (tag 5)
got msg in protocol 0 with tag = 5, contents =  from 3 got msg in protocol 0 with tag = 5, contents =  from 1 got msg in protocol 0 with tag = 5, contents =  from 2
This completes the first round. The remaining three rounds execute similarly, based on the decisions from the choice sequences. When any participant votes no (tag 2), the coordinator instead aborts the transaction by sending Abort messages (tag 4). In that case, participants respond with AckAbort messages (tag 6). Once all four rounds are over, all nodes exit.
Proof Size Statistics
Section 5.2 and Table 1 describe the size of our development. Those
were obtained by using the
coqwc tool on manually dissected files,
according to our vision of what should count as a program, spec, or a proof.
These numbers might slightly differ from reported in the paper due to
the evolution of the project since the submission.