← All papers
First page of CV-Rules: Serializability Verification of Concurrency Control Protocols via Explicit Transaction Ordering

CV-Rules: Serializability Verification of Concurrency Control Protocols via Explicit Transaction Ordering

Takashi Hoshino, Shigeo Mitsunari, Takashi Kambayashi, Ryoji Kurosawa, Sho Nakazono

cs.LO Jun 24, 2026 · v1 cs.DB cs.DC
Mechanizes in Lean proofs of serializability equivalences and correctness of five concurrency control protocols.
We present CV-rules, an alternative characterization of serializability in which a transaction order constructed by a protocol satisfies two per-read conditions, C-rule (Causality) and V-rule (View Consistency), that constrain the reads-from relation and competing writers. While classical Multi-Version Serialization Graph (MVSG) reasoning characterizes serializability via its acyclicity, our approach requires explicit order construction, enabling direct proofs that build on the protocol's own mechanisms. We prove that CV-rules, serializability, and MVSG acyclicity are all equivalent. Moreover, the C/V separation reveals that serializability is polynomial-time decidable for any fixed bound on the width of the order forced by C-rule. We verify five protocols: Two-Phase Locking, Multi-Version Timestamp Ordering, Serial Safety Net (SSN), Aria, and SnapChain. For SSN and Aria, whose original papers defined only certification conditions, we identify explicit transaction orders arising from their mechanisms; we also prove that Aria's unique-write constraint is unnecessary for serializability. SnapChain, in contrast, 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.

Classical MVSG reasoning characterizes serializability via acyclicity but does not directly leverage protocol mechanisms for proof construction.

CV-rules require constructing an explicit transaction order satisfying a Causality condition (C-rule) and a View Consistency condition (V-rule). The equivalence of CV-rules, serializability, and MVSG acyclicity is proved. Five protocols are verified: 2PL, MVTO, SSN, Aria, and SnapChain. All results except complexity bounds are mechanized in Lean with no axioms or admitted goals.

Aria's unique-write constraint is shown unnecessary for serializability. SnapChain is designed directly from CV-rules. The C/V separation reveals polynomial-time decidability for fixed-width C-rule orders.