Dissertation Defense
Wolf Honoré
Title: The Atomic Distributed Object Model for Distributed System Verification
Advisor: Zhong Shao
Other committee members:
Ruzica Piskac
James Aspnes
Benjamin Pierce (University of Pennsylvania)
Abstract:
Distributed systems are at the heart of most web-based applications and are responsible for replicating and maintaining critical data. Unfortunately, their inherent concurrency combined with an asynchronous and unreliable network makes them prone to implementation bugs that can have serious real-world consequences. Formal verification can offer strong assurances of correctness; however, despite recent advances, reasoning directly about a system’s implementation remains prohibitively complex. The key is to find the right abstraction that faithfully models a system’s behaviors, while avoiding irrelevant implementation details.
This dissertation presents such an abstraction called the atomic distributed object (ADO) model, which hides the existence of the network and reduces all behaviors to three atomic operations. This not only makes the ADO model simpler, which enables more scalable verification, but it also means it is general enough to capture a wide variety of systems. We describe three verification frameworks built around the ADO model, each implemented in the Coq proof assistant and targeted at different problems. The first, Advert, supports compositional reasoning about distributed objects, which can be combined to build more complex applications. The second, Adore, proves the safety of a general class of reconfiguration schemes, which is an essential, but often overlooked, operation for practical distributed systems. Finally, AdoB shows that the ADO model can be used for liveness reasoning, and can express both benign and byzantine failure models in a unified manner.