Formally verifying the properties of a distributed file system, with Availability under Partition properties. The file system consists of interdependent CRDT objects under a strong safety invariant (tree shape). Paper by Mahsa Najafzadeh, Marc Shapiro and Patrick Eugster, published at VMCAI 2018. The paper is available here.
In the PaPoC 2016 programme: Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira and Marc Shapiro. The CISE Tool: Proving Weakly-Consistent Applications Correct Alejandro Z. Tomsic, Tyler Crain and Marc Shapiro. PhysiCS: efficient consistent snapshots for scalable snapshot isolation Marek Zawirski, Carlos Baquero, Annette Bieniusa, Nuno Preguiça and Marc Shapiro. Eventually Consistent Register Revisited
https://www.liglab.fr/evenements/keynote-speeches/marc-shapiro-just-right-consistency Consistency —ensuring that data items distributed over remote computers agree with each other— is a fundamental issue of distributed computing. No single consistency model is appropriate for all uses: strong consistency requires lots of synchronisation, which has availability and performance issues; weak consistency performs and scales better but is error-prone. Indeed, the famous “CAP” …
Asynchronous replication is available and fast, but what about consistency? We propose a logic for showing that such a program maintains its invariants. We implemented the rule in a static analysis tool and ran a few interesting examples. See the video of the tool and the paper to appear at POPL 2016: ‘Cause I’m Strong …