This is the code base for the Kondo prototype, as described in the OSDI'24 paper "Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Systems Proofs".
The paper introduces the concept of an Invariant Taxonomy that factors the invariants of a distributed protocol into Protocol Invariants and Regular Invariants. Kondo is a tool that helps developers automatically generate "Regular Invariants" for their distributed protocol, and lift a simpler, synchronous proof of the protocol to the general asynchronous setting.
This artifact has two main directories.
The directory local-dafny/ contains the source code and executable for the Kondo tool. It is a fork of Dafny 4.2.0.
The core Kondo functionality is implemented in the local-dafny/Source/DafnyCore/Kondo/ sub-directory.
The directory kondoPrototypes/ contains the protocols on which Kondo is evaluated, together with the scripts for performing the evaluation.
The following instructions have been tested on an M3 MacBook Pro running MacOS Sonoma. Libraries and commands for other OS may differ.
We begin with building our local version of Dafny that contains Kondo extensions.
-
Dependencies:
- Install .NET SDK (version 6.0)
- This can be done using brew:
brew install dotnet-sdk, - Or through a manual install https://dotnet.microsoft.com/en-us/download/dotnet/6.0
- This can be done using brew:
- [python3 and pip3 are needed but they are likely already part of the Mac installation]
- Install .NET SDK (version 6.0)
-
Build Dafny. From the project root:
cd local-dafny make -
To check that Dafny runs as expected, run from the local-dafny directory:
./Scripts/dafny /compile:0 test.dfy
The expected output is
Dafny program verifier finished with 1 verified, 0 errors
Now that Dafny is set up, we check that all 10 protocols in our evaluation passes the dafny verifier.
cd kondoPrototypes/
./verify-all Note that warnings of the form Warning: /!\ No terms found to trigger on. can be ignored
This script runs the dafny verifier on each of the protocol, and takes about 5min on an M3 MacBook Pro. Note that for each protocol, there are three versions:
- Manual: This is fully manual proof of the asynchronous protocol (i.e. what a user would do without Kondo)
- Sync: This is a synchronous proof of the protocol, and serves as the input to Kondo (step 1 in Figure 6)
- Kondo: This is the Kondo-generated asynchronous protocol
Important
This step must be completed before moving on to the Detailed Instructions section, as it produces auto-generated files required to complete the evaluation.
One may also verify each version of each protocol individually, by running the verify script in the respective sub-directory for the protocol version. For instance:
./kondoPrototypes/clientServer/sync/verifyThis section involves reproducing the results published in the paper. Note that Kondo's capabilities has advanced since the original accepted manuscript, and as a result the Evaluation section in the camera-ready paper will be different from the original version. The instructions here present the expected results in the updated Evaluation, and how to reproduce them.
The main addition to Kondo is that Kondo now automatically generates a draft of the final proof (box 5 in Figure 6). As such, the user is only responsible for completing the proof of the synchronous protocol (box 5 in Figure 6).
Kondo's goal is to relieve developer effort in verifying distributed systems. To evaluate this, we apply two metrics:
- The user should be responsible for writing fewer invariants
- The user should be responible for writing fewer lines of proof code
The next two section detail how we obtain these numbers.
Claim: Users write fewer invariants when using Kondo.
To evaluate this claim, we compare the number of invariant clauses a user would have to manually derive and prove when using Kondo, compared to the baseline of not using Kondo. The table below presents the numbers.
| protocol | without Kondo | with Kondo |
|---|---|---|
| Client-Server | 5 | 1 |
| Ring Leader Election | 6 | 1 |
| Simplified Leader Election | 7 | 3 |
| Two-Phase Commit | 8 | 4 |
| Paxos | 27 | 20 |
| Flexible Paxos | 27 | 21 |
| Distributed Lock | 2 | 0 |
| ShardedKV | 2 | 0 |
| ShardedKV-Batched | 2 | 0 |
| Lock Server | 7 | 1 |
The numbers in this table are all obtained through manual inspection. To derive the "with Kondo" figures for a protocol, look at applicationProof.dfy file in the sync/ sub-directory, e.g., kondoPrototypes/paxos/sync/applicationProof.dfy. This file contains the proof of the synchronous protocol, and it's inductive invariant. The number of invariants clauses is found in the predicate ProtocolInv(c: Constants, v: Variables).
Note that each clause in ProtocolInv may count as more than one invariant, should it contain more that one sub-clause. In that case, the actual number is marked as a comment. For example, the following ProtocolInv definition would show that
// Protocol bundle: 4 clauses in total
ghost predicate ProtocolInv(c: Constants, v: Variables)
requires v.WF(c)
{
&& Invariant_A(c, v)
&& Invariant_B(c, v)
&& Invariant_C(c, v) // 2
}there are 4 clauses in total, as Invariant_C accounts for 2 of them.
To derive the "without Kondo" figures for a protocol, we look at two files:
- applicationProof.dfy file in the manual/ sub-directory, e.g., `kondoPrototypes/paxos/manual/applicationProof.dfy. This file contains a fully manual proof of the asynchronous protocol.
- messageInvariants.dfy file in the manual/ sub-directory, e.g.
kondoPrototypes/paxos/manual/messageInvariants.dfy. This file contains helper lemmas used in the final asynchronous protocol proof.
The total number of invariants clauses is found in the predicate ProtocolInv(c: Constants, v: Variables) in applicationProof.dfy, and predicate MessageInv(c: Constants, v: Variables) in messageInvariants.dfy (note that the conjunct v.WF(c) is always omitted from the count).
Claim: Users write fewer lines of proof code when using Kondo
To evaluate this claim, we compare the number of lines of proof code a user would have to manually derive and prove when using Kondo, compared to the baseline of not using Kondo. The table below presents the numbers.
| protocol | without Kondo | with Kondo | final modifications |
|---|---|---|---|
| Client-Server | 93 | 40 | 0 |
| Ring Leader Election | 191 | 63 | 0 |
| Simplified Leader Election | 136 | 94 | 0 |
| Two-Phase Commit | 184 | 133 | 19 |
| Paxos | 856 | 557 | 234 |
| Flexible Paxos | 856 | 554 | 242 |
| Distributed Lock | 64 | 31 | 0 |
| ShardedKV | 172 | 61 | 7 |
| ShardedKV-Batched | 172 | 31 | 0 |
| Lock Server | 267 | 44 | 15 |
These columns are simply a count in the number of lines of code in the respective proof files. For each protocol, "without Kondo" is the sum of source lines of code (SLOC) in the files kondoPrototypes/<protocol>/manual/messageInvariants.dfy and kondoPrototypes/<protocol>/manual/applicationProof.dfy. Meanwhile, "with Kondo" is the SLOC in the file kondoPrototypes/<protocol>/sync/applicationProof.dfy.
To obtain these numbers, run
cd kondoPrototypes/evaluation
python3 eval.pyThe output is written to the CSV file sloc.csv.
This column counts the number of lines of proof code of lemmas that the user had to modify in the final draft proof that Kondo generated. These numbers are obtained through manual inspection.
For each non-zero entry, the relevant file is kondoPrototypes/<protocol>/async-kondo/applicationProof.dfy. In this file, every modified lemma is commented with it's SLOC above its signature. E.g.,
// modified: 19 lines
lemma InvNextAC3(c: Constants, v: Variables, v': Variables)
... means that the lemma InvNextAC3 is modified (in Two-Phase Commit), and the lemma spans 19 lines. Each entry in the table is the sum of such lines in the respective proof files.