IronFleet: Proving Practical Distributed Systems Correct

Our next paper is "IronFleet: Proving Practical Distributed Systems Correct" by Hawblitzel, et al.

Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at fullprogram scale, much less distributed-system scale. We describe a methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification.

We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from “tested” to “correct.”

Link: https://web.eecs.umich.edu/~manosk/assets/papers/ironfleet-sosp15.pdf

Afterwards we'll head over to the Pocket Pub or Cliff's for a drink and a bite.