Sreeja S. Nair
Marc Shapiro
ABSTRACT
We study a proof methodology for verifying the safety of data invariants of highly-available distributed applications that replicate state. The proof is (1) modular: one can reason about each individual operation separately, and (2) sequential: one can reason about a distributed application as if it were sequential. We automate the methodology and illustrate the use of the tool with a representative example.
- C. Baquero, P. S. Almeida, A. Cunha, and C. Ferreira. Composition in state-based replicated data types. Bulletin of the EATCS, 123, 2017. URL http://eatcs.org/beatcs/index.php/beatcs/article/view/507.Google Scholar
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO'05, pages 364--387, Berlin, Heidelberg, 2006. Springer-Verlag. ISBN 3-540-36749-7, 978-3-540-36749-9. URL http://dx.doi.org/10.1007/11804192_17. Google ScholarDigital Library
- S. Burckhardt. Principles of Eventual Consistency, volume 1 of Foundations and Trends in Programming Languages. Now Publishers, Oct. 2014. URL http://research.microsoft.com/pubs/230852/final-printversion-10-5-14.pdf. Google ScholarDigital Library
- S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski. Replicated data types: Specification, verification, optimality. pages 271--284, San Diego, CA, USA, Jan. 2014. URL http://doi.acm.org/10.1145/2535838.2535848. Google ScholarDigital Library
- V. B. F. Gomes, M. Kleppmann, D. P. Mulligan, and A. R. Beresford. A framework for establishing strong eventual consistency for conflict-free replicated datatypes. Archive of Formal Proofs, 2017, 2017. URL https://www.isa-afp.org/entries/CRDT.shtml.Google Scholar
- A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, and M. Shapiro. 'Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems. pages 371--384, St. Petersburg, FL, USA, 2016. URL http://dx.doi.org/10.1145/2837614.2837625. Google ScholarDigital Library
- R. Jagadeesan and J. Riely. Eventual consistency for CRDTs. In A. Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 968--995. Springer, 2018. ISBN 978-3-319-89883-4. URL https://doi.org/10.1007/978-3-319-89884-1_34.Google Scholar
- G. Marcelino, V. Balegas, and C. Ferreira. Bringing hybrid consistency closer to programmers. PaPoC '17, pages 6:1--6:4, Belgrade, Serbia, 2017. ACM. URL http://doi.acm.org/10.1145/3064889.3064896. Google ScholarDigital Library
- S. Nair and M. Shapiro. Improving the "Correct Eventual Consistency" tool. Rapport de recherche RR-9191, Paris, France, July 2018. URL https://hal.inria.fr/hal-01832888.Google Scholar
- M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, and M. Shapiro. The CISE tool: Proving weakly-consistent applications correct. EuroSys 2016 workshops, London, UK, Apr. 2016. URL http://dx.doi.org/10.1145/2911151.2911160. Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271--307, 2007. URL https://doi.org/10.1016/j.tcs.2006.12.035. Google ScholarDigital Library
- M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Technical Report 7506, Jan. 2011.Google ScholarDigital Library
- M. Shapiro, N. Preguiça, C. Baquero, and M. Zawirski. Conflict-free replicated data types. volume 6976, pages 386--400, Grenoble, France, Oct. 2011. URL https://doi.org/10.1007/978-3-642-24550-3_29. Google ScholarDigital Library
- K. Sivaramakrishnan, G. Kaki, and S. Jagannathan. Declarative programming over eventually consistent data stores. PLDI '15, pages 413--424, Portland, OR, USA, 2015. URL http://doi.acm.org/10.1145/2737924.2737981. Google ScholarDigital Library
- Invariant Safety for Distributed Applications
Recommendations
Proving the Safety of Highly-Available Distributed Objects
Programming Languages and SystemsAbstractTo provide high availability in distributed systems, object replicas allow concurrent updates. Although replicas eventually converge, they may diverge temporarily, for instance when the network fails. This makes it difficult for the developer to ...
Another Look at LTL Model Checking
We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a {\em symbolic} LTL model checker that appears to be quite efficient in practice. In particular, we ...
Automatic Verification of Fault-Tolerant Register Emulations
The design and verification of fault-tolerant distributed algorithms is a complicated task. Usually, the proof of correctness is done manually, and thus depends on the skill of the prover. Using automated verification methods, such as model checking, ...
Comments