SCCP 2026 — Accepted Paper Summaries
1st Symposium on Consistency Checking Principles (co-located with VLDB 2026), September 4, 2026. Summaries are based on the final PDFs of all 10 papers.
Note: These summaries were generated by an AI model (Fable 5) and lightly reviewed. They are provided as a convenience only; please consult the papers themselves for authoritative descriptions of the work.
Session 1: Checking Reality
1. Extending Elle for Transaction Workloads with Duplicate Values
Zhiheng Cai (Tsinghua), Si Liu (The Chinese University of Hong Kong, Shenzhen), Hengfeng Wei (Hunan), Yuxing Chen (Renmin)
Elle, the widely adopted black-box isolation validator behind Jepsen, crucially relies on the unique-value assumption: every value read can be deterministically matched to a single write. With duplicate values — which arise naturally in real workloads (e.g., via retries) and are precisely where many isolation bugs manifest — a read list like [1,2,1] no longer identifies which append produced each element, breaking WR and WW dependency inference; the paper further shows that a natural transaction-level “choice set” fix is unsound, admitting unfaithful acyclic resolutions and even masking non-serializable histories. The solution shifts to operation-level reasoning via list unfolding: each read list is unfolded into its successive prefixes linked by a new append order, so each list extension is attributed to a specific source append, with an append-order condition and acyclicity required at both the operation and transaction levels — proven sound and complete. The SMT-based prototype Elle⁺ (~3K lines of C++, using hyper-polygraphs) rediscovered two serializability bugs in MySQL 8.0 and MariaDB 11.5 that only trigger with duplicate values, and verifies histories of 10K transactions / 80K operations in under 100s even when every key receives duplicate appends.
Significance: Removing Elle’s unique-value assumption — with a soundness-and-completeness guarantee rather than a heuristic — closes the single biggest gap between what practical black-box checkers can consume and how real applications actually write data, unlocking a class of duplicate-value-only bugs that existing validators structurally cannot see.
2. Efficient Black-Box Serializability Checking in the Presence of Range Predicates
Qikang Liu (Simon Fraser), Si Liu (The Chinese University of Hong Kong, Shenzhen), Yuepeng Wang (Simon Fraser)
Black-box serializability checkers largely target key-value histories where read-from dependencies are explicit; range predicates break this, since a predicate read or range update touches an unknown, state-dependent set of rows. The paper reduces checking to finding an accepting run in a deterministic finite automaton over candidate serial orders, made tractable by two ideas: merging transaction prefixes that reach identical database states, and pruning prefixes whose implied states contradict observed query results. Their tool, SerCheck, outperforms the state-of-the-art checkConsistency with a widening gap as workloads grow, verifying 106 serializable histories, detecting 298 violations, and reproducing 16 known serializability bugs in real databases.
Significance: Predicate/range operations are where SQL databases actually get used and where most checkers give up, so an efficient state-based technique here moves black-box checking meaningfully closer to production SQL workloads.
3. Specifying and Analyzing Transactional Consistency Models with Predicates (Extended Abstract)
Hengfeng Wei (Hunan), Si Liu (The Chinese University of Hong Kong, Shenzhen), Yuxing Chen (Renmin)
Formal treatments of transactional consistency mostly ignore predicate operations, leaving predicate anomalies (like the subtleties around phantoms) defined informally and inconsistently across the literature. The paper extends execution models with predicate reads (classified as internal or external), introduces an ExtPred axiom governing which writes must “explain” an external predicate read, and adds new Pred-WR and Pred-RW dependency-edge types. On this foundation it proves the first characterization theorems for predicate-based histories: serializability iff the dependency graph is acyclic, and snapshot isolation iff every cycle contains two adjacent anti-dependency edges — carefully handling “changing matches,” where an overwrite alters whether a row satisfies a predicate.
Significance: This supplies the missing theoretical bedrock — Adya-style graph characterizations extended to predicates — that both checkers (like paper #2) and protocol verifiers need before they can make rigorous claims about SQL-level isolation.
Session 2: Who Broke Serializability and Snapshot Isolation?
4. Diagnosing the Structure of Strict-Serializability Violations Across Spanner-like Read-Only Transaction Protocols
Sejong Kim, Yon Dohn Chung (Korea University)
Spanner-style systems can boost read-only transaction performance by letting reads skip waiting on prepared conflicting writes, at the cost of weakening strict serializability — but the structure of the resulting anomalies is poorly understood. The authors build a controlled family of protocols targeting progressively weaker models (RSS, POS, SER) and dissect execution traces via dependency graphs, uncovering a puzzle: POS/SER produce 181–359× more cycle-forming skip pairs than RSS despite only 1.5–2× more skip-induced anti-dependencies. The explanation is “anti-regular anti-dependencies” (ARA) — reads skipping writes that already completed in real time, driven by cross-region visibility lag — which both form violation cycles directly and provide return paths that let other skips become cycle-forming.
Significance: By pinpointing ARA pairs as the mechanism that amplifies anomalies, the paper turns “weaker reads are riskier” from folklore into an actionable design principle — preserving regularity selectively could buy back performance without opening the ARA floodgate.
5. Verified Key-Value Stores Satisfying Snapshot Isolation (Extended Abstract)
Arnaud Daby-Seesaram, Léon Ducruet, Lars Birkedal, Amin Timany (Aarhus)
Testing finds isolation bugs but cannot rule them out, and prior formally verified stores relied on inefficient global-lock implementations. Using the Iris separation-logic framework, the authors build SIrIS, an in-memory key-value store based on a lock-free variant of Reed’s multi-version concurrency control with a verified garbage collector, and prove it satisfies snapshot isolation via logically atomic triples that capture linearization points. The store performs competitively (~1M transactions/second), and the same logic lets client code be verified against the SI specification; liveness (e.g., deadlock-freedom) remains future work.
Significance: This is a rare demonstration that machine-checked isolation guarantees and competitive lock-free performance are not mutually exclusive, pointing toward verification — not just checking — as a practical endgame for consistency assurance.
Session 3: Many Models, One Theory
6. Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
Qiuhuan Xiong (Nanjing), Si Liu (The Chinese University of Hong Kong, Shenzhen), Hengfeng Wei (Hunan), Yuxing Chen (Renmin), Jidong Ge (Nanjing)
Production databases (Oracle, MySQL, PostgreSQL, CockroachDB, TiDB) assign isolation levels per transaction, yet whether concurrency control protocols correctly enforce guarantees under such mixed settings has remained largely unanswered — mixing subtly complex level semantics, with database documentation leaving the combination underspecified. The paper develops MixIso, a formal semantic framework extending the Cerone-style (VIS, AR) axiomatic approach with per-transaction visibility: each transaction’s observed effects must conform to the axioms of its own assigned level (RA, CC, PC, PSI, SI, or SER), preserving “isolation autonomy” — a transaction’s guarantee depends only on its own level, so stronger transactions cannot impose visibility requirements on weaker ones. A protocol conforms if every history it produces admits a consistent abstract execution; MixIso is shown to generalize the homogeneous framework and to be equivalent to Bouajjani et al.’s recent formalization on their common levels. Two case studies demonstrate applicability: a conformance proof for the SI–S2PL protocol combining SI and serializability (used in Microsoft SQL Server and Oracle Berkeley DB), and a new protocol mixing PC, SI, and SER — via a construction that extracts VIS from a case analysis on each transaction’s level and AR from commit timestamps.
Significance: Mixed isolation levels are the norm in deployed systems but a blind spot in the theory, and MixIso supplies the first general semantic framework for proving — not just testing — that real protocols deliver the per-transaction guarantees they advertise, with a clear path to mixed-level black-box checking and robustness analysis.
7. Polygraph: From Transaction Isolation Guarantees to Isolation Verification
Jian Zhang, Cheng Tan (Northeastern)
Existing isolation formalisms were built for definition, not checking: they assume internal metadata clients cannot see, require expensive state exploration, or need a bespoke algorithm per isolation level. Polygraph is a theoretical framework designed for verification from the start, modeling executions as graphs with known dependencies, “superpositions” (unresolved orderings), and implications, and characterizing each isolation level by which edge types and implication rules are enabled — correctness reduces to acyclicity of canonical augmented dependency graphs. The framework is proven equivalent to prior formalizations (e.g., Adya), and an implementation of six isolation-level checkers shares 98% of its 14K lines, with each level needing only ~240–285 lines, validated on PostgreSQL, MySQL, and TiKV traces including range queries and non-unique values.
Significance: Polygraph reframes isolation theory around the needs of checkers rather than definitions, and the 98%-shared implementation is compelling evidence that one unified formalism can replace today’s fragmented one-checker-per-level landscape.
8. Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions
Shabnam Ghasemirad (ETH Zurich), Christoph Sprenger (ETH Zurich), Si Liu (The Chinese University of Hong Kong, Shenzhen), David Basin (ETH Zurich)
In the authors’ VerIso framework (VLDB 2025), proving that a protocol satisfies an isolation level means refining an abstract centralized model (CIL) — but the abstraction gap makes these proofs labor-intensive, and refinement alone is sometimes insufficient, forcing ad-hoc, per-protocol Lipton-style reduction arguments. This paper, fully formalized in Isabelle/HOL, makes three moves: a generic reduction framework (parameterized on an event system, a dependency relation, and a desired “good” event order) that proves any execution can be commuted into an order-consistent one; a dichotomy theorem over seven isolation levels — levels at or above update atomicity (UA, PSI, SI, SER, SSER) can be verified by direct refinement alone, while weaker levels (RA, CC) inherently require reduction because write conflicts cause “inverted commits” whose timestamp order diverges from execution order; and a hierarchy of intermediate models (TXM, TXM_UA↑, TXM_CC↓, and a distributed 2PC-shaped DTXM) in which the reduction is performed once and for all at a high abstraction level. Verifying a new protocol then collapses to a single refinement of DTXM; ongoing case studies re-verify Eiger-PORT+ (CC) and ROLA (UA) to validate both ends of the lattice.
Significance: By factoring the hardest proof step out of per-protocol efforts and explaining why weak levels are harder to verify (the write-conflict/commit-inversion dichotomy), this work makes mechanized isolation verification scale beyond one-off heroic proofs — the deductive counterpart to Polygraph’s unification on the checking side.
Session 4: Consistency Goes Agentic
9. Notified Serializability: A Consistency Model for Concurrent LLM Agents
Hongtao Lyu, Dingyan Zhang, Mingyu Wu, Xingda Wei, Haibo Chen (SJTU)
Classical concurrency control fits LLM agents badly: inference takes minutes so lock waits and aborts are ruinously expensive, agents read broadly for context so spurious overlaps trigger conflicts, and live targets like Kubernetes clusters cannot fork state or buffer writes. The paper proposes notified serializability, where the runtime reports conflicts and agents decide whether to repair affected operations, realized in MTPO (Monotonic Trajectory Pre-Order): agents get pre-assigned ranks, reads are filtered to rank-appropriate values, writes apply immediately, and registered inverse functions provide saga-style compensation for out-of-order writes. On ten contended two-agent workloads MTPO achieves 1.4× speedup at 1.15× token cost with correctness within 5% of serial execution, where 2PL and OCC preserve correctness only by giving up nearly all concurrency.
Significance: This is one of the first serious attempts to design — rather than merely borrow — a consistency model for the economics of LLM agents, opening a new design space where the “transaction” can participate in its own conflict resolution.
10. Beyond Pass Rate: A Hierarchy of Behavioral Consistency for LLM Agents
Tian Lu, Zikai Wang, Cheng Tan (Northeastern)
Agent evaluation fixates on pass rate, which says nothing about whether an agent behaves the same way across runs — and the gap is large: tasks with 80%+ pass rates see two random runs agree on their state-modifying action sequence only ~39% of the time. The paper proposes a five-level hierarchy of behavioral consistency — token-identical, action-equivalent, effect-equivalent, state-equivalent, and outcome-equivalent — with automated trajectory classifiers, evaluated over 17 models on 10 system-administration tasks (8,000+ runs). Findings: consistency and correctness are orthogonal; effect-equivalence consistency spans only 0.18–0.57 across models; larger dense models are more consistent while MoE models underperform at equal pass rates; higher temperature monotonically hurts consistency; and a task’s read/write structure predicts consistency better than pass rate does.
Significance: By giving behavioral repeatability a formal hierarchy and measurement methodology, the paper imports the consistency-model mindset into agent evaluation — a prerequisite for anyone who wants to deploy agents on real systems where predictability matters as much as success.