CAREER: Verifying Distributed System Implementations

University Of Washington, Seattle WA

Investigators

Abstract

Billions of people depend on distributed systems every day for health care, banking, transportation, and more. Despite costly testing efforts, these complex services still fail in practice, leading to data loss and major service outages that threaten everyone's convenience, finances, and safety. This project is developing the tools and techniques necessary to verify (mathematically prove) safety and reliability for distributed systems implementations under any combination of network and machine misbehaviors. The intellectual merits are to develop compositional verification techniques where the programmer can independently prove correctness for applications and reliability for fault-tolerance components. The broader significance and importance are to provide rigorous reliability guarantees for the core computational infrastructure society depends on and to train a new generation of engineers who will create high-performance, verified distributed systems implementations. This project aims to make verification tractable by developing verified system transformers which automatically wrap simple systems with fault tolerance mechanisms guaranteed to preserve equivalence. This approach separates concerns of application correctness from fault tolerance which eases proof effort and enables greater code reuse. Industrial practitioners are already using an early prototype verified system transformer as a guide in exploring designs and alternate implementations. An outcome of this project is an extensive library of such transformers covering a broad range of critical distributed system features including reconfiguration, ring maintenance, and software update. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.