CONIX Publication

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs

Authors: Deian Stefan, Klaus von Gleissenthal, Rami Kici Gokhan, Alexander Bakst, Ranjit Jhala


We present pretend synchrony, a new approach to verifying distributed systems that is 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 by three orders of magnitude.

Release Date: 1/13/2019
Uploaded File: View