Elle: Inferring Isolation Anomalies from Experimental Observations
https://arxiv.org/abs/2003.10554
Method
"Elle infers an Adya-style dependency graph between client-observed transactions... We take the union of these dependency graphs, with each edge labeled with its dependency relationship(s), and search for cycles with particular properties"
Population
"We have implemented Elle as a checker in the open-source distributed systems testing framework Jepsen and applied it to four distributed systems, including SQL, document, and graph databases"
What it does not show
Reasons about individual objects rather than predicates, so it cannot distinguish repeatable read from serializability. Evaluated against synthetic workloads on four specific system versions in adversarial conditions, so it establishes no general false-positive or false-negative rate.
Kyle Kingsbury, Peter Alvaro
Where the previous-generation checker timed out or exhausted memory after a few hundred transactions, this approach checked histories of hundreds of thousands in tens of seconds — which is what makes the practice affordable. It revealed anomalies in every system tested.
Tier II: Methodology paper evaluated against four real shipped systems with performance and detection results. Observational under adversarial lab conditions rather than a controlled comparison.