Klaus von Gleissenthal, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, Ranjit Jhala
We present pretend synchrony, a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness.
To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT.
We have implemented our approach as a framework for writing verified distributed programs in Go.
We develop four challenging case studies — the classic two-phase commit protocol, a distributed key-value store, the Raft leader election protocol and multi-paxos — to demonstrate that pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing the manually specified invariants by a factor of 6, and faster, reducing checking time by three orders of magnitude.
VM Username: popl19
VM Password: popl19
Artifact Evaluation Download Link
Thank you for evaluating our artifact! Our artifact evaluation consists of three parts:
To evaluate the verification effort of our approach, we have manually annotated the lines of the proofs of the Two-Phase commit protocol, Raft leader election and Single-decree Paxos written in IceT and Dafny with the following categories:
Dafny proofs can be found
in ~/Desktop/popl19-artifact-evaluation/icet_vs_dafny/dafny
and IceT proofs can be found
in ~/Desktop/popl19-artifact-evaluation/icet_vs_dafny/icet.
Double clicking
~/Desktop/popl19-artifact-evaluation/icet_vs_dafny/dafny-comparison
will run the
~/Desktop/popl19-artifact-evaluation/icet_vs_dafny/print_table.py
script, which will in turn print the Table 7.1 from the paper (without
the performance metrics).
You can also measure the runtime of the annotated proofs
using briskit command.
Our Goolong library and benchmarks can be found
in ~/Desktop/popl19-artifact-evaluation/gochai/.
Running make in that folder will build the benchmarks.
To get the verification time of our benchmarks, simply double
click
the ~/Desktop/popl19-artifact-evaluation/gochai/verify-benchmarks
script. It will open a new terminal window, verify the benchmarks, and
report how much time it took from start to finish.
If you want to run the performance evaluation on our EC2 machines,
please notify us such that we can provide you the SSH keys to the
instances and the IP addresses. The SSH key will go into
the ~/Desktop/popl19-artifact-evaluation/amazon-scripts/key-pair.pem
file, with file permissions set using chmod 600
key-pair.pem. Since the IPs of the instances can change, we
will send you them as well. You will need the update the following
portion of
the ~/Desktop/popl19-artifact-evaluation/amazon-scripts/info.sh
file:
...
export IPS=( \
"ec2-18-224-190-16.us-east-2.compute.amazonaws.com" \
"ec2-18-223-143-90.us-east-2.compute.amazonaws.com" \
"ec2-13-59-150-246.us-east-2.compute.amazonaws.com" \
)
...
After these steps, you can run EPaxos, PSync and Goolong on the cloud with 3 instances.
Simply run ./multi_run.sh ./test_gochai.sh -b in the ~/Desktop/popl19-artifact-evaluation/amazon-scripts/ folder
(-b is for batched processing).
It will run the script 10 times, and report the average (in seconds).
Each run executes 5000 requests, so the throughput (req/ms) can be
calculated by the formula ((5000 / average_time) / 1000)
Simply run ./multi_run.sh ./test_epaxos.sh -b in the ~/Desktop/popl19-artifact-evaluation/amazon-scripts/ folder
(-b is for batched processing).
It will run the script 10 times, and report the average (in seconds).
Each run executes 5000 requests, so the throughput (req/ms) can be
calculated by the formula ((5000 / average_time) / 1000)
For this, you are going to need three terminals. In terminal 1
run ~/Desktop/popl19-artifact-evaluation/amazon-scripts/test_psync.sh
--test 1. Similarly, in terminals 2 and 3 run with ...
--test 2 and ... --test 3.
The output will look the following:
... stopping ... #decisions = 254000, Δt = 10137.0, throughput = 25.05672289632041 DONE !
T in ... throughtput = T in the output contains the throughput value (in reqs/ms) for a single run. The table 7.2 in the paper contains the average of running this command ten times.