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

Featured


FAQ on CRDTs
SyncFree Software Repository  

SyncFree Technology
  • Bounded Counters: maintaining numeric invariants with high availability
  • Commander: Bug-Finding for Programs Running on Weakly Consistent Platforms
  • Verifico: CRDT-App Verification Framework for Isabelle

            

 This project is funded by the European Union, 7th Research Framework Programme, ICT call 10, grant agreement n°609551. 

Contact (Project Coordinator)

MARC dot SHAPIRO atsign ACM dot ORG