CAREER: Distributed System Synthesis on Certified Middleware

Distributed systems are the backbone of modern computing. However, they are complicated and prone to bugs due to their combinatorially large state-spaces, and node and network failures. Recent occurrences of data, currency and service loss have shown that reliability of distributed systems remains elusive. The inherent complication is faced by not only protocol and system designers that provide interfaces but even distributed application programmers that use these interfaces. This project addresses programmer productivity and reliability of distributed systems that spans both the client applications and the supporting distributed middleware. This project includes both novel automatic synthesis techniques for client applications and novel verification techniques for distributed middleware. Distributed stores provide a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given the high-level integrity properties of the application, this project automatically decides the minimum required coordination that guarantees integrity and convergence and automatically synthesizes protocols for replicated objects. The reliability of these applications is crucially dependent on the correctness of the underlying middleware of subtle protocols such as broadcast and consensus. The middleware is classically designed as stacks of layers, and its correctness is often stated compositionally as intuitive arguments on temporal precedence of the events exchanged between each layer and its sub-layers. This project builds a development and verification framework in a proof assistant to design a mechanically verified middleware stack. The framework is based on a compositional and temporal program logic so that the proofs match the intuitive arguments. 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.