Verdi: A Framework for Formally Verifying Distributed System Implementations
Implementing reliable distributed systems is challenging because they run in unreliable environments and must tolerate faults gracefully: machines may crash and networks may reorder, drop, or duplicate packets. Failing to do so can lead to catastrophic failures and major outage of web services.
We present Verdi, a framework for implementing and formally verifying practical distributed systems in Coq. Verdi formalizes five network semantics with different kinds of faults, and allows developers to choose the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling developers to construct systems from modular components. This separation of concerns eases reasoning because the developer can verify their system in an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi’s utility, we present a series of case studies including a key-value store application and a primary-backup replication mechanism.
Tue 16 JunDisplayed time zone: Tijuana, Baja California change
14:00 - 15:40
Semantics IResearch Papers at PLDI Main RED (Portland 256)
Chair(s): Hans-J. Boehm Google
|A Formal C Memory Model Supporting Integer-Pointer Casts|
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, William Mansky University of Pennsylvania, Dmitri Garbuzov University of Pennsylvania, Steve Zdancewic , Viktor Vafeiadis MPI-SWS, GermanyMedia Attached
|Defining the undefinedness of C|
Chris Hathhorn University of Missouri, Chucky Ellison University of Illinois, Grigore Roşu University of Illinois at Urbana-ChampaignMedia Attached
Daejun Park University of Illinois at Urbana-Champaign, Andrei Stefanescu University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-ChampaignMedia Attached
|Verdi: A Framework for Formally Verifying Distributed System Implementations|
James R. Wilcox University of Washington, Doug Woos University of Washington, Pavel Panchekha University of Washington, Zachary Tatlock University of Washington, Seattle, Xi Wang University of Washington, Michael D. Ernst University of Washington, Thomas Anderson University of WashingtonMedia Attached