Explicit Transaction Ordering Unlocks Polynomial-Time Serializability Verification

CV-Rules replaces the decades-old 'check for cycles in the serialization graph' with a direct construction of an explicit transaction order that satisfies two simple rules: C-rule (Causality) and V-rule (View Consistency). Classical Multi-Version Serialization Graph (MVSG) reasoning proves serializability by showing the graph is acyclic. CV-Rules instead forces the protocol to produce an explicit total order on transactions, and then checks that each read sees the right write (C-rule) and that competing writers are consistent with that order (V-rule). The paper proves all three characterizations are equivalent.

Polynomial-Time Decidability for Bounded Forced Orders

The C/V separation reveals a hidden structure: serializability is polynomial-time decidable for any fixed bound on the width of the order forced by C-rule. This is not just theory for the paper. The width bound limits how many transactions can be causally independent at any point, a property many real-world protocols naturally satisfy. The authors show that checking serializability under CV-Rules reduces to a bounded-width problem, giving a practical complexity result for the first time.

Five Protocols, All Proven in Lean

The paper verifies five protocols: Two-Phase Locking (2PL), Multi-Version Timestamp Ordering (MVTO), Serial Safety Net (SSN), Aria, and SnapChain. For SSN and Aria, whose original papers defined only certification conditions, the authors identify explicit transaction orders hiding in those mechanisms. A bonus result: Aria's unique-write constraint turns out to be unnecessary for serializability, a useful insight for implementors. SnapChain is designed directly from CV-rules, enforcing V-rule by construction. All results except the complexity bounds are mechanized in Lean with no additional axioms and no admitted goals, meaning the proofs are machine-checkable down to the Lean kernel.

SnapChain, built from the ground up using CV-rules, shows that protocol design can now target explicit orders instead of graph acyclicity, opening the door to simpler, provably correct concurrency control for databases and distributed systems.

Source: CV-Rules: Serializability Verification of Concurrency Control Protocols via Explicit Transaction Ordering
Domain: arxiv.org