Document Open Access Logo

Consistency Models with Global Operation Sequencing and their Composition

Authors Alexey Gotsman, Sebastian Burckhardt

PDF
Thumbnail PDF

File

LIPIcs.DISC.2017.23.pdf
  • Filesize: 0.67 MB
  • 16 pages

Document Identifiers

Author Details

Alexey Gotsman
Sebastian Burckhardt

Cite As Get BibTex

Alexey Gotsman and Sebastian Burckhardt. Consistency Models with Global Operation Sequencing and their Composition. In 31st International Symposium on Distributed Computing (DISC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 91, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.DISC.2017.23

Abstract

Modern distributed systems often achieve availability and scalability by providing consistency guarantees about the data they manage weaker than linearizability. We consider a class of such consistency models that, despite this weakening, guarantee that clients eventually agree on a global sequence of operations, while seeing a subsequence of this final sequence at any given point of time. Examples of such models include the classical Total Store Order (TSO) and recently proposed dual TSO, Global Sequence Protocol (GSP) and Ordered Sequential Consistency.

We define a unified model, called Global Sequence Consistency (GSC), that has the above models as its special cases, and investigate its key properties. First, we propose a condition under which multiple objects each satisfying GSC can be composed so that the whole set of objects satisfies GSC. Second, we prove an interesting relationship between special cases of GSC - GSP, TSO and dual TSO: we show that clients that do not communicate out-of-band cannot tell the difference between these models. To obtain these results, we propose a novel axiomatic specification of GSC and prove its equivalence to the operational definition of the model.

Subject Classification

Keywords
  • Consistency conditions
  • Weak memory models
  • Compositionality

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Microsoft TouchDevelop. https://www.touchdevelop.com/. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. The benefits of duality in verifying concurrent programs under TSO. In CONCUR: International Conference on Concurrency Theory, 2016. Google Scholar
  3. Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky. A programming language perspective on transactional memory consistency. In PODC: Symposium on Principles of Distributed Computing, 2013. Google Scholar
  4. Giovanni Bernardi and Alexey Gotsman. Robustness against consistency models with atomic visibility. In CONCUR: International Conference on Concurrency Theory, 2016. Google Scholar
  5. Phil Bernstein, Sebastian Burckhardt, Sergey Bykov, Natacha Crooks, Jose Faleiro, Gabriel Kliot, Alok Kumbhare, Muntasir Raihan Rahman, Vivek Shah, Adriana Szekeres, and Jorgen Thelin. Geo-distribution of actor-based services. Technical Report MSR-TR-2017-3, Microsoft Research, 2017. Google Scholar
  6. Philip A. Bernstein, Sergey Bykov, Alan Geller, Gabriel Kliot, and Jorgen Thelin. Orleans: Distributed virtual actors for programmability and scalability. Technical Report MSR-TR-2014-41, Microsoft Research, 2014. Google Scholar
  7. Hans-J. Boehm and Sarita V. Adve. Foundations of the C++ concurrency memory model. In PLDI: Conference on Programming Language Design and Implementation, 2008. Google Scholar
  8. Sebastian Burckhardt. Principles of Eventual Consistency. now publishers, 2014. Google Scholar
  9. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: specification, verification, optimality. In POPL: Symposium on Principles of Programming Languages, 2014. Google Scholar
  10. Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global sequence protocol: A robust abstraction for replicated shared state. In ECOOP: European Conference on Object-Oriented Programming, 2015. Google Scholar
  11. Xavier Défago, André Schiper, and Péter Urbán. Total order broadcast and multicast algorithms: Taxonomy and survey. ACM Comput. Surv., 36(4), 2004. Google Scholar
  12. Ivana Filipovic, Peter O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52), 2010. Google Scholar
  13. Peter C. Fishburn. Intransitive indifference with unequal indifference intervals. Journal of Mathematical Psychology, 7, 1970. Google Scholar
  14. Seth Gilbert and Nancy Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2), 2002. Google Scholar
  15. Alexey Gotsman and Sebastian Burckhardt. Consistency models with global operation sequencing and their composition (extended version). arXiv CoRR, 1707.09242, 2017. URL: http://arxiv.org/abs/1701.05463.
  16. Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3), 1990. Google Scholar
  17. Lisa Higham and Jalal Kawash. Memory consistency and process coordination for sparc multiprocessors. In HiPC: International Conference on High Performance Computing, 2000. Google Scholar
  18. Patrick Hunt, Mahadev Konar, Flavio Paiva Junqueira, and Benjamin Reed. ZooKeeper: Wait-free coordination for internet-scale systems. In USENIX ATC: USENIX Annual Technical Conference, 2010. Google Scholar
  19. ISO/IEC Standard. Programming languages - C++, 14882:2011, 2011. Google Scholar
  20. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., 28(9), 1979. Google Scholar
  21. Kfir Lev-Ari, Edward Bortnikov, Idit Keidar, and Alexander Shraer. Modular composition of coordination services. In USENIX ATC: USENIX Annual Technical Conference, 2016. Google Scholar
  22. Kfir Lev-Ari, Edward Bortnikov, Idit Keidar, and Alexander Shraer. Composing ordered sequential consistency. Information Processing Letters, 123, 2017. Google Scholar
  23. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs: International Conference on Theorem Proving in Higher Order Logics, 2009. Google Scholar
  24. S. Park and D. L. Dill. An executable specification, analyzer and verifier for RMO. In SPAA'95: Symposium on Parallel Algorithms and Architectures, 1995. Google Scholar
  25. Matthieu Perrin, Matoula Petrolia, Achour Mostéfaoui, and Claude Jard. On composition and implementation of sequential consistency. In DISC: International Symposium on Distributed Computing, 2016. Google Scholar
  26. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22, 1990. Google Scholar
  27. Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2), 1988. Google Scholar
  28. Daniel J. Sorin, Mark D. Hill, and David A. Wood. A Primer on Memory Consistency and Cache Coherence. Morgan &Claypool Publishers, 1st edition, 2011. Google Scholar
  29. Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent W. Welch. Session guarantees for weakly consistent replicated data. In PDIS: Conference on Parallel and Distributed Information Systems, 1994. Google Scholar
  30. Roman Vitenberg and Roy Friedman. On the locality of consistency conditions. In DISC: International Symposium on Distributed Computing, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact