Document Open Access Logo

Concurrent Specifications Beyond Linearizability

Authors Éric Goubault, Jérémy Ledent, Samuel Mimram

PDF

File

Thumbnail PDF
PDF
LIPIcs.OPODIS.2018.28.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • concurrent specification
  • concurrent object
  • linearizability

Metrics

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

Abstract

With the advent of parallel architectures, distributed programs are used intensively and the question of how to formally specify the behaviors expected from such programs becomes crucial. A very general way to specify concurrent objects is to simply give the set of all the execution traces that we consider correct for the object. In many cases, one is only interested in studying a subclass of these concurrent specifications, and more convenient tools such as linearizability can be used to describe them.
In this paper, what we call a concurrent specification will be a set of execution traces that moreover satisfies a number of axioms. As we argue, these are actually the only concurrent specifications of interest: we prove that, in a reasonable computational model, every program satisfies all of our axioms. Restricting to this class of concurrent specifications allows us to formally relate our concurrent specifications with the ones obtained by linearizability, as well as its more recent variants (set- and interval-linearizability).

Cite As Get BibTex

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.OPODIS.2018.28

Author Details

Éric Goubault
  • École Polytechnique, Palaiseau, France
Jérémy Ledent
  • École Polytechnique, Palaiseau, France
Samuel Mimram
  • École Polytechnique, Palaiseau, France

References

  1. Elizabeth Borowsky and Eli Gafni. Immediate Atomic Snapshots and Fast Renaming. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Distributed Computing, PODC '93, pages 41-51. ACM, 1993. Google Scholar
  2. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Specifying Concurrent Problems: Beyond Linearizability and up to Tasks. In Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, Proceedings, pages 420-435, 2015. Google Scholar
  3. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238-252, 1977. Google Scholar
  4. Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theoretical Computer Science, 411(51):4379-4398, 2010. European Symposium on Programming 2009. Google Scholar
  5. Seth Gilbert and Wojciech Golab. Making Sense of Relativistic Distributed Systems. In Fabian Kuhn, editor, Distributed Computing, DISC 2015, volume 8784 of LNCS, pages 361-375. Springer Berlin Heidelberg, 2014. Google Scholar
  6. Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, pages 6:1-6:15, 2016. Google Scholar
  7. Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis. Modular Verification of Concurrency-Aware Linearizability. In Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, Proceedings, pages 371-387, 2015. Google Scholar
  8. Maurice Herlihy. Wait-free Synchronization. ACM Transactions on Programming Languages and Systems, 13(1):124-149, January 1991. Google Scholar
  9. Maurice Herlihy, Dmitry Kozlov, and Sergio Rajsbaum. Distributed Computing Through Combinatorial Topology. Morgan Kaufmann Publishers Inc., 2013. Google Scholar
  10. Maurice Herlihy and Jeannette M. Wing. Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems, 12(3):463-492, 1990. Google Scholar
  11. J Martin E Hyland and C-HL Ong. On full abstraction for PCF: I, II, and III. Information and computation, 163(2):285-408, 2000. Google Scholar
  12. L. Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computers, 28(9):690-691, 1979. Google Scholar
  13. Leslie Lamport. On interprocess communication. Distributed Computing, 1(2):77-85, 1986. Google Scholar
  14. Richard J Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717-721, 1975. Google Scholar
  15. Paul-André Melliès and Samuel Mimram. Asynchronous games: innocence without alternation. In International Conference on Concurrency Theory, pages 395-411. Springer, 2007. Google Scholar
  16. J. Misra. Axioms for memory access in asynchronous hardware systems. In Stephen D. Brookes, Andrew William Roscoe, and Glynn Winskel, editors, Seminar on Concurrency, pages 96-110. Springer Berlin Heidelberg, 1985. Google Scholar
  17. Gil Neiger. Set-Linearizability. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, page 396, 1994. Google Scholar
  18. Mogens Nielsen. Models for concurrency. In International Symposium on Mathematical Foundations of Computer Science, pages 43-46. Springer, 1991. Google Scholar
  19. Christos H. Papadimitriou. The Serializability of Concurrent Database Updates. Journal of the ACM, 26(4):631-653, 1979. Google Scholar
  20. M. Raynal, G. Thia-Kime, and M. Ahamad. From serializable to causal transactions for collaborative applications. In Proceedings of the 23rd EUROMICRO Conference, pages 314-321, 1997. Google Scholar
  21. G. Smith, K. Winter, and R. J. Colvin. A sound and complete definition of linearizability on weak memory models. ArXiv e-prints, February 2018. URL: http://arxiv.org/abs/1802.04954.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact