How to Enforce and Verify Invariants in Weakly Consistent Databases
Weak consistency is fundamental to achieving high availability and low latency in geo-replicated systems, allowing the execution of operations without coordination. However, these consistency models may jeopardise the correctness of applications, leading to broken invariants. To circumvent this problem, some systems combine strong consistency with weak consistency.
This paper presents a study on the maintenance of application invariants in weakly consistent databases. For each class of invariants identified, we explain how to combine strong and weak consistency to preserve invariants. We also explain how we verified the correctness of some of the proposed mechanisms using a verification language called VeriFx.
To encourage the verification of real applications, we envision a fully automatic verification tool based on the methodology we used for verifying applications in VeriFx.
Tue 24 OctDisplayed time zone: Lisbon change
16:00 - 17:30
|How to Enforce and Verify Invariants in Weakly Consistent Databases
|Local-First in Practice: Learnings of building a high-performance, local-first music app
Johannes Schickling None
|MVC, MVCC and Causal Trees
Victor Grishchenko Unaffiliated
|Mixed & Verified Consistency with Propel & ConOpY