Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels
Modern databases embrace weak isolation levels to cater for highly available transactions. However, weak isolation bugs have recently manifested in many production databases. This raises the concern of whether database implementations actually deliver their promised isolation guarantees in practice. In this paper we present Plume, the first efficient, complete, black-box checker for weak isolation levels. Plume builds on modular, fine-grained, transactional anomalous patterns, with which we establish sound and complete characterizations of representative weak isolation levels, including read committed, read atomicity, and transactional causal consistency. Plume leverages a novel combination of two techniques, vectors and tree clocks, to accelerate isolation checking. Our extensive assessment shows that Plume can reproduce all known violations in a large collection of anomalous database execution histories, detect new isolation bugs in three production databases along with informative counterexamples, find more weak isolation anomalies than the state-of-the-art checkers, and efficiently validate isolation guarantees under a wide variety of workloads.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | Formal Methods 2OOPSLA 2024 at San Gabriel Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
16:00 20mTalk | A Constraint Solving Approach to Parikh Images of Regular Languages OOPSLA 2024 DOI | ||
16:20 20mTalk | Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing OOPSLA 2024 Wenjia Ye National University of Singapore, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
16:40 20mTalk | Inductive diagrams for causal reasoning OOPSLA 2024 Jonathan Castello University of California, Santa Cruz, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz DOI Pre-print | ||
17:00 20mTalk | Message-Observing Sessions OOPSLA 2024 DOI | ||
17:20 20mTalk | Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels OOPSLA 2024 Si Liu ETH Zurich, Long Gu State Key Laboratory for Novel Software Technology, Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, David Basin ETH Zurich DOI |