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

点击翻译按钮获取中文摘要

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.