Just-Right Consistency, or How to tailor consistency to application requirements
Just-Right Consistency (a.k.a. Explicit Consistency) is a novel approach to consistency that tailors the amount of synchronisation to the application requirements. An application whose invariants require no synchronisation is maximally concurrent and available. Even to enforce stronger invariants doesn't necessarily require to synchronise every operation. The CISE analysis ensures that those operations that are critical for maintaining the application's correctness are synchronised. Furthermore, synchronisation can often by optimised by “reservation” techniques (delaying and batching synchronisation). We are developing a new tool that guarantees that invariants are maintained without coordination, by using only CRDT rules to merge concurrent updates, when this is possible.
The CISE logic and tool
CISE is a sound logic that proves that a given distributed program maintains a given application invariant of interest under a given consistency model. Our SMT-based tool automates the CISE analysis. We have successfully verified several example applications using it. If the application does not maintain the invariant, the tool provides a counter-example, which helps the developer diagnose the problem. With this information, the developer can fix the problem, either by weakening application effects or invariants, and/or by adding concurrency control that disallows the incorrect concurrency.
Example
The developer writes the properties of her program as Java annotations. Below is a code sample for bank application with two operations deposit and debit. The invariant is to keep the balance greater or equal to zero.
Further reading
- The basic idea is in a paper by Balegas et al. presented at EuroSys 2015: Putting Consistency back into Eventual Consistency. V. Balegas et al., EuroSys, Apr. 2015.
- For a short, intuitive explanation of the CISE logic and tool, see the short paper: The CISE Tool: Proving Weakly-Consistent Applications Correct, Najafzadeh et al., PaPoC, April 2016.
- The CISE logic is formalised and proved in a paper by Gotsman et al., POPL 2016. Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems. A. Gotsman et al., POPL, Jan. 2016
- Download the CISE tool:
Software Repository
