Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus von Gleissenthall (University of California)
Date: Fri, May 24, 2019
Room: 0.E220 Social Data Lab
In this talk, I will 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 have implemented our approach as a framework for writing verified distributed programs in Go. 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.
Jurriaan Hage | Security Type Error Diagnosis for Functional Languages
Next: Alex Summers | Deductive Verification for Systems Software