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

许多现实世界中广泛使用的Web服务，如Amazon、Facebook和其他公司构建和维护的Web服务，都将复杂的程序逻辑封装在事务中。 虽然可串行化是用来推理并发执行事务行为的黄金标准，但其执行成本导致许多商业数据库系统提供支持，并鼓励使用较弱的变体，其中事务可能会在执行时见证其他事务的影响，削弱了可串行化提供的强隔离保证。 弱隔离在提高可用性的同时使程序推理复杂化，使得验证数据库应用程序正确性或实现有用的程序转换、优化和测试/调试工具变得具有挑战性。 因此，安全和安保受到损害。 更复杂的问题是数据库和弱一致性之间的相互作用，弱一致性是底层数据存储的一个属性，它利用地理分布的镜像站点之间的复制来提高吞吐量和可用性。 毫不奇怪，弱隔离和弱一致性以微妙和不平凡的方式相互作用。 为了更好地理解这种交互，该项目开发了新的基本原则以及新的语言抽象和实现技术，这些技术对强隔离和一致性保证放松时可能出现的不同行为敏感。该项目研究了新的基础设施，用于在现代复制数据存储上验证和实施高级程序，这些数据存储仅支持副本之间的一致性和事务之间的隔离的弱执行。这项工作的结果将提高许多广泛使用的Web服务和系统的健壮性，并降低与开发和认证现代分布式数据库应用程序相关的工作、风险和成本。研究人员将让研究生和本科生参与这项研究。

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.