Pith. sign in

REVIEW 2 major objections 5 minor 62 references

Verifying Isolation Levels of Database Implementations for Free Using Separation Logic

T0 review · 2 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read For three weak isolation levels, any database implementation that satisfies a given set of separation-logic per-operation specifications automatically implements that isolation level, for every possible client, with a machine-checked proof.

desk verdict Genuinely new free theorem connecting separation-logic specs to a Crooks-style consistency model, but the paper owes the reader a proof that its amended model is still equivalent to the dependency-graph model. read the letter →

arxiv 2607.15877 v1 pith:7NR6CDQZ submitted 2026-07-17 cs.DB

Anders Alnor Mathiasen , Amin Timany , Lars Birkedal This is my paper · ORCID
classification cs.DB MSC 68Q6068P15
keywords isolationlevelsseparationlogicfreetheoremtransactionalconsistencystate-basedmodelghostcodelinearizabilityformalverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper's central thesis is that isolation-level correctness can be read off the structure of separation-logic specifications: verify the individual database operations against the appropriate Hoare-style specification, and the database automatically satisfies the corresponding isolation level in a state-based transactional consistency model. The proof works for read uncommitted, read committed, and snapshot isolation, covers arbitrary client programs and arbitrary transaction workloads, and is fully machine-checked. The mechanism is a trace-based extraction: operations are instrumented with ghost code that records start and end events, linearization points are inserted logically, operations are grouped into transactions, and an invariant guarantees those transactions admit an execution passing the isolation level's commit test. The result is a free theorem, meaning the model-level guarantee needs no additional proof for each concrete database implementation once its operations meet the specifications.

What carries the argument

The load-bearing mechanism is a four-level trace extraction. Level 0 is instrumented executable code; ghost operations emit pre and post events into a global trace with fresh tags (level 1). From that trace, a sequence of linearization points is constructed (level 2), constrained to be coherent with the trace in the standard linearizability sense. The linearization points are chopped into transactions per connection (level 3), requiring each transaction to read its own most recent write, have ordered operations, and end with a single commit. At the top, the transactions must admit an execution of the state-based model whose commit test holds. The global proof invariant ValidTrace(I,t) packag

What would settle it

One disqualifying observation would be a database implementation that provably satisfies the snapshot-isolation separation-logic specification yet has a committed execution whose transactions cannot be ordered into any state-based execution satisfying the snapshot-isolation commit test. A second would be an execution accepted by the amended state-based commit test but rejected by the dependency-graph definition of the same isolation level, which would refute the claimed equivalence between the two models.

Watch

Extended reading notes

Core claim

The paper proves an adequacy theorem: for an isolation level I with its separation-logic specification specI, any implementation libI satisfying specI, wrapped with the ghost instrumentation, produces only valid traces under arbitrary verified clients, and no thread crashes. A valid trace is one for which a sequence of linearization points, a set of transactions, and a state-based execution exist such that the isolation level's commit test holds for all committed transactions. This is exactly implementation correctness in the state-based consistency model, and, via the model's established equivalence, in the dependency-graph formulation used by the database community. The proof is uniform: i

Load-bearing premise

The result inherits correctness of the separation-logic specifications: if those specifications permit a behavior that violates the intended isolation guarantee, the free theorem still holds formally but offers no real guarantee.

Editorial extensions

If this is right

  • Verifying a database's isolation level reduces to proving per-operation separation-logic specifications; the consistency-model guarantee follows automatically for all possible client programs.
  • The guarantee holds for every transaction workload, not just a fixed workload, so it is strictly stronger than model-checking approaches that enumerate interleavings.
  • The result is a free theorem: new database implementations acquire the model-level guarantee without re-proving the connection, as long as they satisfy the specifications.
  • Clients can be verified against the same modular per-operation specifications, so correctness composes with other libraries and verified components.
  • Because the proof is machine-checked, the link between executable code and the isolation-level model is mechanized end to end.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the same extraction pipeline should extend to stronger and additional isolation levels (such as serializability or parallel snapshot isolation) once separation-logic specifications exist; the main friction is designing the per-level commit test and the corresponding resource wrapping, not the trace machinery.
  • Editorial inference: the method's practical power depends on the cost of proving the underlying per-operation specifications for a real database; for high-performance engines this is a substantial verification effort, though it is paid once per implementation rather than per workload.
  • Editorial inference: a testable extension would be to instantiate the pipeline for a small distributed database and show that the extracted transactions satisfy the commit test on all interleavings, providing a concrete end-to-end case against which this paper's machinery can be checked.
  • Editorial inference: because the equivalence between the amended state-based model and the dependency-graph model is cited rather than proven in this paper, a rigorous independent check of that equivalence for the modified NoConf test would close the only remaining semantic gap.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper presents a method for proving that any database implementation satisfying the separation-logic specifications of Alnor Mathiasen et al. [3] implements the corresponding isolation level in the state-based model of Crooks et al. [16]. The method instruments database operations with ghost pre/post events, enforces a global trace invariant ValidTrace(I,t), extracts linearization points and transactions, and proves a free theorem (Theorem 5.1): for any verified clients, all reachable traces satisfy the commit test of I. Proofs are mechanized in Rocq/Iris/Aneris (13,000+ lines). The paper covers read uncommitted, read committed, and snapshot isolation, with a detailed proof sketch for snapshot isolation.

Significance. If the central claims hold, this is a significant step: it avoids workload-specific model checking and gives a modular, machine-checked bridge from executable code to abstract consistency models. The paper is commendable for shipping a large Rocq formalization and for stating the theorem parametrically in the prior specifications, making the result a genuine free theorem. However, the significance depends on the amended Section 3 model preserving the Crooks--Adya equivalence; this is currently asserted rather than proved.

major comments (2)
  1. [§3, Definition 3.3 and Figure 5] The amended NoConf leaves the snapshot index i unconstrained for blind writes. A transaction T with no NoPriorWrite read of k may set i = j-1, so an execution [T1={W(k,1),C} at index 1, T2={W(k,2),C} at index 2] is accepted. If T1 and T2 overlap in the source execution, Adya's write-write conflict rule forbids both commits. The paper cites Crooks et al. [16] for equivalence but explicitly states that this model has been amended (removed unique-value and one-write-per-key assumptions, changed NoConf). No proof is supplied that the amended model remains equivalent to the dependency-graph model. This is load-bearing: Theorem 5.1 is stated for the amended model and the intro/conclusion claim Adya as the endpoint. Please either prove the equivalence for the amended model or scope the claims to the amended model and state which standard guarantees are lost.
  2. [Theorem 5.1 / §4–§5] The Adequacy theorem inherits the separation-logic specifications specI from the authors' own prior work [3]. ValidTrace(I,t) establishes the amended state-based commit test, but nothing in the paper proves that specI captures the intended isolation level beyond the write-skew example in Section A. Since the headline claim is that isolation levels are derived from the structure of specifications, an explicit statement that the result is only as strong as specI -- together with a summary of the phenomena checked for each level in [3] -- would make the dependency visible. This is a premise concern, not an internal inconsistency, but it is central to the advertised guarantee.
minor comments (5)
  1. [§3, Figure 5] CT_SI(T,E) is written with NoConf(E,T,s), while Definition 3.3 defines NoConf(E,T,i). The third argument should be an index, not a state; the notation should be made consistent.
  2. [§5.3, Figure 13] The second transaction's read is rendered as R((τ2,c2),y,x0); from the trace in Figure 9 it should be y,y0.
  3. [§3, §5.4] Definition 3.5 and the text around it refer to 'Theorem 3.5'; it is a definition. Similarly, the commit tests in Figure 5 are called 'Theorem 3.3/3.4' but are definitions.
  4. [§5, The Global Proof Invariant] The same symbol t is used for the event trace and for the linearization-point sequence. This is easy to confuse; distinct symbols (e.g., t and ℓ) would improve readability.
  5. [Mechanization] The paper claims that all proofs are mechanized but gives no artifact description (location of the Rocq development, key theorem names). A short reproducibility note would help readers and reviewers.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the free theorem is an explicit conditional whose premise (specI) is machine-checked prior work; the proof connects two distinct formalisms rather than reducing to its input.

full rationale

The derivation chain is: assume specI(lib) from Alnor Mathiasen et al. [3]; prove specI(Wrap(lib)) by instantiating the existentially quantified resources and maintaining the trace invariant; conclude ValidTrace(I,t) via the adequacy theorem. The conclusion contains the state-based commit test (Complete/NoConf, Preread, or True), which is not identical to the input separation-logic specification. The input is a set of per-operation atomic Hoare triples with CanCommit; the output is an existential execution E satisfying the commit test. To get from one to the other the proof must construct linearization points, group them into transactions, build an execution, and show coherence at every level. That is a substantive translation, not a re-definition. The reliance on [3] is an explicit premise, and the paper states that the specifications from [3] are machine-checked; under the review rules, machine-checked prior work counts as independent support and does not make the conditional circular. The amended state-based model and the citation of Crooks et al. [16] for equivalence to the dependency-graph model is a correctness/verification gap (the amended NoConf is not re-proven equivalent), but a missing external equivalence proof is not internal circularity: the Adya target is not encoded into the separation-logic specifications by construction. There are no fitted parameters, no prediction of a fitted quantity, and no uniqueness theorem imported from the same authors. Accordingly, the paper receives score 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

No numerical free parameters are fitted: this is a formal proof, not an empirical study. The introduced ghost trace and permission machinery are proof artifacts with no runtime or physical counterpart; their soundness is delegated to the Iris/Aneris background. The central unproven premise is that the separation-logic specifications from [3] are the right characterization of the isolation levels, plus the unproven equivalence of the amended state-based model to the dependency-graph model.

assumptions (5)
  • domain assumption specI from Alnor Mathiasen et al. [3] correctly characterizes weak isolation levels at the program-execution level.
    Theorem 5.1 takes specI as the only precondition about the implementation; the paper does not prove the specifications themselves match intended isolation semantics.
  • domain assumption The state-based model of Crooks et al. [16] is equivalent to the Adya dependency-graph model, including the amended snapshot-isolation commit test.
    Used to claim the dependency-graph result; the paper cites [16] but does not prove equivalence after the amendment in Section 3.
  • standard math Soundness of Iris/Aneris and of the fresh/emit ghost-code operational semantics (Birkedal et al. [8], Aneris [36]).
    Background mechanized logic accepted as foundation; not re-proven here.
  • domain assumption Clients under consideration are verified against the universal Hoare triple ∀lib.{specI(lib)} e⊕lib {True}.
    Theorem 5.1 only covers programs with such proofs; unverified clients are outside the theorem's scope.
  • domain assumption Databases are AnerisLang programs matching the key-value API init/start/read/write/commit.
    The method is tied to the AnerisLang key-value API; SQL and richer APIs are out of scope, as acknowledged in Section 9.
invented entities (3)
  • Global event trace t with pre/post events and fresh/emit ghost operations
    purpose: Level-1 record of every database operation start/end, used to extract transactions for the consistency model.
    Formal bookkeeping added to the AnerisLang operational semantics; adapted from Birkedal et al. [8]; erasable and has no runtime counterpart.
  • Linearization-point sequence (level 2) with PermissionLin/PermissionPost ghost resources
    purpose: Gives each operation a logical order point and lets the proof update the trace invariant per operation.
    Ghost-theory construct internal to the Iris proof; no empirical handle outside the paper.
  • LatestWrite(k, ov, c) wrapping resource
    purpose: Strengthens the local points-to resource so the read linearization point can be inserted while maintaining ReflectSI.
    Definition in Section 7 used only inside the proof; no observable runtime effect.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Isolation Levels of Database Implementations for Free Using Separation Logic." pith.science (2026). https://pith.science/paper/7NR6CDQZ

@misc{pith2026260715877,
  author       = {Pith},
  title        = {Pith review of: Verifying Isolation Levels of Database Implementations for Free Using Separation Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7NR6CDQZ}},
  note         = {Machine review of arXiv:2607.15877}
}
read the original abstract

Modern databases are highly concurrent and provide transactions as a mean of grouping several database operations into atomically applied units. Database vendors and software engineers use isolation levels to describe the consistency guarantees of transactions. The popular isolation levels give weak guarantees, with intricate semantics, to optimize performance of applications. The problem of assuring that database implementations actually implement the isolation level guarantees that application developers build their systems upon has received a great deal of attention from the testing community. But until now, there exists no method for formally verifying that a database implementation actually implements the isolation level that database vendors says it provides. In this paper, we present a method for verifying that a database implements an isolation level: we derive isolation levels directly, as formalized in transactional consistency models by the database community, from the structure of separation logic specifications. By doing so, we consider all program executions that a database and arbitrary clients of the database could produce. The result is a so-called free theorem meaning that any database implementation, whose operations are verified against a specific set of separation logic specifications, actually implements its isolation level. As all proofs in this paper are mechanized in the Rocq proof assistant and build upon a detailed semantic model of program execution, we believe this contribution raises the bar for the achievable robustness of databases.

Figures

Figures reproduced from arXiv: 2607.15877 by the authors.

Figure 1
Figure 1. Extraction method exemplified with the read operation. emitting the post event into the global trace does not brake the invariant for each of the database operations; where we get to assume that the database operations satisfy their separation logic specifications. Thus, in summary, we are proving isolation levels from the structure of separation logic specifications alone. In Section 6, we present the proof structu… view at source ↗
Figure 2
Figure 2. Comparison of prior work about verification of database and software transactional memory imple [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. The write skew example. Isolation levels. Having formal￾ized what a transaction is, the next step is to define transac￾tional guarantees, i.e., isolation levels. We can think of an isola￾tion level as all the executions of a transactional workload we will allow. Throughout this paper, we primarily focus on one particular isolation level, namely snapshot isolation, to explain our ideas. Snapshot isolation, together w… view at source ↗
Figures from the paper (13 more)
Figure 4
Figure 4. Figure 4: The write skew example in the state-based model with its two possible executions. Both executions start from the initial state, here we represent the initial values as version zero, e.g., 𝑥0, but they differ in which transaction applies its write first. The fact that s…
Figure 5
Figure 5. Figure 5: Isolation levels defined using state-based commit tests. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Specification for snapshot isolation. Parametric resources. As mentioned above, all resources in the specification are existentially quantified. All a user of the specification knows about the resources is that they work with the per-operation specifications. Thus, any…
Figure 7
Figure 7. Figure 7: Per-operation specification for snapshot isolation. [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]
Figure 8
Figure 8. Figure 8: Instrumentation of database operations show one possible trace of pre and post emit events that can come from the write skew example from [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Extraction of the write skew example at level 1 (events from the start and commit operations are omitted). In terms of the operational semantics, we have integrated the code instrumentation primitives fresh and emit of Birkedal et al. [8] into the operational semantics…
Figure 10
Figure 10. Figure 10: An excerpt of Aneris’s operational semantics; [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: Hoare-triple specifications for the fresh and emit code instrumentation operations. where the predicate ValidTrace(I, 𝑡), which we refer to as the global proof invariant, is defined in Equation (The Global Proof Invariant). The argument I is the isolation level that t…
Figure 12
Figure 12. Figure 12: Extraction of the write skew example from level 1 to level 2 (start and commit operations are omitted). 5.3 Set of Transactions Adhering to the State-based Model (Level 3) At level 3, we "chop" the sequence of operations (their linearization points) into sets of trans…
Figure 13
Figure 13. Figure 13: Extraction of the write skew example from level 2 to level 3. 5.4 Implementation Correctness in the State-based Model The rest of (The Global Proof Invariant) asserts that there exists an execution E that is coherent with the set of committed transactions (comTrans(T …
Figure 14
Figure 14. Figure 14: Extraction of the write skew example from level 3 to the model level. Now that we have defined the extraction method, we can formally state our main theorem that gives us implementation correctness for a database implementation verified with the specifications of [3] …
Figure 15
Figure 15. Figure 15: Excerpt of ghost theory. insert a pre event or a post event into the global trace, we need to update ReflectI (𝑡,𝑡) accordingly. These updates can be made using Law 2 and Law 3, respectively. As the code instrumentation, i.e., the emit and fresh expressions, are atomi…
Figure 16
Figure 16. Figure 16: write skew example program. Proving safety of the write skew example, does little to strengthen our assurance that the separation logic specifications correctly captures snapshot isolation; snapshot isolation is known for allowing both transactions in the write skew e…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

62 extracted references · 6 canonical work pages

  1. [3]

    Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, and Lars Birkedal. 2025. Reasoning about Weak Isolation Levels in Separation Logic.Proceedings of the ACM on Programming Languages9, ICFP (2025), 306–340

    2025

  2. [16]

    Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. 2017. Seeing is Believing: A Client-Centric Specification of Database Isolation. InProceedings of the ACM Symposium on Principles of Distributed Computing(Washington, DC, USA)(PODC ’17). Association for Computing Machinery, New York, NY, USA, 73–82. doi:10.1145/3087801.3087802

    arXiv 2017

  3. [1]

    A. Adya. 1999.Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Technical Report. USA

    1999

  4. [2]

    A. Adya, B. Liskov, and P. O’Neil. 2000. Generalized isolation level definitions. InProceedings of 16th International Conference on Data Engineering (Cat. No.00CB37073). 67–78. doi:10.1109/ICDE.2000.839388

    arXiv 2000

  5. [4]

    Aneris-Team. 2023. https://github.com/logsem/aneris/blob/master/documentation.pdf

    2023

  6. [5]

    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky. 2013. A programming language perspective on transactional memory consistency. InProceedings of the 2013 ACM Symposium on Principles of Distributed Computing (Montréal, Québec, Canada)(PODC ’13). Association for Computing Machinery, New York, NY, USA, 309–318. doi:10. 1145/2484239.2484267

    arXiv 2013

  7. [6]

    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky. 2017. Characterizing transactional memory consistency conditions using observational refinement.Journal of the ACM (JACM)65, 1 (2017), 1–44

    2017

  8. [7]

    Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O’Neil, and Patrick O’Neil. 1995. A Critique of ANSI SQL Isolation Levels.SIGMOD Rec.24, 2 (may 1995), 1–10. doi:10.1145/568271.223785

    arXiv 1995

Show all 62 references
  1. [8]

    Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos

  2. [9]

    Ranadeep Biswas and Constantin Enea. 2019. On the complexity of checking transactional consistency.Proc. ACM Program. Lang.3, OOPSLA, Article 165 (Oct. 2019), 28 pages. doi:10.1145/3360591

    2019 doi

  3. [10]

    Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, and Mooly Sagiv. 2012. Eventually Consistent Transactions. In Programming Languages and Systems, Helmut Seidl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 67–86

    2012

  4. [11]

    Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In26th International Conference on Concurrency Theory (CONCUR 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 42), Luca A...

    2015 doi

  5. [12]

    Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A framework for transactional consistency models with atomic visibility. In26th International Conference on Concurrency Theory (CONCUR 2015). Schloss Dagstuhl– Leibniz-Zentrum für Informatik, 58–71

    2015

  6. [13]

    Andrea Cerone and Alexey Gotsman. 2018. Analysing Snapshot Isolation.J. ACM65, 2, Article 11 (Jan. 2018), 41 pages. doi:10.1145/3152396

    2018 doi

  7. [14]

    Chandra, Robert Griesemer, and Joshua Redstone

    Tushar D. Chandra, Robert Griesemer, and Joshua Redstone. 2007. Paxos made live: an engineering perspective. In Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing(Portland, Oregon, USA)(PODC ’07). Association for Computing Machinery, Ne...

    2007

  8. [15]

    Frans Kaashoek, and Nickolai Zeldovich

    Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2023. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In17th USENIX Symposium on Operating Systems Design and Implementat...

    2023

  9. [17]

    Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. InECOOP 2014 – Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 207–231

    2014

  10. [18]

    Luke Dalessandro, Dave Dice, Michael Scott, Nir Shavit, and Michael Spear. 2010. Transactional mutex locks. In European Conference on Parallel Processing. Springer, 2–13

    2010

  11. [19]

    Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. 2013. Towards formally specifying and verifying transactional memory.Formal Aspects of Computing25, 5 (2013), 769–799

    2013

  12. [20]

    Seth Gilbert and Nancy Lynch. 2002. Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services.SIGACT News33, 2 (jun 2002), 51–59. doi:10.1145/564585.564601

    2002

  13. [21]

    Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. 2021. Distributed causal memory: modular specification and verification in higher-order distributed separation logic.Proc. ACM Program. Lang. 5, POPL (2021), 1–29. doi:10.1145/3434323

    2021 doi

  14. [22]

    Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal. 2023. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols.Proc. ACM Program. Lang.7, ICFP, Article 217 (aug 2023), 31 pages. doi:10...

    2023 doi

  15. [23]

    Long Gu, Si Liu, Tiancheng Xing, Hengfeng Wei, Yuxing Chen, and David Basin. 2024. IsoVista: Black-box checking database isolation guarantees.Proceedings of the VLDB Endowment17, 12 (2024), 4325–4328

    2024

  16. [24]

    Rachid Guerraoui and Michal Kapalka. 2008. On the correctness of transactional memory. InProceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming. 175–184

    2008

  17. [25]

    Herlihy and Jeannette M

    Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst.12, 3 (jul 1990), 463–492. doi:10.1145/78969.78972

    1990

  18. [26]

    C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming.Commun. ACM12, 10 (1969), 576–580. doi:10.1145/363235.363259

    1969

  19. [27]

    Kaile Huang, Si Liu, Zhenge Chen, Hengfeng Wei, David Basin, Haixiang Li, and Anqun Pan. 2023. Efficient Black-Box Checking of Snapshot Isolation in Databases.Proc. VLDB Endow.16, 6 (Feb. 2023), 1264–1276. doi:10.14778/3583140. 3583145

    2023 doi

  20. [28]

    Damien Imbs and Michel Raynal. 2012. Virtual world consistency: A condition for STM systems (with a versatile protocol with invisible read operations).Theoretical Computer Science444 (2012), 113–127

    2012

  21. [29]

    Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. InProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. 256–269. doi:10.1145/2951913.2951943

    2016

  22. [30]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic.J. Funct. Program.28 (2018), e20. doi:10.1017/S0956796818000151

    2018 doi

  23. [31]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Program...

    2015

  24. [32]

    Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan. 2017. Alone together: compositional reasoning and inference for weak isolation.Proceedings of the ACM on Programming Languages2, POPL (Dec. 2017), 1–34. doi:10.1145/3158115

    2017 doi

  25. [33]

    Bas Ketsman, Christoph Koch, Frank Neven, and Brecht Vandevoort. 2023. Concurrency control for database theorists. SIGMOD Rec.51, 4 (jan 2023), 6–17. doi:10.1145/3582302.3582304

    2023

  26. [34]

    Kyle Kingsbury and Peter Alvaro. 2020. Elle: inferring isolation anomalies from experimental observations.Proc. VLDB Endow.14, 3 (Nov. 2020), 268–280. doi:10.14778/3430915.3430918

    2020

  27. [35]

    Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. InProgramming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the Europea...

    2017 doi

  28. [36]

    Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal

  29. [37]

    Mohsen Lesani, Victor Luchangco, and Mark Moir. 2012. A framework for formally verifying software transactional memory algorithms. InInternational Conference on Concurrency Theory. Springer, 516–530

    2012

  30. [38]

    Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J Bell, Adam Chlipala, Benjamin C Pierce, and Steve Zdancewic

  31. [39]

    Si Liu, Long Gu, Hengfeng Wei, and David Basin. 2024. Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels.Proc. ACM Program. Lang.8, OOPSLA2, Article 302 (Oct. 2024), 29 pages. doi:10.1145/3689742

    2024 doi

  32. [40]

    Lasse Møldrup and Andreas Pavlogiannis. 2025. AWDIT: An Optimal Weak Database Isolation Tester.Proceedings of the ACM on Programming Languages9, PLDI (2025), 1540–1564

    2025

  33. [41]

    Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. 2023. Modular Verification of State-Based CRDTs in Separation Logic. In37th European Conference on Object-Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPI...

    2023 doi

  34. [42]

    Abel Nieto, Léon Gondelman, Alban Reynaud, and Lars Birkedal. 2022. Modular Verification of Op-Based CRDTs in Separation Logic.Proc. ACM Program. Lang.OOPSLA (2022). Accepted for publication

    2022

  35. [43]

    Susan Owicki and David Gries. 1976. Verifying properties of parallel programs: an axiomatic approach.Commun. ACM19, 5 (May 1976), 279–285. doi:10.1145/360051.360224

    1976

  36. [44]

    Papadimitriou

    Christos H. Papadimitriou. 1979. The Serializability of Concurrent Database Updates.J. ACM26, 4 (oct 1979), 631–653. doi:10.1145/322154.322158 28 Anders Alnor Mathiasen, Amin Timany, and Lars Birkedal

    1979

  37. [45]

    Lauren Pick, Amanda Xu, Ankush Desai, Sanjit A Seshia, and Aws Albarghouthi. 2025. Checking Observational Correctness of Database Systems.Proceedings of the ACM on Programming Languages9, OOPSLA1 (2025), 1661–1688

    2025

  38. [46]

    Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018. On Parallel Snapshot Isolation and Release/Acquire Consistency. InProgramming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 940–967

    2018

  39. [47]

    Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018. On the Semantics of Snapshot Isolation. arXiv:1805.06196 [cs.LO] https://arxiv.org/abs/1805.06196

    2018 arXiv

  40. [48]

    Reynolds

    J.C. Reynolds. 2002. Separation logic: a logic for shared mutable data structures. InProceedings 17th Annual IEEE Symposium on Logic in Computer Science. 55–74. doi:10.1109/LICS.2002.1029817

    2002 arXiv

  41. [49]

    Gerhard Schellhorn, Stefan Bodenmüller, and Wolfgang Reif. 2025. Verification of forward simulations with thread-local, step-local proof obligations.Science of Computer Programming241 (2025), 103227

    2025

  42. [50]

    Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. 2023. Grove: A Separation- Logic Library for Verifying Distributed Systems. InProceedings of the 29th Symposium on Operating Systems Principles (Koblenz, Germany)(SOSP ’23). Association for ...

    2023

  43. [51]

    Tim Soethout, Tijs van der Storm, and Jurgen J. Vinju. 2021. Automated Validation of State-Based Client-Centric Isolation with TLA+. InSoftware Engineering and Formal Methods. SEFM 2020 Collocated Workshops, Loek Cleophas and Mieke Massink (Eds.). Springer International Publis...

    2021

  44. [52]

    Yair Sovran, Russell Power, Marcos K Aguilera, and Jinyang Li. 2011. Transactional storage for geo-replicated systems. InProceedings of the Twenty-Third ACM Symposium on Operating Systems Principles. 385–400

    2011

  45. [53]

    Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. 2024. Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.Proc. ACM Program. Lang.8, POPL, Article 9 (ja...

    2024 doi

  46. [54]

    Pierce, and Steve Zdancewic

    Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic

  47. [55]

    Yu Xia, Xiangyao Yu, Matthew Butrovich, Andrew Pavlo, and Srinivas Devadas. 2022. Litmus: Towards a practical database management system with verifiable acid properties and transaction correctness. InProceedings of the 2022 international conference on management of data. 1478–1492

    2022

  48. [56]

    2020.Parametric Operational Semantics for Consistency Models

    Shale Xiong. 2020.Parametric Operational Semantics for Consistency Models. PhD thesis. Imperial College London

    2020

  49. [57]

    Jian Zhang, Ye Ji, Shuai Mu, and Cheng Tan. 2023. Viper: A Fast Snapshot Isolation Checker. InProceedings of the Eighteenth European Conference on Computer Systems(Rome, Italy)(EuroSys ’23). Association for Computing Machinery, New York, NY, USA, 654–671. doi:10.1145/3552326.3567492

    2023

  50. [58]

    Zhanhao Zhao, Hexiang Pan, Gang Chen, Xiaoyong Du, Wei Lu, and Beng Chin Ooi. 2023. VeriTxn: Verifiable transactions for cloud-native databases with storage disaggregation.Proceedings of the ACM on Management of Data1, 4 (2023), 1–27. Verifying Isolation Levels of Database Imp...

    2023

  51. [2019]

    ACM Program

    Interaction trees: representing recursive and impure programs in Coq.Proc. ACM Program. Lang.4, POPL, Article 51 (Dec. 2019), 32 pages. doi:10.1145/3371119

    2019 doi

  52. [2020]

    Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. InProgramming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, ...

    2020 doi

  53. [2021]

    ACM Program

    Theorems for Free from Separation Logic Specifications.Proc. ACM Program. Lang.5, ICFP, Article 81 (aug 2021), 29 pages. doi:10.1145/3473586

    2021 doi

  54. [2022]

    C4: verified transactional objects.Proceedings of the ACM on Programming Languages6, OOPSLA1 (2022), 1–31

    2022

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.