Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 11:19 - 11:41 at Sala II - Concurrency Chair(s): Ori Lahav

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 bu ers, have been replaced by simple assignments, yielding a program that can be veri ed using Floyd-Hoare style Veri cation Conditions and SMT. We implement our approach as a framework for writing veri ed 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 veri cation of functional correctness simpler by reducing manually speci ed invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.

Wed 16 Jan

Displayed time zone: Belfast change

10:35 - 12:03
ConcurrencyResearch Papers at Sala II
Chair(s): Ori Lahav Tel Aviv University
10:35
22m
Talk
A True Positives Theorem for a Static Race Detector
Research Papers
Nikos Gorogiannis , Peter W. O'Hearn Facebook and University College London, Ilya Sergey Yale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
10:57
22m
Talk
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Research Papers
Roland Meyer , Sebastian Wolff TU Braunschweig
Link to publication DOI Pre-print Media Attached File Attached
11:19
22m
Talk
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Alexander Bakst , Deian Stefan University of California San Diego, Ranjit Jhala University of California, San Diego
Link to publication DOI Media Attached
11:41
22m
Talk
Weak-Consistency Specification via Visibility Relaxation
Research Papers
Michael Emmi SRI International, Constantin Enea Université Paris Diderot
Link to publication DOI Media Attached File Attached