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的法定任务，反映了通过评估智力的构想，并通过评估了基金会的MERIT构成了基础的构成和广泛的构成。