Most databases can be configured to operate under isolation levels weaker than serializability. These enforce fewer restrictions on the concurrent access to data and consequently allow for more performant implementations. While formal frameworks for rigorously specifying isolation levels exist, reasoning about the semantic differences between specifications remains notoriously difficult. This paper proposes a tool -- Isolde -- that can automatically generate examples that are allowed by an isolation level but disallowed by another. This simple primitive unlocks a range of useful reasoning tasks, including checking equivalence between definitions, and verifying (by refutation) subtle semantic properties of isolation levels. For example, Isolde allowed us to easily and automatically reproduce a famously elusive result from the literature and to discover a previously unknown bug in the alternative specification of a standard isolation level used in a state-of-the-art isolation checker.

翻译：大多数数据库可以在比可串行化更弱的隔离级别下运行。这些隔离级别对数据的并发访问施加更少的限制，从而允许更高性能的实现。尽管存在用于严格指定隔离级别的形式化框架，但推理不同规范之间的语义差异仍然非常困难。本文提出了一种工具——Isolde——它可以自动生成由一个隔离级别允许但被另一个隔离级别禁止的示例。这一简单的原语解锁了一系列有用的推理任务，包括检查定义之间的等价性，以及通过反驳来验证隔离级别的微妙语义属性。例如，Isolde使我们能够轻松、自动地重现文献中一个著名而难以捉摸的结果，并发现最先进隔离检查器中所用标准隔离级别替代规范中一个先前未知的错误。