Pith. sign in

REVIEW 3 major objections 4 minor 30 references

On the Complexity of Checking Transactional Consistency

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read The paper proves that checking read committed, read atomic, and causal consistency is polynomial-time, while checking prefix consistency and snapshot isolation is NP-complete, with polynomial-time algorithms for the hard cases when the…

desk verdict Solid complexity results for PC and SI, but the RC algorithm is buggy and the model omits commit timing, so the practical claims need a careful rewrite. read the letter →

arxiv 1908.04509 v1 pith:6TDQAVBX submitted 2019-08-13 cs.DB cs.PL

Ranadeep Biswas , Constantin Enea This is my paper · ORCID
classification cs.DBcs.PL MSC 68Q1768P1568Q25
keywords transactionalconsistencyreadcommittedatomiccausalprefixsnapshotisolationserializabilitycheckingNP-completeness
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 asks how hard it is to decide whether a recorded transaction execution really satisfies a weak consistency model, the question behind black-box testing of databases. It claims that read committed, read atomic, and causal consistency can be checked in polynomial time, while prefix consistency and snapshot isolation are NP-complete, joining serializability on the hard side. The polynomial algorithms are saturation procedures that build the forced commit-order edges by instantiating axioms from a uniform axiomatic schema. For the NP-complete models, the paper gives a polynomial-time route when the history's width, such as the number of sessions, or the size of biconnected components of its communication graph is fixed. If the claims are right, consistency checking can be automated for the easy models and made practical for the hard ones in bounded-width executions.

What carries the argument

The load-bearing object is the uniform axiomatic schema for consistency criteria, in which each axiom is a first-order implication forcing commit-order predecessors for any transaction whose write is read. The paper also uses two algorithmic constructions: a saturation procedure that instantiates these axioms to close a partial commit order, and a reduction from prefix consistency and snapshot isolation to serializability that splits each transaction into separate read and write transactions, with auxiliary variables for snapshot isolation to forbid conflicting transactions from observing the same prefix. For bounded width, serializability is checked by a search over antichains of the session order, and for communication graphs, by checking each biconnected component in isolation.

What would settle it

Take a database execution whose write-read relation is fixed and compare the paper's Read Committed axiom with the ANSI SQL read-committed definition: if a history is rejected by the paper's monotonicity condition but accepted by the SQL definition, the polynomial-time result would not transfer to standard read committed. For the NP-hardness half, a direct check is to instantiate the SAT reduction on a small satisfiable formula and verify that the constructed history is prefix consistent exactly when the formula is satisfiable, and that an unsatisfiable formula yields a cyclic commit order.

Watch

Extended reading notes

Core claim

The paper's central discovery is a complexity dichotomy for verifying transactional consistency, expressed through a uniform axiomatic framework. A history is a set of transactions with a session order and a write-read relation, and each criterion is the existence of a total commit order extending both and satisfying an axiom of the form: whenever a transaction $t_1$ writing $x$ is read by $t_3$, every competing writer $t_2$ of $x$ that is related to $t_3$ in a criterion-specific way must commit before $t_1$. Under this framework, read committed, read atomic, and causal consistency yield acyclic forced-order constraints computable in polynomial time, so checking them is polynomial. Prefix consistency and snapshot isolation are NP-complete, proved by one SAT reduction in which truth values of formula variables and literals are encoded by the polarity of the commit order between paired transactions, and unsatisfied clauses become commit-order cycles. The same reduction also gives a new NP-completeness proof for serializability. The paper further proves that prefix consistency, snapshot isolation, and serializability become polynomial when the history width is bounded, by reducing the first two to serializability through splitting each transaction into a read part and a write part, adding auxiliary variables for snapshot isolation, and solving serializability by search over session-order antichains; and that all criteria decompose over biconnected components of the communication graph.

Load-bearing premise

The complexity proofs assume the paper's axiomatic definitions are faithful to what databases mean by these consistency levels; in particular, its Read Committed axiom includes a within-transaction monotonicity condition that may be stronger than the ANSI SQL definition of read committed.

Editorial extensions

If this is right

  • Checking read committed, read atomic, and causal consistency can be fully automated in polynomial time for arbitrary histories, enabling precise black-box monitoring rather than anomaly-pattern matching.
  • Prefix consistency and snapshot isolation are NP-complete in general, so no polynomial-time algorithm for arbitrary histories exists unless P equals NP.
  • When the number of sessions or the width of a history is fixed, prefix consistency, snapshot isolation, and serializability become polynomial-time checkable, making them practical for many real deployments.
  • When every biconnected component of the communication graph has bounded size, all the considered consistency criteria are polynomial-time checkable even if the total number of sessions is unbounded.
  • The experimental results show that these algorithms can be orders of magnitude more efficient than direct SAT encodings and can expose consistency violations in production database executions.

Reading between the lines

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

  • If the axiomatic equivalence to earlier formalizations holds only for histories where every value is written at most once, then databases whose behavior depends on concrete values, violating data independence, could escape both the polynomial algorithms and the NP-completeness transfer.
  • The same axiom schema could classify other consistency models: any criterion expressible with a fixed first-order axiom of that shape would inherit the polynomial saturation argument unless the axiom mentions commit order on the left-hand side.
  • The read/write-splitting reduction turns a prefix consistency or snapshot isolation checker into a serializability checker, so tools built for serializability monitoring could be repurposed for weaker models with the same core engine.
  • The reported absence of large biconnected components in experimental histories suggests the worst case may be rare; testing on histories with more sessions and variables could reveal when communication-graph decomposition actually pays off.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper introduces an axiomatic framework for read committed (RC), read atomic (RA), causal consistency (CC), prefix consistency (PC), snapshot isolation (SI), and serializability (SER), where histories are triples (T, so, wr) and a consistency criterion holds if a total commit order co extending so ∪ wr satisfies a set of first-order axioms. The main theoretical results are that RC, RA, and CC are polynomial-time checkable, while PC, SI, and SER are NP-complete, with polynomial-time algorithms when the width of the session order or the size of biconnected components of the communication graph is fixed. The paper also reports an experimental evaluation on histories extracted from CockroachDB, Galera, and AntidoteDB.

Significance. If the axiomatic definitions are accepted as faithful formalizations of the named consistency models, the paper fills a real gap in the literature: it provides the first systematic complexity study of checking transactional consistency beyond serializability, gives a uniform SAT-reduction for the NP-complete cases, and supplies fixed-parameter tractability results for bounded width and bounded biconnected components. The proofs are largely self-contained and do not appear circular; the reduction in Section 3.2 is concrete, and the algorithms in Sections 4 and 5 are clearly defined and backed by an experimental comparison against a SAT baseline. The main value of the paper is therefore contingent on the semantic fidelity of the axiom system to the consistency models that databases actually implement.

major comments (3)
  1. [§2.2, Fig. 2(a), Def. 2.5] The formalization of Read Committed does not capture the standard P1 (dirty read) prohibition, because Def. 2.2 histories contain no commit timestamps or read timestamps. A history with transaction t1 writing x, transaction t2 reading x from t1, and t1 committing only after that read but before t2 commits has exactly the same representation as a clean read, and the RC axiom in Fig. 2(a) is vacuous when the read is the first read of x in t2. Thus the polynomial-time result of Thm. 3.1 for RC is not a complexity result for the ANSI/SQL read-committed semantics, which forbids dirty reads. Moreover, the RC axiom adds a within-transaction monotonicity condition that is stronger than standard read committed, so even after adding timestamps the equivalence would require justification.
  2. [§3, Appendix E] The claimed equivalence with the Cerone et al. formalization is not sufficient to repair the dirty-read gap. Appendix E defines the visibility relation as wr ∪ so or its transitive closure, which makes every writer in wr visible to the reader, including a writer that has not committed at the time of the read; no axiom or preprocessing step in the paper rules out such writes. Since the appended equivalence proof is informal and, as the appendix itself notes, does not cover RC at all, the paper has not established that any of the main results apply to the standard consistency models rather than to the paper's own axioms. This is a load-bearing assumption for the title and abstract claims.
  3. [Appendix B, Algorithm 3] The printed algorithm for Read Committed does not implement the RC axiom of Fig. 2(a). The axiom's antecedent requires ⟨t2, α⟩ ∈ wr ; po, but line 6 of Algorithm 3 checks ∃α, β with ⟨t1, α⟩ ∈ wrx, ⟨t2, β⟩ ∈ (so ∪ wr), and ⟨α, β⟩ ∈ po. This is type-incorrect because so relates transactions while α and β are operations, and it differs from the proof text in the same appendix, which correctly uses ⟨t2, β⟩ ∈ wr. As printed, Algorithm 3 checks a different property, so Thm. 3.1's proof does not match the algorithm it refers to. The output comments of Algorithms 3 and 4 also incorrectly say 'Causal consistency' instead of the intended models.
minor comments (4)
  1. [§7] The sentence 'sequential consistency is g serializability' is garbled and should be rewritten, as it does not convey a coherent technical claim.
  2. [Appendix E] The equivalence proofs are only sketched; for reproducibility, the construction of the visibility relation vis from a given commit order co should be given explicitly in both directions for each model, rather than by example and assertion.
  3. [§6, Table 2] The violation statistics are interesting, but the paper should state whether the extracted histories were filtered to exclude executions in which a transaction reads a value written by a not-yet-committed transaction; without such a statement, the experimental results inherit the semantic ambiguity of the RC/RA definitions.
  4. [§2.1] The remark that 'A history includes only successful or committed transactions' conflates 'successful' with 'committed'; a transaction can be successful but uncommitted at the time of a read, and the formalism should be explicit about how commit events are represented.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the complexity theorems are proved directly from the paper's own explicit axioms and reductions, with self-citations present only in contextual related-work passages.

full rationale

I walked the derivation chain for the central claims (polynomial-time checkability of RC/RA/CC, NP-completeness of PC/SI/SER, and the bounded-width and biconnected-component fixed-parameter tractability results). All of these are proved directly from the paper's explicitly stated axiomatic definitions (Definition 2.5, Figure 2, Table 1). The polynomial-time algorithms (Algorithm 1 and its RC/RA analogues) are saturation procedures whose soundness and completeness are proved in Appendix B by showing that the saturated order is acyclic iff a valid total commit order exists; no fitted parameter or target-consistency assumption is used as an input. The NP-hardness proof (Theorem 3.2) is a self-contained reduction from SAT to histories h_phi, with the two implications proved from the Prefix/Serializability axioms and Lemma 3.3. The PC-to-SER and SI-to-SER reductions (Section 4) are explicit constructions with acyclicity arguments relating co'_1, co'_2, RW(co'_1), and WR(co'_1) to Prefix/Conflict violations; they are not circular. The communication-graph decomposition (Section 5) is proved by a minimal-path argument over biconnected components. The only self-citations are [11] and [17], used in related work to position the results as extensions of prior causal-consistency and linearizability-monitoring work; these citations are not load-bearing for the paper's proofs. The claim that the axiomatic definitions are equivalent to the formalization of Cerone et al. [14] (Appendix E) is informal and concerns external semantic adequacy, not circular reasoning: a mismatch with database implementations would be a correctness or scope issue, not a reduction of a claimed result to its own input. No self-definitional, fitted-input, or uniqueness-imported-by-self-citation pattern is present.

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

No free parameters or invented entities. The central claims rest on domain assumptions about how histories are represented (explicit write-read relation, unique write values, data-independence), syntactic simplifications of transactions, and the equivalence of the paper's axioms with prior standard formalizations.

assumptions (5)
  • domain assumption Histories come with an explicit write-read relation wr, and executions can be restricted to those where each value is written at most once.
    Section 2.1 justifies via data-independence [25], claiming any buggy behavior can be exposed in such executions. Load-bearing for applicability of all algorithms to real executions.
  • domain assumption Each transaction has at most one write per variable, and reads of a variable are not preceded by writes to that variable in the same transaction.
    Section 2.1 argues these syntactic simplifications are without loss of generality because only last writes and non-preceded reads are constrained by consistency criteria.
  • domain assumption Aborted transactions can be ignored because their effects are never visible.
    Section 2.1, stated as a standard database assumption.
  • domain assumption The axiomatic definitions in Figure 2 are equivalent to previous formalizations by Cerone et al. [14].
    Appendix E gives an informal equivalence proof; this is load-bearing because the complexity results are proved for these axioms, not for the original definitions.
  • domain assumption The session order is a strict partial order that is a union of sequences (sessions), and the number of sessions or width is a relevant fixed parameter.
    Section 4 defines width; Section 5 assumes session order is a union of sequences. The fixed-parameter results rely on this.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the Complexity of Checking Transactional Consistency." pith.science (2026). https://pith.science/paper/6TDQAVBX

@misc{pith2026190804509,
  author       = {Pith},
  title        = {Pith review of: On the Complexity of Checking Transactional Consistency},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6TDQAVBX}},
  note         = {Machine review of arXiv:1908.04509}
}
read the original abstract

Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different consistency models for transactions corresponding to different tradeoffs between consistency and availability. In this work, we investigate the problem of checking whether a given execution of a transactional database adheres to some consistency model. We show that consistency models like read committed, read atomic, and causal consistency are polynomial time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete consistency models, we devise algorithms that are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. We evaluate the scalability of these algorithms in the context of several production databases.

Figures

Figures reproduced from arXiv: 1908.04509 by the authors.

Figure 1
Figure 1. Examples of transactions used to justify our simplifying assumptions (each box represents a different [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Definitions of consistency axioms. The reflexive and transitive, resp., transitive, closure of a relation [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Examples of histories used to explain the axioms in Figure 2. For readability, the [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (14 more)
Figure 4
Figure 4. Figure 4: Applying the RA and CC checking algorithms. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Sub-histories included in hφ for each literal λij and variable xk . to represent the Causal axiom. The following is a consequence of the fact that these algorithms run in polynomial time (or equivalently, the Datalog programs can be evaluated in polynomial time over a …
Figure 6
Figure 6. Figure 6: Applying checkSER on the serializable history on the left. The right part pictures a search for valid [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Reducing PC to SER. Initially, the value of every variable is 0. [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: Cycles with non-consecutive write transactions. • Since [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: Cycles in co′ 2 correspond to Prefix violations. Proof. Assume that co′ 2 is cyclic. Any min￾imal cycle in co′ 2 still satisfies the properties of minimal cycles of co′ 1 proved in Lemma 4.5 (be￾cause all write transactions are still totally or￾dered and co′ 2 doesn’t …
Figure 10
Figure 10. Figure 10: Prefix violations correspond to cycles in [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]
Figure 11
Figure 11. Figure 11: Reducing SI to SER. Note that hR |W and h c R |W have the same width (the session order is defined exactly in the same way), which implies, by Lemma 4.4, that h and h c R |W have the same width. The following result can be proved using similar reasoning as in the case…
Figure 12
Figure 12. Figure 12: A history and its communication graph. Formally, a communication graph of a history h is an undirected graph Comm(h) = (V, E) where the set of vertices V is the set of sessions in h 10, and (v,v ′ ) ∈ E iff the sessions v and v ′ contain two transactions t1 and t2, re…
Figure 13
Figure 13. Figure 13: Minimal paths between transac￾tions in the same biconnected component. • if ⟨t3,t4⟩ ∈ so, then there exists a smaller path between t0 and t1 that uses the so relation between ⟨t3,t4⟩ (we recall that so ⊆ Ð i coi ) instead of the transactions in C2, pictured in Figure …
Figure 14
Figure 14. Figure 14: Scalability of our Serializability checking algorithm in Section 4.1 and a comparison to a SAT encoding. [PITH_FULL_IMAGE:figures/full_fig_p022_14.png]
Figure 15
Figure 15. Figure 15: Scalability of SI and CC checking, and a comparison to a SAT encoding. [PITH_FULL_IMAGE:figures/full_fig_p023_15.png]
Figure 16
Figure 16. Figure 16: Cycles in co′ 2 corresponding to Conflict violations. Now we prove, if co is not acyclic, then h does not satisfie Read Committed. If the history is Read Committed, there must be a commit order co′ for h, for which ⟨h, co′ ⟩ satisfies Read Committed. co′ must be acycl…
Figure 17
Figure 17. Figure 17: ∀co′ .∃co.⟨h ′ , co′ ⟩ |= Serializability ⇒ ⟨h, co⟩ |= Prefix ∧ Conflict ∀(O, po) ∈ t, ∀o ∈ O, o = read(x,n)∧  o ′ ∈ po−1 (o) | o ′ = _(x, _) [PITH_FULL_IMAGE:figures/full_fig_p032_17.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 17 canonical work pages

  1. [1]

    [n. d.]. http://jepsen.io Retrieved March 28th, 2019

    work page 2019

  2. [2]

    [n. d.]. https://github.com/jepsen-io/jepsen/blob/master/galera/src/jepsen/galera/dirty_reads.clj Retrieved March 28th, 2019

    work page 2019

  3. [3]

    [n. d.]. https://github.com/cockroachdb/cockroach Retrieved March 28th, 2019

    work page 2019

  4. [4]

    [n. d.]. https://www.cockroachlabs.com/docs/v2.1/transactions.html#isolation-levels Retrieved March 28th, 2019

    work page 2019

  5. [5]

    [n. d.]. http://galeracluster.com Retrieved March 28th, 2019

    work page 2019

  6. [6]

    [n. d.]. http://galeracluster.com/documentation-webpages/faq.html Retrieved March 28th, 2019

    work page 2019

  7. [7]

    [n. d.]. http://galeracluster.com/documentation-webpages/isolationlevels.html# intra-node-vs-inter-node-isolation-in-galera-cluster Retrieved March 28th, 2019

    work page 2019

  8. [8]

    [n. d.]. https://www.antidotedb.eu Retrieved March 28th, 2019

    work page 2019

Show all 30 references
  1. [9]

    [n. d.]. https://antidotedb.gitbook.io/documentation/overview/configuration Retrieved March 28th, 2019

    2019

  2. [10]

    Bernstein, Jim Gray, Jim Melton, Elizabeth J

    Hal Berenson, Philip A. Bernstein, Jim Gray, Jim Melton, Elizabeth J. O’Neil, and Patrick E. O’Neil. 1995. A Critique of ANSI SQL Isolation Levels. In Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, San Jose, California, USA, May 22-25, 1995....

    1995

  3. [11]

    Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017. On verifying causal consistency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Go...

    2017

  4. [12]

    Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014. Replicated data types: specification, verification, optimality. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2...

    2014

  5. [13]

    Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. 2015. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague, Czech Republic (LIPIc...

    2015 doi

  6. [14]

    Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015 (LIPIcs) , Luca Aceto and David de Fruto...

    2015 doi

  7. [15]

    Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2018. Data-centric dynamic partial order reduction. PACMPL 2, POPL (2018), 31:1–31:30. https://doi.org/10.1145/3158119

    2018 doi

  8. [16]

    Niklas Eén and Niklas Sörensson. 2003. An Extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers (Lecture Notes in Computer Science) , Enrico Giu...

    2003 doi

  9. [17]

    Michael Emmi and Constantin Enea. 2018. Sound, complete, and tractable linearizability monitoring for concurrent collections. PACMPL 2, POPL (2018), 25:1–25:27. https://doi.org/10.1145/3158113

    2018 doi

  10. [18]

    Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 , Jens Palsberg...

    2005

  11. [19]

    Gibbons and Ephraim Korach

    Phillip B. Gibbons and Ephraim Korach. 1997. Testing Shared Memories. SIAM J. Comput. 26, 4 (1997), 1208–1244. https://doi.org/10.1137/S0097539794279614

    1997 doi

  12. [20]

    Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978), 558–565. https://doi.org/10.1145/359545.359563

    1978

  13. [21]

    Mazurkiewicz

    Antoni W. Mazurkiewicz. 1986. Trace Theory. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986 (Lecture Notes in Computer Science), Wilfried Brauer, Wolfgang Reis...

    1986 doi

  14. [22]

    Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, and Georg Weissenbacher. 2018. Randomized testing of distributed systems with probabilistic guarantees. PACMPL 2, OOPSLA (2018), 160:1–160:28. https://doi.org/10.1145/3276530

    2018 doi

  15. [23]

    Papadimitriou

    Christos H. Papadimitriou. 1979. The serializability of concurrent database updates. J. ACM 26, 4 (1979), 631–653. https://doi.org/10.1145/322154.322158 , Vol. 1, No. 1, Article . Publication date: August 2018. On the Complexity of Checking Transactional Consistency 27

    1979

  16. [24]

    Terry, Alan J

    Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent B. Welch. 1994. Session Guarantees for Weakly Consistent Replicated Data. In Proceedings of the Third International Conference on Parallel and Distributed Information Systems (PDIS 94),...

    1994

  17. [25]

    Pierre Wolper. 1986. Expressing Interesting Properties of Programs in Propositional Temporal Logic. InConference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986. ACM Press, 184–193. https://...

    1986

  18. [26]

    Along with them, we define a partial commit order WR(co′ 1) WR(co′

    as in the case of prefix consistency. Along with them, we define a partial commit order WR(co′ 1) WR(co′

  19. [27]

    ={ Wt1, Rt2 |∃x2,1∈ vars(hc R|W). Rt2,Wt2 ∈ wrx2, 1 ′, Wt1,Wt2 ∈ co′ 1,Wt1 writes x2,1} which intuitively, enforces that the read part Rt2 of a transaction t2 observes the effects of the write part Wt1 of a transaction t1 when t1 and t2 write on a common variable and the commi...

  20. [28]

    Differently from the previous case, the cycle in co′ 2 here can also contains the dependencies in WR(co′

    since this would imply that it contains two non-consecutive write transactions. Differently from the previous case, the cycle in co′ 2 here can also contains the dependencies in WR(co′

  21. [29]

    The case of minimal cycles in co′ 2 that contain only a dependency from RW(co′ 1), and no dependencies from WR(co′ 1), can be dealt with as in the case of PC

    which are from write transactions to read transactions. The case of minimal cycles in co′ 2 that contain only a dependency from RW(co′ 1), and no dependencies from WR(co′ 1), can be dealt with as in the case of PC. Consider a minimal cycle ofco′ 2 that contains a dependency Wt...

  22. [30]

    For the “if” direction, let co′ be a commit (total) order on transactions of hc R|W which satis- fies the serializability axiom

    The relations between these transactions of hc R|W imply that the corresponding transactions of h are related as shown in Figure 16b, which implies a violation of Conflict, a contradiction of the hypothesis. For the “if” direction, let co′ be a commit (total) order on transact...

    2018

Pith tools

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