View topic and apply at https://jobs.inria.fr/public/classic/fr/offres/2018-00527
Advertising a postdoc position on “Just-Right Consistency for planet-scale storage;” see https://team.inria.fr/regal/job-offers/postdoctoral-position-just-right-consistency-for-planet-scale-storage/
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
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” impossibility result shows there is an inherent trade-off between fault tolerance, performance, and programmability. The first part of the talk will provide some general background on the consistency trade-off.
This has led to a split between databases designed for strong consistency and those designed for performance and availability; application designers must make an early decision of which consistency model to go with. Instead, we propose to fine-tune the database to provide the highest possible performance and availability that is appropriate for a given application. Our Just-Right Consistency approach leverages a novel static analysis (called CISE), which can prove whether a given distributed application maintains a given correctness invariant. In the second part of the talk, we will explain the intuition behind CISE, and how we use it to co-design the application and its consistency model, thereby minimising synchronisation to what is strictly necessary to ensure correctness
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 Enough: Reasoning about Consistency Choices in Distributed Systems.
A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, M. Shapiro.
Symp. on Principles of Programming Languages, Jan. 2016. St. Petersburg, Florida, USA
Read our new paper, to appear in Systor in May 2015 (Haifa, Israel): “Merging Semantics for Conflict Updates in Geo-Distributed File Systems” by Vinh Tao, Marc Shapiro, and Vianney Rancurel. http://lip6.fr/Marc.Shapiro/papers/geodistr-FS-Systor-2015.pdf