[PLF23] How to Enforce and Verify Invariants in Weakly Consistent Databases

[PLF23] How to Enforce and Verify Invariants in Weakly Consistent Databases

Dina Borrego, Carla Ferreira, Nuno Preguica

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.