{"id":"cfe0bdf1-6883-4902-88e5-b5a5246e8cfa","arxiv_id":"1908.04509","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Checking read committed, read atomic, and causal consistency is polynomial-time, while prefix consistency and snapshot isolation are NP-complete, with polynomial algorithms when session counts are fixed.","lead":"This paper analyzes the computational difficulty of automatically checking whether a database execution obeys a given transactional consistency model. It identifies which models are easy to check, which are inherently hard, and provides practical algorithms for the hard cases.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Formal histories omit commit/read timing, so the RC axioms accept dirty reads from later-committed writers; equivalence to standard consistency models is not established.","rationale":"The reader's verdict is CONDITIONAL, and my stress-test supports keeping that verdict. The reader's weakest assumption was that the paper's axiomatic definitions faithfully capture standard consistency semantics; I agree that this is load-bearing, but I found a more concrete and more damaging mismatch than the RC monotonicity point. The history model records no commit or read timestamps, only a write-read relation and session order. Standard read committed forbids dirty reads: a read must not observe a value written by a transaction that has not yet committed. In the paper's abstraction, a dirty read from a transaction that later commits is indistinguishable from a legitimate read, because the wr relation is identical and the commit order can place the writer before the reader. The RC axiom is vacuous in the minimal dirty-read history, so the polynomial checker accepts an execution that violates the standard isolation level. The same issue applies to the claimed equivalence with Cerone et al.: the proof in Appendix E chooses visibility relations that include all wr edges, so a dirty read can be declared visible even though the writer was not committed at read time. This is not merely a proof gap; it changes the extension of the consistency predicate. The NP-completeness and polynomial-time results may still be correct for the paper's formal definitions, but without timestamps or an explicit commitment-before-read convention the results do not transfer to database read committed as usually understood. I also noted the concrete error in Algorithm 3's pseudocode (reversed po direction and so union wr), but that is a fixable presentation issue rather than a threat to the formal framework. Because the formal complexity theorems are likely sound for the stated definitions, the appropriate response is to require the authors to clarify align the semantic model (or restrict the practical claims), which is exactly a conditional accept rather than a rejection.","tokens_in":33419,"tokens_out":25804,"duration_ms":273290,"concrete_test":"Take the two-transaction history U: write x=1; T: read x=1, with no session order between U and T, wr(U, read)=T, and U's commit after T's read but before T's commit. Evaluate the paper's RC definition (Definition 2.5 + Fig. 2a): since no read of x precedes T's read, the axiom imposes no constraint, and co={U<T} witnesses satisfaction, so the checker accepts. Under Berenson et al. P1 this is a dirty read and must be rejected. Run the published Algorithm 3 on this input: it also accepts. This counterexample settles whether the formal RC is standard read committed; if the authors intend a commitment-before-read assumption, it must be stated and enforced in the extraction of wr.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central theorems prove complexity for Definition 2.5 histories (T, so, wr) with the axioms of Figure 2. For these to be complexity results about real consistency models, the axioms must match standard semantics. Appendix E attempts equivalence with Cerone et al., but it is informal and does not cover RC; moreover, none of the definitions carry commit or snapshot timestamps. Consequently, a dirty read -- T reading x from U before U commits, with U committing later -- is represented identically to a clean read: the wr relation contains (U, read), so any co must place U before T, and the RC axiom is vacuous. The polynomial RC checker therefore returns true for an execution that violates ANSI P1 (dirty read). The same lack of timing infects the claimed equivalence with Cerone et al., whose Ext axiom is checked by taking vis to be wr union so (or its closure), thereby declaring the uncommitted writer visible. Unless the authors restrict to executions where dirty reads cannot occur, or add commit timestamps to the history, the polynomial-time and NP-completeness results are not about the consistency models databases implement.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":33615,"tokens_out":8860,"duration_ms":97859,"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":[{"comment":"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.","section":"§2.2, Fig. 2(a), Def. 2.5"},{"comment":"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.","section":"§3, Appendix E"},{"comment":"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.","section":"Appendix B, Algorithm 3"}],"minor_comments":[{"comment":"The sentence 'sequential consistency is g serializability' is garbled and should be rewritten, as it does not convey a coherent technical claim.","section":"§7"},{"comment":"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.","section":"Appendix E"},{"comment":"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.","section":"§6, Table 2"},{"comment":"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.","section":"§2.1"}],"recommendation":"major_revision","confidential_remarks":"The main risk is scope: the title and abstract promise results about standard database consistency models, while the formal results are proved for the authors' axiomatic definitions. I recommend asking the authors to either extend the formalism with commit/read timing and prove the equivalence, or explicitly restrict the claims to their own axiom system. The complexity results themselves are coherent and likely correct for that system, so the paper is repairable, but the revision is substantial."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version first: this paper has the first NP-completeness results for prefix consistency and snapshot isolation, plus a neat polynomial-time algorithm for fixed-width histories and a useful empirical section. You should take it seriously. But the Read Committed part is a problem: Algorithm 3 in the appendix uses the wrong condition relative to the paper's own axiom, and the entire history model lacks commit/read timestamps, so the formalization cannot distinguish a dirty read from a clean one. That means the claimed polynomial-time checkers for RC are not about the consistency model databases actually implement.\n\nWhat's genuinely new and good: the NP-completeness proofs for PC and SI appear sound, and the reduction from SAT is uniform across PC/SI/SER, giving a new proof of Papadimitriou's result. The fixed-width and fixed-biconnected-component algorithms are elegant and clearly explained. The experimental work found real bugs in CockroachDB and Galera, and the AntidoteDB violations are confirmed by the developers; that's a solid practical contribution.\n\nSoft spots, in rough order of importance. First, the RC algorithm: line 6 of Algorithm 3 checks (so∪wr) with ⟨α,β⟩∈po, but the RC axiom (Figure 2a) requires ⟨t2,α⟩∈wr;po, i.e., an earlier read in program order picking up a value from t2. The two are not equivalent, and the proof in Appendix B doesn't repair the mismatch. Second, the histories carry no commit or read timing. Since every transaction in the history is committed by definition, the \"read from a committed transaction\" part of RC is vacuous, and a read executed before the writer committed looks identical to one executed after. So the RC check accepts executions that violate ANSI P1. The claimed equivalence with Cerone et al. in Appendix E is informal and doesn't cover RC at all. I don't think this kills the PC/SI/SER results—those models are defined through the commit order and the axioms, and the reductions are self-contained—but it does mean the paper's external claims need to be stated more carefully.\n\nMinor: the appendix algorithms are labeled 'Causal consistency' but are for RC and RA.\n\nWho should read this: anyone working on verification of transactional consistency; the fixed-width algorithm is directly useful. It deserves a serious referee, but the RC section needs to be fixed—either by correcting the algorithm and adding timestamps to the model, or by restricting the claims to a version of RC that matches the axioms.","headline":"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.","tokens_in":34106,"tokens_out":5707,"would_cite":true,"duration_ms":58821,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68P15","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["transactional consistency","read committed","read atomic","causal consistency","prefix consistency","snapshot isolation","serializability checking","NP-completeness"],"falsifier":"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.","tokens_in":33233,"feed_emoji":"⚖️","tokens_out":4762,"duration_ms":45817,"temperature":0.7,"pith_summary":"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.","feed_headline":"Three consistency checks are fast; two are NP-complete","feed_subtitle":"A uniform axiom framework maps when verifying database consistency is polynomial and when it hits a hard wall.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Provides the original definitions of read committed, read atomic, and snapshot isolation that the paper's axioms are meant to capture.","marker":"[10]"},{"why":"Gives the formalization of these consistency models using visibility and commit order, which Appendix E shows is equivalent to the paper's write-read-based axioms.","marker":"[14]"},{"why":"Establishes the NP-completeness of checking serializability, the baseline result that the paper complements and reproves with a new reduction.","marker":"[23]"},{"why":"Shows polynomial-time checking of causal consistency in a non-transactional setting, which the paper extends to transactions.","marker":"[11]"},{"why":"Introduces the visibility and arbitration-order specification methodology that underlies the paper's axiomatic framework.","marker":"[12]"},{"why":"Supplies the communication-graph abstraction that the paper adapts to decompose consistency checking over biconnected components.","marker":"[15]"},{"why":"Introduces prefix consistency through the global sequence protocol, the model the paper formalizes with the Prefix axiom.","marker":"[13]"},{"why":"Defines session guarantees, the basis for the session order that organizes transactions in the paper's histories.","marker":"[24]"},{"why":"Supports the data-independence assumption used to justify histories where each value is written at most once.","marker":"[25]"}],"fun_headline_variants":["Three consistency checks easy, two NP-complete","Verifying database consistency: a complexity divide","Snapshot isolation and prefix consistency: NP-complete","When checking transactional consistency is tractable","Axiomatic framework separates easy and hard consistency checks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Three consistency checks easy, two NP-complete","Verifying database consistency: a complexity divide","Snapshot isolation and prefix consistency: NP-complete","When checking transactional consistency is tractable","Axiomatic framework separates easy and hard consistency checks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000202,"raw_usage":{"total_tokens":1388,"prompt_tokens":957,"completion_tokens":431,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":573,"completion_tokens_details":{"reasoning_tokens":362}},"tokens_in":573,"tokens_out":431,"duration_ms":4811,"temperature":1.0,"reasoning_tokens":362,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:40:43.359850+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows polynomial-time checking of causal consistency in a non-transactional setting, which the paper extends to transactions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supports the data-independence assumption used to justify histories where each value is written at most once."}],"review_version":1}