Elle: Inferring Isolation Anomalies from Experimental Observations
đź“ś Abstract
Users who care about their data store it in databases, which (at least in principle) guarantee some form of transactional isolation. However, experience shows that many databases do not provide the isolation guarantees they claim. With the recent proliferation of new distributed databases, demand has grown for checkers that can, by generating client workloads and injecting faults, produce anomalies that witness a violation of a stated guarantee. An ideal checker would be sound (no false positives), efficient (polynomial in history length and concurrency), effective (finding violations in real databases), general (analyzing many patterns of transactions), and informative (justifying the presence of an anomaly with understandable counterexamples). Sadly, we are aware of no checkers that satisfy these goals. We present Elle: a novel checker which infers an Adya-style dependency graph between client-observed transactions. It does so by carefully selecting database objects and operations when generating histories, so as to ensure that the results of database reads reveal information about their version history. Elle can detect every anomaly in Adya et al’s formalism (except for predicates), discriminate between them, and provide concise explanations of each. This paper makes the following contributions: we present Elle, demonstrate its soundness over specific datatypes, measure its efficiency against the current state of the art, and give evidence of its effectiveness via a case study of four real databases.
✨ Summary
Summary and documented influence
The paper introduces Elle, a black-box transactional-isolation checker that infers Adya-style dependency graphs from client-visible transaction histories. Its central technique is to use datatypes and operations—especially append-only lists—that make object-version histories both traceable and recoverable. This allows the checker to infer write-read, write-write, and read-write dependencies without access to a database’s internal execution history.
Elle identifies dependency-cycle anomalies such as G0, G1c, G-single, and G2, as well as aborted reads, intermediate reads, dirty updates, garbage reads, duplicate writes, and internal inconsistencies. The paper argues that the reported anomalies are sound under its observation conditions: a detected anomaly must occur in every compatible interpretation of the client observations. Its graph-based analysis is linear in history length and avoids the concurrency-driven combinatorial growth associated with general serializability and linearizability checking.
The implementation was integrated into Jepsen, where it remains available as a transactional-consistency checker for database histories and supports list-append and read/write-register analyses. (github.com) The paper’s approach has subsequently been used as a reference point for new isolation checkers. For example, later work on efficient black-box snapshot-isolation checking describes Elle as a state-of-the-art checker while addressing limitations related to its datatype and workload assumptions. (vldb.org) Research on version-certificate recovery likewise compares its approach with Elle and identifies predicate operations as an important capability not supported by Elle’s original model. (doc.ic.ac.uk) More recent work explicitly extends Elle’s unique-value assumption to transaction workloads containing duplicate values, indicating that the paper’s inference model continues to motivate research on broader black-box isolation validation. (arxiv.org) The checker has also been used in subsequent Jepsen database analyses, including transactional-isolation testing of MySQL. (jepsen.io)