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

分布式数据库，如b谷歌的Spanner和Amazon的DynamoDB和Redshift，是许多分布式应用程序的基础，并帮助应用程序开发人员处理复杂的问题，包括并发性、崩溃恢复、复制和面对网络分区时的一致性。然而，构建这些基础设施系统是具有挑战性且容易出错的，并且错误的成本很高。该项目旨在演示形式验证处理复杂分布式数据库的可行性，从而消除可能导致应用程序错误和中断的所有类型的bug。具体来说，该项目将开发一个名为vDDB的原型分布式数据库，以及一个名为Phlox的新验证框架，该框架将用于正式指定vDDB并验证其正确性。vDDB将结合实际系统中常见的复杂优化，如多版本并发控制、读集验证、租约等。验证vDDB的一个关键挑战在于处理许多不同类型的非确定性。例如，通常可能提交的事务可能会被迫中止，因为某些服务器崩溃，或者发生了网络中断，或者其他事务恰好在它之前运行，并对共享数据进行了冲突更改。所有这些形式的非确定性对于证明开发人员来说都很难进行推理，Phlox的一个中心主题是使用一种称为预言变量的证明技术，它可以预先解决未来的非确定性，而不是迫使开发人员在程序运行时考虑许多可能的执行。这个项目有两个主要的相关好处。首先是建立更可靠的分布式系统。分布式数据库是许多分布式系统的基础，它帮助应用程序开发人员处理并发性、可用性和容错性，但是它们的复杂性会导致导致中断的细微错误。能够正式指定和验证它们的正确性将提高它们的可靠性，并可以避免过去在未经验证的系统中发生的一些中断。第二是教育系统工程师如何使用形式化方法来指定和验证其实现的正确性。该项目包括开发用于验证分布式系统的新教程和实验作业，这些将在麻省理工学院和纽约大学的课堂上教授，以及继续组织一年一度的新英格兰系统验证日，将系统验证研究人员和实践者聚集在一起。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.