Alone Together: Compositional Reasoning and Inference for Weak Isolation
Alone Together: Compositional Reasoning and Inference for Weak Isolation
复制标题
DOI：
10.1145/3158115
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Jagannathan, Suresh
中科院分区：
文献类型：
--
作者：
Kaki, Gowtham;Nagar, Kartik;Jagannathan, Suresh
可串行化是一个广为人知的正确性标准，它通过确保并发事务在执行时彼此隔离，简化了对并发事务行为的推理。然而，实施可序列化隔离会带来巨大的性能成本，因为它必然会限制利用并发性的机会，即使这样的机会不会违反特定于应用程序的不变量。因此，数据库系统在实践中支持并经常鼓励开发人员使用较弱的替代方案来实现事务。这些替代方案打破了可序列化提供的强隔离保证，从而允许更大的并发性。不幸的是，弱隔离的语义没有得到很好的理解，通常只能从低级实现构件的角度进行非正式的解释。因此，在这种环境下验证高层正确性属性仍然是一个具有挑战性的问题。为了解决这个问题，我们提出了一种新的程序逻辑，它能够对并发执行的弱隔离事务的行为进行组合推理。认识到使用此逻辑所需的证明负担可能会阻止应用程序开发人员，我们还描述了一个基于此基础的推理过程，该过程确定最弱的隔离级别，该隔离级别仍然保证与此类事务相关联的高级一致性不变量的安全性。有效推理的关键是观察到弱隔离的事务可以被视为抽象数据库状态上的函数(一元)计算，允许我们将它们的操作视为数据库上的状态转换器。这种解释允许使用现成的SMT解算器进行自动验证。我们的开发是基于事务的特定隔离语义的参数化的，允许它适用于一系列弱隔离机制。在实际应用程序(用OCaml中的嵌入式DSL编写)上的案例研究和实验证明了我们方法的实用性，并提供了强有力的证据，表明弱隔离事务的自动验证可以与强隔离可序列化事务的验证放在相同的正式基础上。
Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializablity to permit greater concurrency. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem.To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency invariants associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers.Our development is parametric over a transaction's specific isolation semantics, allowing it to be applicable over a range of weak isolation mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts.