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

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

• 批准号: 2319168
• 负责人: Joseph Tassarotti
• 金额: $ 24.99万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319168&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的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。