Collaborative Research: FMitF: Track I: The Phlox framework for verifying a high-performance distributed database

点击翻译按钮获取中文摘要

Distributed databases, such as Google's Spanner and Amazon's DynamoDB and Redshift, are the foundation of many distributed applications and help application developers handle complex issues including concurrency, crash recovery, replication, and consistency in the face of network partitions. Building these infrastructure systems, however, is challenging and error-prone, and the cost of bugs is high. This project aims to demonstrate the feasibility of formal verification to handle sophisticated distributed databases, so as to eliminate entire classes of bugs that can lead to application errors and outages. Specifically, this project will develop a prototype distributed database called vDDB, along with a new verification framework called Phlox, which will be used to formally specify vDDB and verify its correctness. vDDB will incorporate sophisticated optimizations seen in real systems, such as multi-version concurrency control, read-set validation, leases, etc. A key challenge in verifying vDDB lies in handling many different types of non-determinism. For example, a transaction that might normally commit may be forced to abort because some server crashed, or a network outage happened, or other transactions happened to run just before it and made conflicting changes to shared data. All of these forms of non-determinism are difficult for proof developers to reason about, and a central theme in Phlox is to use a proof technique called prophecy variables, which resolves future non-determinism once upfront, instead of forcing developers to consider many possible executions as the program runs.This project has two primary related benefits. The first comes from building more reliable distributed systems. Distributed databases are the foundation of many distributed systems, helping application developers handle concurrency, availability, and fault tolerance, yet their complexity leads to subtle bugs that cause outages. Being able to formally specify and verify their correctness will improve their reliability and could avoid some of the outages that have occurred with unverified systems in the past. The second comes from educating systems engineers about the use of formal methods to specify and verify the correctness of their implementations. This project includes the development of new tutorials and lab assignments for verification of distributed systems that will be taught in classes at MIT and NYU, as well as the continued organization of the annual New England Systems Verification Day that brings together systems verification researchers and practitioners.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.