Mechanizing verification of transactional anomalies in weak isolation levels
Mechanizing Transactional Anomalous Patterns for Weak Isolation Levels
Databases
Summary
Databases sometimes run several operations at once, which can cause strange behaviors called anomalies. These anomalies happen when the rules that control how operations interact are weak or relaxed. The paper’s authors turned earlier theoretical descriptions of these anomalies into machine-checked proofs, confirming their accuracy and revealing some hidden issues. They fixed these problems and improved the way weak isolation rules are checked, making automated tools more reliable.
What this means in practice
- •For database system builders: Use machine-checked definitions of transactional anomalies to rigorously verify weak isolation levels in new or existing database systems.
- •For software verification teams: Improve automated tools for checking transaction consistency by incorporating refined anomaly characterizations and transaction history models.
A theory result. No direct application yet.
Authors
Long Gu, Si Liu, Hengfeng Wei
Abstract
Recently proposed transactional anomalous patterns (TAPs) provide a semantic characterization of weak isolation levels and serve as the foundation for TAP-based isolation checking. Yet, these characterizations currently exist only as pen-and-paper proofs. We present the first machine-checked formalization of TAPs and their associated weak isolation levels in Rocq. We further establish machine-checked proofs of the corresponding TAP-based characterization theorems. The mechanization process revealed two subtle issues in the original presentation: an underspecified transaction history model and an incomplete TAP characterization of the Read Atomicity isolation level that failed to capture violations of session guarantees. We address these issues by refining the definition of transaction histories and the corresponding TAP definitions, and re-establish all characterization theorems in Rocq. These refinements have further been integrated into the weak isolation checker Plume.