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 | |||
16:00 22mTalk | How to Enforce and Verify Invariants in Weakly Consistent Databases PLF Dina Borrego NOVA LINCS, FCT, Universidade NOVA de Lisboa, Carla Ferreira NOVA University Lisbon, Nuno Preguica NOVA LINCS, FCT, Universidade NOVA de Lisboa | ||
16:22 22mTalk | Local-First in Practice: Learnings of building a high-performance, local-first music app PLF Johannes Schickling None | ||
16:45 22mTalk | MVC, MVCC and Causal Trees PLF Victor Grishchenko Unaffiliated | ||
17:07 22mTalk | Mixed & Verified Consistency with Propel & ConOpY PLF Mirko Köhler TU Darmstadt, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen |