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

合作研究：FMitF：第一轨：用于验证高性能分布式数据库的 Phlox 框架

• 批准号: 2319167
• 负责人: Nickolai Zeldovich
• 金额: $ 50万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319167&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; 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.

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