How to Enforce and Verify Invariants in Weakly Consistent Databases
summary
Study shows how to preserve application invariants on weakly consistent, geo‑replicated stores by combining weak ops with targeted strong handling: uses Antidote SQL’s non‑blocking touch/visibility column to retain conflicting rows rather than blocking, and generalises that touch idea to disjunctions and implications. Mechanisms are encoded and mechanically checked with VeriFx plus TLA+/TLC (models explore up to ~10 operations; four models for disjunctions), some proofs abort and tests validate specific examples while full automatic verification remains future work.
AI-written summary · about
chapters (13)
- 0:00Maintaining invariants in local-first
- 2:49Locks fail for invariants
- 3:36Antidote SQL’s referential integrity
- 6:04Verifying invariant mechanisms
- 7:50Generalizing touching to disjunctions
- 10:18Conclusion and future directions
- 11:05Q&A: Application-specific vs general
- 12:29Q&A: Motivation for referential integrity
- 13:55Q&A: Model checking with operations
- 15:44Q&A: Formal proof tools in practice
- 16:28Q&A: Excluding operations for invariants
- 17:56Q&A: Transactions and CRDT semantics
- 20:01Q&A: Custom semantics for enforcement
related talks
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
25mSafe Replication through Bounded Concurrency Verification
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
24mArbitration-Free Consistency Is Available (and Vice Versa)
15mRethinking Safe Consistency in Distributed Object-Oriented Programming
41mProving linearizability of fault-tolerant register protocols: dependency graph approach
14mUniStore: A fault-tolerant marriage of causal and strong consistency