CCF-SHF: Small: CRONUS: High-Level Reasoning of Low-Level Isolation

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

Many real-world widely-used web services, like those built and maintained by Amazon, Facebook, and others, encapsulate complex program logic within transactions. Although serializability is the gold standard used to reason about the behavior of concurrently executing transactions, its enforcement cost has led many commercial database systems to provide support for, and encourage the use of, weaker variants, in which a transaction may witness effects from other transactions as it executes, weakening the strong isolation guarantees provided by serializability. Weak isolation, while improving availability complicates program reasoning, making it challenging to verify database application correctness, or implement useful program transformations, optimizations, and testing/debugging tools. Safety and security are thus compromised. Further complicating matters is the interplay between the database and weak consistency, a property of the underlying data store that exploits replication among geo-distributed mirrored sites to improve throughput and availability. Not surprisingly, weak isolation and weak consistency interact in subtle and non-trivial ways. To better understand this interaction, this project develops new foundational principles and new language abstractions and implementation techniques sensitive to the different behaviors possible when strong isolation and consistency guarantees are loosened. The project investigates new infrastructure for verifying and implementing high-level programs on modern replicated data stores that support only weak enforcement of consistency among replicas and isolation among transactions. Results from this effort will increase the robustness of many widely-used Web services and systems, and lower the effort, risk, and cost associated with developing and certifying modern distributed database applications. The investigators will involve graduate and undergraduate students in this research.