Distributed Components
Building reliable distributed systems is challenging for many reasons. Such systems must tolerate faults gracefully: machines may crash, new nodes may suddenly join or leave the system, and the network may drop, reorder, or duplicate packets. Distributed systems are also highly concurrent; engineers must ensure that for any schedule of events, the system's key correctness guarantees are maintained and that the service remains available. Furthermore, large-scale applications are often built by composing services from multiple distributed systems, requiring developers to reason about interactions between different systems.
To help address these challenges, the Distributed Components (or "DisCo" for short) project provides reusable infrastructure for formally verifying distributed systems using the Coq proof assistant.
Jan 2018 James Wilcox will give a talk on Distributed Separation Logic (Disel) at POPL 2018.
Jan 2017 Ryan Doenges will give a talk on Verdi extensions to support churn at CoqPL 2017.
Jan 2016 James Wilcox will give a talk on our experiences verifying Raft in Verdi at CPP 2016.
Jun 2015 Doug Woos will give a talk on the design of the Verdi framework at PLDI 2015.
Ilya Sergey, James R. Wilcox, and Zachary Tatlock.
Programming and Proving with Distributed Protocols.
POPL 2018, Los Angeles, CA, January 2018.
Slides (Keynote). Slides (PDF).
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson.
Planning for Change in a Formal Verification of the Raft Consensus Protocol.
CPP 2016, St. Petersburg, FL, January 2016.
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson.
Verdi: A Framework for Implementing and Verifying Distributed Systems.
PLDI 2015, Portland, OR, June 2015.
Currently, DisCo projects include:
DisCo is an international collaboration between researchers at the Unviersity of Washington, University College London, and the University of Illinois. Many volunteers have helped out on DisCo projects; we're very grateful for their contributions! Folks currently working on DisCo include: