眼见为实：基于状态的统一一致性与隔离模型

本文引入了一个一致性与隔离的统一模型，该模型最小化了这些保证的定义方式与其被感知方式之间的差距。我们的方法基于一个简单的观察：应用程序将存储系统视为通过一系列状态转换的黑盒，其中一部分状态被应用程序观察到。为了达到最大的清晰度，隔离和一致性保证应被表达为对这些状态的约束。然而，目前这些属性被表达为对应用程序不可见的操作历史的约束。我们表明，采用基于状态的方法来表达这些保证带来了几个好处。首先，它使得更容易关注给定隔离或一致性级别所允许的（并且应用程序必须处理的）异常，而不是它所禁止的异常。其次，它统一了通常各自孤立的隔离和一致性理论，并为组合这些保证提供了结构。我们利用这种模块性，将 Chockler 等人针对单操作证明的因果一致性与会话保证之间的等价性，应用于事务（独立于其执行时的隔离级别）。第三，通过剔除虚假的区别，它为日益拥挤的拟议一致性和隔离属性领域带来了清晰度：我们发现 Sovran 等人最近提出的并行快照隔离实际上是 Adya 等人提出的较早保证——惰性一致性（或 PL-2+）——的一种具体实现。