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

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

arxiv: 2606.25409 · v1 · pith:5BNIJJCRnew · submitted 2026-06-24 · 💻 cs.LO · cs.DB· cs.DC

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

Takashi Hoshino , Shigeo Mitsunari , Takashi Kambayashi , Ryoji Kurosawa , Sho Nakazono This is my paper

Pith reviewed 2026-06-25 20:17 UTC · model grok-4.3

classification 💻 cs.LO cs.DBcs.DC

keywords serializabilityconcurrency control protocolstransaction orderingMVSG acyclicityC-ruleV-ruleprotocol verification

0 comments

The pith

CV-rules characterize serializability by an explicit transaction order satisfying causality and view consistency.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes CV-rules as an alternative to the standard Multi-Version Serialization Graph for proving serializability. It requires constructing an explicit transaction order that meets C-rule for causality and V-rule for view consistency, constraining how reads relate to writes. This equivalence allows verifying protocols by building on their own mechanisms rather than graph checks. The authors demonstrate this for five protocols and show polynomial-time decidability when the order width is bounded. All but complexity results are mechanized in Lean.

Core claim

CV-rules, serializability, and MVSG acyclicity are equivalent, where CV-rules are satisfied by an explicit transaction order meeting C-rule (Causality) and V-rule (View Consistency) on the reads-from relation and competing writers.

What carries the argument

CV-rules: the pair of per-read conditions (Causality and View Consistency) that an explicit transaction order must satisfy to ensure serializability.

If this is right

Five protocols (Two-Phase Locking, Multi-Version Timestamp Ordering, SSN, Aria, SnapChain) are serializable because their mechanisms yield orders satisfying CV-rules.
Aria's unique-write constraint is unnecessary for serializability.
Serializability is polynomial-time decidable for fixed bounds on the width of the C-rule order.
SnapChain is designed to enforce V-rule by construction.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The approach may extend to verifying additional concurrency protocols by identifying suitable orders from their certification conditions.
Bounded-width cases suggest that many practical schedules have limited dependency width, making verification efficient.
Explicit orders could support runtime monitoring or synthesis of serializable executions in database systems.

Load-bearing premise

The certification conditions of the examined protocols suffice to exhibit explicit transaction orders satisfying both C-rule and V-rule.

What would settle it

A concrete schedule or protocol execution where an order satisfies C-rule and V-rule but the execution is not serializable, or where serializability holds without such an order.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

CV-rules give a mechanized, constructive alternative to MVSG for serializability, with explicit orders extracted for SSN and Aria plus a new protocol built from the rules.

read the letter

The paper's core move is to replace MVSG acyclicity with two per-read conditions, C-rule and V-rule, that together characterize serializability. They prove the three notions equivalent and then use the split to build explicit transaction orders directly from the mechanisms of five protocols. The Lean development covers the equivalence, the order constructions for TPL, MVTO, SSN, Aria, and SnapChain, and the removal of Aria's unique-write constraint, all with no axioms and no admitted goals. That level of formal backing is uncommon and directly addresses the usual worry that protocol-specific arguments might miss some interleaving.

What stands out is the constructive angle: instead of checking a graph after the fact, the rules let you exhibit an order that the protocol already enforces. For SSN and Aria this means turning certification conditions into concrete orders; for SnapChain the protocol is designed around V-rule from the start. The polynomial-time result for fixed C-rule width follows from the separation but sits outside the mechanized part.

The main limitation is that the complexity claim is not machine-checked, so it rests on the paper's pen-and-paper argument. Everything else that matters for the central claims is covered by the Lean proofs. The work is aimed at people who design or verify concurrency control protocols and want a method that stays close to the protocol code rather than moving entirely to graph theory. It deserves referee time because the mechanized equivalence and protocol verifications are concrete and checkable.

Referee Report

0 major / 1 minor

Summary. The paper introduces CV-rules as an alternative characterization of serializability via explicit transaction orders satisfying C-rule (Causality) and V-rule (View Consistency). It proves equivalence of CV-rules, serializability, and MVSG acyclicity. The framework is used to verify five protocols (Two-Phase Locking, Multi-Version Timestamp Ordering, SSN, Aria, SnapChain) by constructing explicit orders from their mechanisms; all equivalence and verification results (including that Aria's unique-write constraint is unnecessary) are mechanized in Lean with no axioms or admitted goals, while the polynomial-time decidability result for fixed bounded C-rule width is not mechanized.

Significance. If the results hold, the work is significant for supplying a mechanized, explicit-order approach to serializability verification that directly exploits protocol mechanisms rather than graph-based reasoning. The complete Lean development (no axioms, no admitted goals) for the equivalences and the five protocol verifications, including novel order constructions for SSN and Aria, provides high assurance and strengthens the central claims. The C/V separation additionally yields a complexity insight on bounded-width decidability.

minor comments (1)

[Abstract] Abstract: the claim that Aria's unique-write constraint is unnecessary for serializability would benefit from an explicit cross-reference to the relevant theorem or section number.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment, detailed summary of our contributions, and recommendation to accept. We are pleased that the explicit-order approach, the complete Lean mechanization (with no axioms or admitted goals), and the C/V separation were viewed as significant.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's derivation consists of proving equivalence between CV-rules, serializability, and MVSG acyclicity plus explicit transaction-order constructions for TPL, MVTO, SSN, Aria and SnapChain. All such results (except complexity bounds) are mechanized in Lean against external standard definitions of serializability and MVSG, with no axioms and no admitted goals. The mechanization directly discharges the weakest assumption by exhibiting the required orders from each protocol's mechanisms. No equations reduce results to fitted parameters, no load-bearing self-citations appear, and no ansatz or uniqueness claim is imported from prior author work. The development is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard definitions of serializability and the multi-version serialization graph from prior database literature; the CV-rules are newly defined and then proven equivalent inside the paper. No free parameters or invented entities appear.

axioms (1)

standard math Standard mathematical background for equivalence of serializability notions
Invoked in the Lean mechanization of the equivalence proofs.

pith-pipeline@v0.9.1-grok · 5771 in / 1369 out tokens · 51984 ms · 2026-06-25T20:17:25.658441+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

46 extracted references · 39 canonical work pages

[1]

Carey, and Miron Livny

Rakesh Agrawal, Michael J. Carey, and Miron Livny. Concurrency control performance modeling: alternatives and implications . ACM Trans. Database Syst. , 12(4):609--654, November 1987. https://doi.org/10.1145/32204.32220 doi:10.1145/32204.32220

work page doi:10.1145/32204.32220 1987
[2]

Reasoning about Weak Isolation Levels in Separation Logic

Anders Alnor Mathiasen, L\' e on Gondelman, L\' e on Ducruet, Amin Timany, and Lars Birkedal. Reasoning about Weak Isolation Levels in Separation Logic . Proc. ACM Program. Lang. , 9(ICFP), August 2025. https://doi.org/10.1145/3747515 doi:10.1145/3747515

work page doi:10.1145/3747515 2025
[3]

Robustness against Consistency Models with Atomic Visibility

Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility . In CONCUR , pages 7:1--7:15, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.7 doi:10.4230/LIPIcs.CONCUR.2016.7

work page doi:10.4230/lipics.concur.2016.7 2016
[4]

Bernstein and Nathan Goodman

Philip A. Bernstein and Nathan Goodman. Multiversion Concurrency Control---Theory and Algorithms . ACM Trans. Database Syst. , 8(4):465--483, December 1983. https://doi.org/10.1145/319996.319998 doi:10.1145/319996.319998

work page doi:10.1145/319996.319998 1983
[5]

Bernstein, Vassos Hadzilacos, and Nathan Goodman

Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems . Addison-Wesley Longman Publishing Co., Inc., USA, 1987

1987
[6]

On the Complexity of Checking Transactional Consistency

Ranadeep Biswas and Constantin Enea. On the Complexity of Checking Transactional Consistency . Proc. ACM Program. Lang. , 3(OOPSLA), October 2019. https://doi.org/10.1145/3360591 doi:10.1145/3360591

work page doi:10.1145/3360591 2019
[7]

A Framework for Transactional Consistency Models with Atomic Visibility

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility . In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1-4, 2015 , volume 42 of LIPIcs , pages 58--71. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2015. https://doi.org/10.4230/L...

work page doi:10.4230/lipics.concur.2015.58 2015
[8]

Analysing Snapshot Isolation

Andrea Cerone and Alexey Gotsman. Analysing Snapshot Isolation . In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing , PODC '16, pages 55--64, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2933057.2933096 doi:10.1145/2933057.2933096

work page doi:10.1145/2933057.2933096 2016
[9]

Frans Kaashoek, and Nickolai Zeldovich

Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning . In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) , pages 447--463, Carlsbad, CA, July 2022. USENIX Association

2022
[10]

Frans Kaashoek, and Nickolai Zeldovich

Yun - Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control . In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023 , pages 871--886. USENIX Associa...

2023
[11]

Serializability Preserving Extensions of Concurrency Control Protocols

Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok. Serializability Preserving Extensions of Concurrency Control Protocols . In Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings , volume 1755 of Lecture Notes in Computer Science , pages 180-...

work page doi:10.1007/3-540-46562-6 1999
[12]

Seeing is believing: A client-centric specification of database isolation

Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. Seeing is believing: A client-centric specification of database isolation. In Proceedings of the ACM Symposium on Principles of Distributed Computing , PODC '17, page 73–82, New York, NY, USA, 2017. Association for Computing Machinery. https://doi.org/10.1145/3087801.3087802 doi:10.1145/3087801.3087802

work page doi:10.1145/3087801.3087802 2017
[13]

Dilworth

Robert P. Dilworth. A Decomposition Theorem for Partially Ordered Sets . Annals of Mathematics , 51(1):161--166, 1950. https://doi.org/10.2307/1969503 doi:10.2307/1969503

work page doi:10.2307/1969503 1950
[14]

Towards Formally Specifying and Verifying Transactional Memory

Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. Towards Formally Specifying and Verifying Transactional Memory . Form. Asp. Comput. , 25(5):769–799, September 2013. https://doi.org/10.1007/s00165-012-0225-8 doi:10.1007/s00165-012-0225-8

work page doi:10.1007/s00165-012-0225-8 2013
[15]

K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. The Notions of Consistency and Predicate Locks in a Database System . Commun. ACM , 19(11):624--633, November 1976. https://doi.org/10.1145/360363.360369 doi:10.1145/360363.360369

work page doi:10.1145/360363.360369 1976
[16]

Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Luca Multazzu, and David A. Basin. VerIso: Verifiable Isolation Guarantees for Database Transactions . Proc. VLDB Endow. , 18(5):1362--1375, 2025. https://doi.org/10.14778/3718057.3718065 doi:10.14778/3718057.3718065

work page doi:10.14778/3718057.3718065 2025
[17]

IsoVista: Black-Box Checking Database Isolation Guarantees

Long Gu, Si Liu, Tiancheng Xing, Hengfeng Wei, Yuxing Chen, and David Basin. IsoVista: Black-Box Checking Database Isolation Guarantees . Proceedings of the VLDB Endowment , 17(12):4325--4328, 2024. https://doi.org/10.14778/3685800.3685866 doi:10.14778/3685800.3685866

work page doi:10.14778/3685800.3685866 2024
[18]

Lean 4 Mechanization of CV-Rules

Takashi Hoshino. Lean 4 Mechanization of CV-Rules . Zenodo, 2026. https://doi.org/10.5281/zenodo.20755695 doi:10.5281/zenodo.20755695

work page doi:10.5281/zenodo.20755695 2026
[19]

Elle: Inferring Isolation Anomalies from Experimental Observations

Kyle Kingsbury and Peter Alvaro. Elle: Inferring Isolation Anomalies from Experimental Observations . Proceedings of the VLDB Endowment , 14(3):268--280, 2020. https://doi.org/10.14778/3430915.3430918 doi:10.14778/3430915.3430918

work page doi:10.14778/3430915.3430918 2020
[20]

H. T. Kung and John T. Robinson. On Optimistic Methods for Concurrency Control . ACM Trans. Database Syst. , 6(2):213--226, June 1981. https://doi.org/10.1145/319566.319567 doi:10.1145/319566.319567

work page doi:10.1145/319566.319567 1981
[21]

A Framework for Formally Verifying Software Transactional Memory Algorithms

Mohsen Lesani, Victor Luchangco, and Mark Moir. A Framework for Formally Verifying Software Transactional Memory Algorithms . In CONCUR 2012 - Concurrency Theory - 23rd International Conference , volume 7454 of Lecture Notes in Computer Science , pages 516--530. Springer, 2012. https://doi.org/10.1007/978-3-642-32940-1\_36 doi:10.1007/978-3-642-32940-1\_36

work page doi:10.1007/978-3-642-32940-1 2012
[22]

Bell, Adam Chlipala, Benjamin C

Mohsen Lesani, Li - yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: verified transactional objects. Proc. ACM Program. Lang. , 6( OOPSLA1 ):1--31, 2022. https://doi.org/10.1145/3527324 doi:10.1145/3527324

work page doi:10.1145/3527324 2022
[23]

Andersen

Hyeontaek Lim, Michael Kaminsky, and David G. Andersen. Cicada: Dependably Fast Multi-Core In-Memory Transactions . In Proceedings of the 2017 ACM International Conference on Management of Data , SIGMOD '17, pages 21--35, New York, NY, USA, 2017. ACM. https://doi.org/10.1145/3035918.3064015 doi:10.1145/3035918.3064015

work page doi:10.1145/3035918.3064015 2017
[24]

Aria: A Fast and Practical Deterministic OLTP Database

Yi Lu, Xiangyao Yu, Lei Cao, and Samuel Madden. Aria: A Fast and Practical Deterministic OLTP Database . Proc. VLDB Endow. , 13(12):2047–2060, July 2020. https://doi.org/10.14778/3407790.3407808 doi:10.14778/3407790.3407808

work page doi:10.14778/3407790.3407808 2047
[25]

Consolidating Concurrency Control and Consensus for Commits under Conflicts

Shuai Mu, Lamont Nelson, Wyatt Lloyd, and Jinyang Li. Consolidating Concurrency Control and Consensus for Commits under Conflicts . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16) , pages 517--532, Savannah, GA, November 2016. USENIX Association

2016
[26]

NWR: Rethinking Thomas Write Rule for Omittable Write Operations , 2020

Sho Nakazono, Hiroyuki Uchiyama, Yasuhiro Fujiwara, Yasuhiro Nakamura, and Hideyuki Kawashima. NWR: Rethinking Thomas Write Rule for Omittable Write Operations , 2020. arXiv preprint . https://doi.org/10.48550/ARXIV.1904.08119 doi:10.48550/ARXIV.1904.08119

work page doi:10.48550/arxiv.1904.08119 2020
[27]

Oze: Decentralized Graph-Based Concurrency Control for Long-Running Update Transactions

Jun Nemoto, Takashi Kambayashi, Takashi Hoshino, and Hideyuki Kawashima. Oze: Decentralized Graph-Based Concurrency Control for Long-Running Update Transactions . Proc. VLDB Endow. , 18(8):2321--2333, April 2025. https://doi.org/10.14778/3742728.3742730 doi:10.14778/3742728.3742730

work page doi:10.14778/3742728.3742730 2025
[28]

Papadimitriou

Christos H. Papadimitriou. The Serializability of Concurrent Database Updates . J. ACM , 26(4):631--653, October 1979. https://doi.org/10.1145/322154.322158 doi:10.1145/322154.322158

work page doi:10.1145/322154.322158 1979
[29]

Papadimitriou and Paris C

Christos H. Papadimitriou and Paris C. Kanellakis. On Concurrency Control by Multiple Versions . ACM Trans. Database Syst. , 9(1):89--99, March 1984. https://doi.org/10.1145/348.318588 doi:10.1145/348.318588

work page doi:10.1145/348.318588 1984
[30]

2PLSF: Two-Phase Locking with Starvation-Freedom

Pedro Ramalhete, Andreia Correia, and Pascal Felber. 2PLSF: Two-Phase Locking with Starvation-Freedom . In Proceedings of the 28th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming , PPoPP '23, pages 39--51, New York, NY, USA, 2023. ACM. https://doi.org/10.1145/3572848.3577433 doi:10.1145/3572848.3577433

work page doi:10.1145/3572848.3577433 2023
[31]

D. P. Reed. Naming and Synchronization in a Decentralized Computer System . Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1978

1978
[32]

iBFS: Concurrent breadth-first search on GPUs,

Kun Ren, Jose M. Faleiro, and Daniel J. Abadi. Design Principles for Scaling Multi-core OLTP Under High Contention . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1583--1598, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882958 doi:10.1145/2882903.2882958

work page doi:10.1145/2882903.2882958 2016
[33]

o der. Ordered Sets . Birkh \

Bernd Schr \"o der. Ordered Sets . Birkh \"a user Cham, 2 edition, 2016. https://doi.org/10.1007/978-3-319-29788-0 doi:10.1007/978-3-319-29788-0

work page doi:10.1007/978-3-319-29788-0 2016
[34]

Vbox: Efficient Black-Box Serializability Verification , 2025

Weihua Sun and Zhaonian Zou. Vbox: Efficient Black-Box Serializability Verification , 2025. arXiv preprint . https://doi.org/10.48550/arXiv.2503.05163 doi:10.48550/arXiv.2503.05163

work page doi:10.48550/arxiv.2503.05163 2025
[35]

Sur l'extension de l'ordre partiel

Edward Szpilrajn. Sur l'extension de l'ordre partiel . Fundamenta Mathematicae , 16:386--389, 1930. https://doi.org/10.4064/fm-16-1-386-389 doi:10.4064/fm-16-1-386-389

work page doi:10.4064/fm-16-1-386-389 1930
[36]

Cobra: Making Transactional Key-Value Stores Verifiably Serializable

Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. Cobra: Making Transactional Key-Value Stores Verifiably Serializable . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) , pages 63--80. USENIX Association, November 2020

2020
[37]

An Analysis of Concurrency Control Protocols for In-Memory Database with CCBench

Takayuki Tanabe, Takashi Hoshino, Hideyuki Kawashima, and Osamu Tatebe. An Analysis of Concurrency Control Protocols for In-Memory Database with CCBench . Proc. VLDB Endow. , 13(13):3531--3544, 2020. https://doi.org/10.14778/3424573.3424575 doi:10.14778/3424573.3424575

work page doi:10.14778/3424573.3424575 2020
[38]

Robert H. Thomas. A Majority Consensus Approach to Concurrency Control for Multiple Copy Databases . ACM Trans. Database Syst. , 4(2):180--209, 1979. https://doi.org/10.1145/320071.320076 doi:10.1145/320071.320076

work page doi:10.1145/320071.320076 1979
[39]

Speedy Transactions in Multicore In-memory Databases

Stephen Tu, Wenting Zheng, Eddie Kohler, Barbara Liskov, and Samuel Madden. Speedy Transactions in Multicore In-memory Databases . In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles , SOSP '13, pages 18--32, New York, NY, USA, 2013. ACM. https://doi.org/10.1145/2517349.2522713 doi:10.1145/2517349.2522713

work page doi:10.1145/2517349.2522713 2013
[40]

Efficiently Making (Almost) Any Concurrency Control Mechanism Serializable

Tianzheng Wang, Ryan Johnson, Alan Fekete, and Ippokratis Pandis. Efficiently Making (Almost) Any Concurrency Control Mechanism Serializable . The VLDB Journal , 26(4):537--562, August 2017. https://doi.org/10.1007/s00778-017-0463-8 doi:10.1007/s00778-017-0463-8

work page doi:10.1007/s00778-017-0463-8 2017
[41]

TicToc: Time Traveling Optimistic Concurrency Control

Zhaoguo Wang, Shuai Mu, Yang Cui, Han Yi, Haibo Chen, and Jinyang Li. Scaling Multicore Databases via Constrained Parallel Execution . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1643--1658, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882934 doi:10.1145/2882903.2882934

work page doi:10.1145/2882903.2882934 2016
[42]

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery

Gerhard Weikum and Gottfried Vossen. Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery . Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002

2002
[43]

Data Consistency in Transactional Storage Systems: A Centralised Semantics

Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data Consistency in Transactional Storage Systems: A Centralised Semantics . In 34th European Conference on Object-Oriented Programming, ECOOP 2020, Berlin, Germany (Virtual Conference), November 15-17, 2020 , volume 166 of LIPIcs , pages 21:1--21:31. Schloss Dagstuhl - Leibniz-Zentrum f \" u ...

work page doi:10.4230/lipics.ecoop.2020.21 2020
[44]

Staring into the Abyss: An Evaluation of Concurrency Control with One Thousand Cores

Xiangyao Yu, George Bezerra, Andrew Pavlo, Srinivas Devadas, and Michael Stonebraker. Staring into the Abyss: An Evaluation of Concurrency Control with One Thousand Cores . Proc. VLDB Endow. , 8(3):209--220, November 2014. https://doi.org/10.14778/2735508.2735511 doi:10.14778/2735508.2735511

work page doi:10.14778/2735508.2735511 2014
[45]

TicToc: Time Traveling Optimistic Concurrency Control

Xiangyao Yu, Andrew Pavlo, Daniel Sanchez, and Srinivas Devadas. TicToc: Time Traveling Optimistic Concurrency Control . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1629--1642, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882935 doi:10.1145/2882903.2882935

work page doi:10.1145/2882903.2882935 2016
[46]

Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R

Irene Zhang, Naveen Kr. Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R. K. Ports. Building Consistent Transactions with Inconsistent Replication . ACM Trans. Comput. Syst. , 35(4), December 2018. https://doi.org/10.1145/3269981 doi:10.1145/3269981

work page doi:10.1145/3269981 2018

[1] [1]

Carey, and Miron Livny

Rakesh Agrawal, Michael J. Carey, and Miron Livny. Concurrency control performance modeling: alternatives and implications . ACM Trans. Database Syst. , 12(4):609--654, November 1987. https://doi.org/10.1145/32204.32220 doi:10.1145/32204.32220

work page doi:10.1145/32204.32220 1987

[2] [2]

Reasoning about Weak Isolation Levels in Separation Logic

Anders Alnor Mathiasen, L\' e on Gondelman, L\' e on Ducruet, Amin Timany, and Lars Birkedal. Reasoning about Weak Isolation Levels in Separation Logic . Proc. ACM Program. Lang. , 9(ICFP), August 2025. https://doi.org/10.1145/3747515 doi:10.1145/3747515

work page doi:10.1145/3747515 2025

[3] [3]

Robustness against Consistency Models with Atomic Visibility

Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility . In CONCUR , pages 7:1--7:15, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.7 doi:10.4230/LIPIcs.CONCUR.2016.7

work page doi:10.4230/lipics.concur.2016.7 2016

[4] [4]

Bernstein and Nathan Goodman

Philip A. Bernstein and Nathan Goodman. Multiversion Concurrency Control---Theory and Algorithms . ACM Trans. Database Syst. , 8(4):465--483, December 1983. https://doi.org/10.1145/319996.319998 doi:10.1145/319996.319998

work page doi:10.1145/319996.319998 1983

[5] [5]

Bernstein, Vassos Hadzilacos, and Nathan Goodman

Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems . Addison-Wesley Longman Publishing Co., Inc., USA, 1987

1987

[6] [6]

On the Complexity of Checking Transactional Consistency

Ranadeep Biswas and Constantin Enea. On the Complexity of Checking Transactional Consistency . Proc. ACM Program. Lang. , 3(OOPSLA), October 2019. https://doi.org/10.1145/3360591 doi:10.1145/3360591

work page doi:10.1145/3360591 2019

[7] [7]

A Framework for Transactional Consistency Models with Atomic Visibility

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility . In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1-4, 2015 , volume 42 of LIPIcs , pages 58--71. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2015. https://doi.org/10.4230/L...

work page doi:10.4230/lipics.concur.2015.58 2015

[8] [8]

Analysing Snapshot Isolation

Andrea Cerone and Alexey Gotsman. Analysing Snapshot Isolation . In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing , PODC '16, pages 55--64, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2933057.2933096 doi:10.1145/2933057.2933096

work page doi:10.1145/2933057.2933096 2016

[9] [9]

Frans Kaashoek, and Nickolai Zeldovich

Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning . In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) , pages 447--463, Carlsbad, CA, July 2022. USENIX Association

2022

[10] [10]

Frans Kaashoek, and Nickolai Zeldovich

Yun - Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control . In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023 , pages 871--886. USENIX Associa...

2023

[11] [11]

Serializability Preserving Extensions of Concurrency Control Protocols

Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok. Serializability Preserving Extensions of Concurrency Control Protocols . In Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings , volume 1755 of Lecture Notes in Computer Science , pages 180-...

work page doi:10.1007/3-540-46562-6 1999

[12] [12]

Seeing is believing: A client-centric specification of database isolation

Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. Seeing is believing: A client-centric specification of database isolation. In Proceedings of the ACM Symposium on Principles of Distributed Computing , PODC '17, page 73–82, New York, NY, USA, 2017. Association for Computing Machinery. https://doi.org/10.1145/3087801.3087802 doi:10.1145/3087801.3087802

work page doi:10.1145/3087801.3087802 2017

[13] [13]

Dilworth

Robert P. Dilworth. A Decomposition Theorem for Partially Ordered Sets . Annals of Mathematics , 51(1):161--166, 1950. https://doi.org/10.2307/1969503 doi:10.2307/1969503

work page doi:10.2307/1969503 1950

[14] [14]

Towards Formally Specifying and Verifying Transactional Memory

Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. Towards Formally Specifying and Verifying Transactional Memory . Form. Asp. Comput. , 25(5):769–799, September 2013. https://doi.org/10.1007/s00165-012-0225-8 doi:10.1007/s00165-012-0225-8

work page doi:10.1007/s00165-012-0225-8 2013

[15] [15]

K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. The Notions of Consistency and Predicate Locks in a Database System . Commun. ACM , 19(11):624--633, November 1976. https://doi.org/10.1145/360363.360369 doi:10.1145/360363.360369

work page doi:10.1145/360363.360369 1976

[16] [16]

Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Luca Multazzu, and David A. Basin. VerIso: Verifiable Isolation Guarantees for Database Transactions . Proc. VLDB Endow. , 18(5):1362--1375, 2025. https://doi.org/10.14778/3718057.3718065 doi:10.14778/3718057.3718065

work page doi:10.14778/3718057.3718065 2025

[17] [17]

IsoVista: Black-Box Checking Database Isolation Guarantees

Long Gu, Si Liu, Tiancheng Xing, Hengfeng Wei, Yuxing Chen, and David Basin. IsoVista: Black-Box Checking Database Isolation Guarantees . Proceedings of the VLDB Endowment , 17(12):4325--4328, 2024. https://doi.org/10.14778/3685800.3685866 doi:10.14778/3685800.3685866

work page doi:10.14778/3685800.3685866 2024

[18] [18]

Lean 4 Mechanization of CV-Rules

Takashi Hoshino. Lean 4 Mechanization of CV-Rules . Zenodo, 2026. https://doi.org/10.5281/zenodo.20755695 doi:10.5281/zenodo.20755695

work page doi:10.5281/zenodo.20755695 2026

[19] [19]

Elle: Inferring Isolation Anomalies from Experimental Observations

Kyle Kingsbury and Peter Alvaro. Elle: Inferring Isolation Anomalies from Experimental Observations . Proceedings of the VLDB Endowment , 14(3):268--280, 2020. https://doi.org/10.14778/3430915.3430918 doi:10.14778/3430915.3430918

work page doi:10.14778/3430915.3430918 2020

[20] [20]

H. T. Kung and John T. Robinson. On Optimistic Methods for Concurrency Control . ACM Trans. Database Syst. , 6(2):213--226, June 1981. https://doi.org/10.1145/319566.319567 doi:10.1145/319566.319567

work page doi:10.1145/319566.319567 1981

[21] [21]

A Framework for Formally Verifying Software Transactional Memory Algorithms

Mohsen Lesani, Victor Luchangco, and Mark Moir. A Framework for Formally Verifying Software Transactional Memory Algorithms . In CONCUR 2012 - Concurrency Theory - 23rd International Conference , volume 7454 of Lecture Notes in Computer Science , pages 516--530. Springer, 2012. https://doi.org/10.1007/978-3-642-32940-1\_36 doi:10.1007/978-3-642-32940-1\_36

work page doi:10.1007/978-3-642-32940-1 2012

[22] [22]

Bell, Adam Chlipala, Benjamin C

Mohsen Lesani, Li - yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: verified transactional objects. Proc. ACM Program. Lang. , 6( OOPSLA1 ):1--31, 2022. https://doi.org/10.1145/3527324 doi:10.1145/3527324

work page doi:10.1145/3527324 2022

[23] [23]

Andersen

Hyeontaek Lim, Michael Kaminsky, and David G. Andersen. Cicada: Dependably Fast Multi-Core In-Memory Transactions . In Proceedings of the 2017 ACM International Conference on Management of Data , SIGMOD '17, pages 21--35, New York, NY, USA, 2017. ACM. https://doi.org/10.1145/3035918.3064015 doi:10.1145/3035918.3064015

work page doi:10.1145/3035918.3064015 2017

[24] [24]

Aria: A Fast and Practical Deterministic OLTP Database

Yi Lu, Xiangyao Yu, Lei Cao, and Samuel Madden. Aria: A Fast and Practical Deterministic OLTP Database . Proc. VLDB Endow. , 13(12):2047–2060, July 2020. https://doi.org/10.14778/3407790.3407808 doi:10.14778/3407790.3407808

work page doi:10.14778/3407790.3407808 2047

[25] [25]

Consolidating Concurrency Control and Consensus for Commits under Conflicts

Shuai Mu, Lamont Nelson, Wyatt Lloyd, and Jinyang Li. Consolidating Concurrency Control and Consensus for Commits under Conflicts . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16) , pages 517--532, Savannah, GA, November 2016. USENIX Association

2016

[26] [26]

NWR: Rethinking Thomas Write Rule for Omittable Write Operations , 2020

Sho Nakazono, Hiroyuki Uchiyama, Yasuhiro Fujiwara, Yasuhiro Nakamura, and Hideyuki Kawashima. NWR: Rethinking Thomas Write Rule for Omittable Write Operations , 2020. arXiv preprint . https://doi.org/10.48550/ARXIV.1904.08119 doi:10.48550/ARXIV.1904.08119

work page doi:10.48550/arxiv.1904.08119 2020

[27] [27]

Oze: Decentralized Graph-Based Concurrency Control for Long-Running Update Transactions

Jun Nemoto, Takashi Kambayashi, Takashi Hoshino, and Hideyuki Kawashima. Oze: Decentralized Graph-Based Concurrency Control for Long-Running Update Transactions . Proc. VLDB Endow. , 18(8):2321--2333, April 2025. https://doi.org/10.14778/3742728.3742730 doi:10.14778/3742728.3742730

work page doi:10.14778/3742728.3742730 2025

[28] [28]

Papadimitriou

Christos H. Papadimitriou. The Serializability of Concurrent Database Updates . J. ACM , 26(4):631--653, October 1979. https://doi.org/10.1145/322154.322158 doi:10.1145/322154.322158

work page doi:10.1145/322154.322158 1979

[29] [29]

Papadimitriou and Paris C

Christos H. Papadimitriou and Paris C. Kanellakis. On Concurrency Control by Multiple Versions . ACM Trans. Database Syst. , 9(1):89--99, March 1984. https://doi.org/10.1145/348.318588 doi:10.1145/348.318588

work page doi:10.1145/348.318588 1984

[30] [30]

2PLSF: Two-Phase Locking with Starvation-Freedom

Pedro Ramalhete, Andreia Correia, and Pascal Felber. 2PLSF: Two-Phase Locking with Starvation-Freedom . In Proceedings of the 28th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming , PPoPP '23, pages 39--51, New York, NY, USA, 2023. ACM. https://doi.org/10.1145/3572848.3577433 doi:10.1145/3572848.3577433

work page doi:10.1145/3572848.3577433 2023

[31] [31]

D. P. Reed. Naming and Synchronization in a Decentralized Computer System . Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1978

1978

[32] [32]

iBFS: Concurrent breadth-first search on GPUs,

Kun Ren, Jose M. Faleiro, and Daniel J. Abadi. Design Principles for Scaling Multi-core OLTP Under High Contention . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1583--1598, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882958 doi:10.1145/2882903.2882958

work page doi:10.1145/2882903.2882958 2016

[33] [33]

o der. Ordered Sets . Birkh \

Bernd Schr \"o der. Ordered Sets . Birkh \"a user Cham, 2 edition, 2016. https://doi.org/10.1007/978-3-319-29788-0 doi:10.1007/978-3-319-29788-0

work page doi:10.1007/978-3-319-29788-0 2016

[34] [34]

Vbox: Efficient Black-Box Serializability Verification , 2025

Weihua Sun and Zhaonian Zou. Vbox: Efficient Black-Box Serializability Verification , 2025. arXiv preprint . https://doi.org/10.48550/arXiv.2503.05163 doi:10.48550/arXiv.2503.05163

work page doi:10.48550/arxiv.2503.05163 2025

[35] [35]

Sur l'extension de l'ordre partiel

Edward Szpilrajn. Sur l'extension de l'ordre partiel . Fundamenta Mathematicae , 16:386--389, 1930. https://doi.org/10.4064/fm-16-1-386-389 doi:10.4064/fm-16-1-386-389

work page doi:10.4064/fm-16-1-386-389 1930

[36] [36]

Cobra: Making Transactional Key-Value Stores Verifiably Serializable

Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. Cobra: Making Transactional Key-Value Stores Verifiably Serializable . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) , pages 63--80. USENIX Association, November 2020

2020

[37] [37]

An Analysis of Concurrency Control Protocols for In-Memory Database with CCBench

Takayuki Tanabe, Takashi Hoshino, Hideyuki Kawashima, and Osamu Tatebe. An Analysis of Concurrency Control Protocols for In-Memory Database with CCBench . Proc. VLDB Endow. , 13(13):3531--3544, 2020. https://doi.org/10.14778/3424573.3424575 doi:10.14778/3424573.3424575

work page doi:10.14778/3424573.3424575 2020

[38] [38]

Robert H. Thomas. A Majority Consensus Approach to Concurrency Control for Multiple Copy Databases . ACM Trans. Database Syst. , 4(2):180--209, 1979. https://doi.org/10.1145/320071.320076 doi:10.1145/320071.320076

work page doi:10.1145/320071.320076 1979

[39] [39]

Speedy Transactions in Multicore In-memory Databases

Stephen Tu, Wenting Zheng, Eddie Kohler, Barbara Liskov, and Samuel Madden. Speedy Transactions in Multicore In-memory Databases . In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles , SOSP '13, pages 18--32, New York, NY, USA, 2013. ACM. https://doi.org/10.1145/2517349.2522713 doi:10.1145/2517349.2522713

work page doi:10.1145/2517349.2522713 2013

[40] [40]

Efficiently Making (Almost) Any Concurrency Control Mechanism Serializable

Tianzheng Wang, Ryan Johnson, Alan Fekete, and Ippokratis Pandis. Efficiently Making (Almost) Any Concurrency Control Mechanism Serializable . The VLDB Journal , 26(4):537--562, August 2017. https://doi.org/10.1007/s00778-017-0463-8 doi:10.1007/s00778-017-0463-8

work page doi:10.1007/s00778-017-0463-8 2017

[41] [41]

TicToc: Time Traveling Optimistic Concurrency Control

Zhaoguo Wang, Shuai Mu, Yang Cui, Han Yi, Haibo Chen, and Jinyang Li. Scaling Multicore Databases via Constrained Parallel Execution . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1643--1658, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882934 doi:10.1145/2882903.2882934

work page doi:10.1145/2882903.2882934 2016

[42] [42]

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery

Gerhard Weikum and Gottfried Vossen. Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery . Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002

2002

[43] [43]

Data Consistency in Transactional Storage Systems: A Centralised Semantics

Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data Consistency in Transactional Storage Systems: A Centralised Semantics . In 34th European Conference on Object-Oriented Programming, ECOOP 2020, Berlin, Germany (Virtual Conference), November 15-17, 2020 , volume 166 of LIPIcs , pages 21:1--21:31. Schloss Dagstuhl - Leibniz-Zentrum f \" u ...

work page doi:10.4230/lipics.ecoop.2020.21 2020

[44] [44]

Staring into the Abyss: An Evaluation of Concurrency Control with One Thousand Cores

Xiangyao Yu, George Bezerra, Andrew Pavlo, Srinivas Devadas, and Michael Stonebraker. Staring into the Abyss: An Evaluation of Concurrency Control with One Thousand Cores . Proc. VLDB Endow. , 8(3):209--220, November 2014. https://doi.org/10.14778/2735508.2735511 doi:10.14778/2735508.2735511

work page doi:10.14778/2735508.2735511 2014

[45] [45]

TicToc: Time Traveling Optimistic Concurrency Control

Xiangyao Yu, Andrew Pavlo, Daniel Sanchez, and Srinivas Devadas. TicToc: Time Traveling Optimistic Concurrency Control . In Proceedings of the 2016 International Conference on Management of Data , SIGMOD '16, pages 1629--1642, New York, NY, USA, 2016. ACM. https://doi.org/10.1145/2882903.2882935 doi:10.1145/2882903.2882935

work page doi:10.1145/2882903.2882935 2016

[46] [46]

Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R

Irene Zhang, Naveen Kr. Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R. K. Ports. Building Consistent Transactions with Inconsistent Replication . ACM Trans. Comput. Syst. , 35(4), December 2018. https://doi.org/10.1145/3269981 doi:10.1145/3269981

work page doi:10.1145/3269981 2018