Reasoning about Transactional Isolation Levels with Isolde
This addresses a problem for database developers and researchers by providing automated reasoning tools for isolation levels, though it is incremental as it builds on existing formal frameworks.
The paper tackles the difficulty of reasoning about semantic differences between transactional isolation levels by introducing Isolde, a tool that automatically generates examples allowed by one level but disallowed by another, enabling tasks like checking equivalence and verifying properties, such as reproducing a known result and discovering a bug in a standard isolation level specification.
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.