CRII: SHF: Distributed Systems With Verified Complexity By Design

Ohio University, Athens OH

Investigators

Abstract

Distributed systems, which coordinate multiple networked computers to meet a shared goal, are critical to the nation's digital infrastructure. Yet they are also notoriously difficult to get right, especially in the face of computer and network faults. Previous research efforts have used tools from formal methods, such as theorem provers, to build distributed systems with formally verified correctness guarantees. This project advances the state-of-the-art by attacking the complementary problem of formally verifying performance guarantees for a class of distributed systems representable as games: distributed routers, load balancers, and others. Such performance guarantees are useful in a wide variety of settings, from real-time systems to low-latency web applications. The project additionally supports curricular development at both the undergraduate and graduate levels, as well as activities such as the investigator's "Coq Bootcamp", a twice-weekly summer seminar on formal verification for undergraduates. The investigator's technical methodology combines tools from programming languages, such as domain-specific languages (DSLs) for correct-by-construction programming in Coq, with recent work in algorithmic game theory: Roughgarden?s smooth games and an implementation of games called multiplicative weights. By composing a DSL for smooth games with a verified implementation of multiplicative weights, this project formally bounds the time within which a smooth game converges, and the quality of the resulting state wrt. optimal. To recover guarantees against a network model that permits faults, the project uses a quantified version of the Verdi system's verified system transformers to wrap smooth games in implementations of common distributed design patterns such as sequence numbering.