Pretend synchrony: synchronous verification of asynchronous distributed programs

Klaus von Gleissenthal, Rami Gökhan Klcl, Alexander Bakst, Deian Stefan, Ranjit Jhala

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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 message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT. We implement our approach as a framework for writing verified distributed programs in Go and evaluate it with four challenging case studies— the classic two-phase commit protocol, the Raft leader election protocol, single-decree Paxos protocol, and a Multi-Paxos based distributed key-value store. We find that pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing manually specified invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.
Original languageEnglish
Article number59
Pages (from-to)1-30
Number of pages30
JournalProceedings of the ACM on Programming Languages
Volume3
Issue numberPOPL
Early online date2 Jan 2019
DOIs
Publication statusPublished - Jan 2019

Fingerprint

Dive into the research topics of 'Pretend synchrony: synchronous verification of asynchronous distributed programs'. Together they form a unique fingerprint.

Cite this