Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasoning about Transactional Isolation Levels with Isolde

Manuel Barros, Alcino Cunha, Jose Pereira, Eunsuk Kang

Abstract

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.

Reasoning about Transactional Isolation Levels with Isolde

Abstract

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.

Paper Structure

This paper contains 45 sections, 43 equations, 8 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Defining isolation
  3. Specifying isolation using a commit-order
  4. The Abstract Execution Paradigm
  5. ceroneFrameworkTransactionalConsistency2015
  6. crooksSeeingBelievingClientCentric2017
  7. A showcase of Isolde
  8. Verifying the equivalence of specifications
  9. Verifying Plume's alternative isolation specifications
  10. Understanding the difference between the two definitions
  11. Verifying definition equivalence across frameworks
  12. Reasoning about isolation level properties
  13. A read anomaly under snapshot isolation
  14. A note on choosing a scope
  15. Reasoning about Update Atomic
  16. ...and 30 more sections

Figures (8)

  • Figure 1: A history allowed by NLU but not by UA.
  • Figure 2: A hierarchy of five isolation levels that have been formalized in both frameworks considered.
  • Figure 3: Total instances solved within the one-hour timeout across different implementations, scopes and problem types.
  • Figure 4: Runtime performance comparison across different implementations, scopes, and problem types.
  • Figure 5: Cumulative number of benchmark instances solved as a function of the total number of CEGIS candidates evaluated, broken down by problem type (rows) and scope (columns). Each curve represents a different implementation; a point $(c, k)$ indicates that $k$ instances were solved using at most $c$ candidates.
  • ...and 3 more figures