FMitF: Track I: Vayu: Verifying Infrastructure for Safe and Performant Tunable Consistency

该项目考虑了确保在现代云平台上执行的数据库支持应用程序的安全性和正确性的新方法。 为这些环境开发的应用程序必须处理许多重要的问题，从容错到可伸缩性。 这些问题使如何推理它们的正确性变得复杂，特别是在证明它们表现出由其规范定义的期望行为方面。 在这个项目中探索的特定方向协同联合收割机的想法，从正式的方法，概率推理，和运行时系统，以减轻这个缺点，通过提供一个自动化的验证pathways.The项目的具体重点是理解的数据库状态，如分片和仲裁复制，用于提高可用性和吞吐量，对应用程序的正确性的非透明系统级实现的影响。 虽然这些方法已被证明在具有高数据量但主要是只读的工作负载中工作良好，但当应用于支持许多短期频繁更新事务的应用程序时，它们的语义变得复杂。 在这些环境中，理解该系统模型支持的弱一致分布式状态如何影响正确性是一个重要的问题。该项目有两个主要的研究方向来解决这些问题。第一个考虑使用正式的方法来描述所需的应用程序的行为。 第二种是设计概率模型来捕获平均情况下的行为，并使用这些模型来指导创建新的运行时协议，即使违反了平均情况的假设，也能保证正确的操作。 在本项目中探索的解决方案平衡了对可扩展、高吞吐量性能的需求与强大的正确性保证，从而能够在不影响性能的情况下降低应用程序开发和维护的风险、工作量和成本。 考虑到这些平台在商业、政府和学术研究和开发中的重要性，在这种环境中提供高度可靠和高效的数据库应用程序的意义是值得注意的。一个包含论文、代码、工具、数据和实验结果的项目存储库将由PI维护，网址为：http://www.cs.purdue.edu/homes/suresh/projects/vayu。 这个URL将无限期地提供，并作为正在进行的项目工作的主要来源。这个奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

This project considers new ways to ensure the safety and correctness of database-backed applications that execute on modern-day cloud platforms. Applications developed for these environments must deal with a host of important concerns, ranging from fault-tolerance to scalability. These issues complicate how to reason about their correctness, especially with respect to proving they exhibit desired behavior as defined by their specifications. The particular directions that are explored in this project synergistically combine ideas from formal methods, probabilistic reasoning, and runtime systems to alleviate this shortcoming by providing an automated verification pathway.The specific focus of the project is understanding the implications of non-opaque system-level implementations of database state such as sharding and quorum replication, used to improve availability and throughput, on application correctness. While these approaches have proven to work well in workloads that have high data volumes but are predominantly read-only, their semantics becomes complicated when applied to applications that support many short-lived frequently-updated transactions. Understanding how the weakly-consistent distributed state supported by this system model affects correctness is an important problem in these environments. The project has two main research thrusts to address these concerns. The first considers the use of formal methods to characterize desired application behavior. The second devise probabilistic models that capture average-case behavior, and uses these models to guide the creation of new runtime protocols that guarantee correct operation even when average-case assumptions are violated.There is growing interest in using cloud-based platforms for executing database-backed applications. The solutions that are explored in this project balance the need for scalable, high-throughput performance with strong correctness guarantees, thus offering the ability to lower the risk, effort and cost of application development and maintenance without compromising performance. Given the significance of these platforms in commercial, government, and academic research and development, the implications of offering highly-assured and efficient database applications in this setting are noteworthy.A project repository housing papers, code, tools, data, and experimental results will be maintained by the PIs at URL:http://www.cs.purdue.edu/homes/suresh/projects/vayu. This URL will be available indefinitely and serve as the main source for dissemination of ongoing project efforts.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.