Document Open Access Logo

Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers

Authors Myrthe S. C. Spronck , Bas Luttik

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.5.pdf
  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Author Details

Myrthe S. C. Spronck
  • Eindhoven University of Technology, The Netherlands
Bas Luttik
  • Eindhoven University of Technology, The Netherlands

Acknowledgements

We thank Rob van Glabbeek for insightful discussions on the topic of this paper.

Cite AsGet BibTex

Myrthe S. C. Spronck and Bas Luttik. Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.5

Abstract

We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions presented in the literature. We use our models to formally analyse by model checking to what extent several well-known mutual exclusion algorithms are robust for relaxed atomicity requirements. Our analyses refute correctness claims made about some of these algorithms in the literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Shared memory algorithms
  • Theory of computation → Verification by model checking
Keywords
  • mutual exclusion
  • model checking
  • non-atomic reads and writes
  • regular register

Metrics

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

Related Versions

Supplementary Materials

References

  1. K. Alagarsamy. Some myths about famous mutual exclusion algorithms. ACM SIGACT News, 34(3):94-103, 2003. Google Scholar
  2. James H. Anderson and Mohamed G. Gouda. Atomic semantics of nonatomic programs. Information Processing Letters, 28(2):99-103, 1988. Google Scholar
  3. Alex A. Aravind. Yet another simple solution for the concurrent programming control problem. IEEE Transactions on Parallel and Distributed Systems, 22(6):1056-1063, 2010. Google Scholar
  4. Hagit Attiya and Jennifer L. Welch. Distributed computing - Fundamentals, simulations, and advanced topics (2. ed.). Wiley series on parallel and distributed computing. Wiley, 2004. Google Scholar
  5. Mark Bouwman, Bas Luttik, and Tim A. C. Willemse. Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica, 57(3-5):551-590, 2020. URL: https://doi.org/10.1007/s00236-020-00371-w.
  6. Peter A. Buhr, David Dice, and Wim H. Hesselink. Dekker’s mutual exclusion algorithm made rw-safe. Concurrency and Computation: Practice and Experience, 28(1):144-165, 2016. Google Scholar
  7. Olav Bunte, Jan Friso Groote, Jeroen J.A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A.C. Willemse. The mCRL2 toolset for analysing concurrent systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 21-39. Springer, 2019. Google Scholar
  8. Franco Cicirelli and Libero Nigro. Modelling and verification of mutual exclusion algorithms. In 2016 IEEE/ACM 20th International Symposium on Distributed Simulation and Real Time Applications (DS-RT), pages 136-144. IEEE, 2016. Google Scholar
  9. Edsger W. Dijkstra. Solution of a problem in concurrent programming control. Communications of the ACM, 8(9):569, 1965. Google Scholar
  10. Rob van Glabbeek. Modelling mutual exclusion in a process algebra with time-outs. CoRR, abs/2106.12785, 2021. URL: https://arxiv.org/abs/2106.12785.
  11. Rob van Glabbeek and Peter Höfner. Progress, Justness, and Fairness. ACM Computing Surveys (CSUR), 52(4):1-38, 2019. Google Scholar
  12. Jan Friso Groote and Jeroen J. A. Keiren. Tutorial: designing distributed software in mCRL2. In Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, pages 226-243. Springer, 2021. Google Scholar
  13. Jan Friso Groote, Jeroen J. A. Keiren, Bas Luttik, Erik P. de Vink, and Tim A. C. Willemse. Modelling and analysing software in mCRL2. In Farhad Arbab and Sung-Shik Jongmans, editors, Formal Aspects of Component Software - 16th International Conference, FACS 2019, Amsterdam, The Netherlands, October 23-25, 2019, Proceedings, volume 12018 of Lecture Notes in Computer Science, pages 25-48. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-40914-2_2.
  14. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press Ltd., 2014. Google Scholar
  15. Wim H. Hesselink. Mechanical verification of Lamport’s bakery algorithm. Science of Computer Programming, 78(9):1622-1638, 2013. Google Scholar
  16. Wim H. Hesselink. Mutual exclusion by four shared bits with not more than quadratic complexity. Science of Computer Programming, 102:57-75, 2015. Google Scholar
  17. Donald E. Knuth. Additional comments on a problem in concurrent programming control. Communications of the ACM, 9(5):321-322, 1966. Google Scholar
  18. Leslie Lamport. A new solution of Dijkstra’s concurrent programming problem. Commun. ACM, 17(8):453-455, August 1974. URL: https://doi.org/10.1145/361082.361093.
  19. Leslie Lamport. The mutual exclusion problem: Part I - A theory of interprocess communication. J. ACM, 33(2):313-326, April 1986. URL: https://doi.org/10.1145/5383.5384.
  20. Leslie Lamport. The mutual exclusion problem: Part II - Statement and solutions. J. ACM, 33(2):327-348, April 1986. URL: https://doi.org/10.1145/5383.5385.
  21. Leslie Lamport. On interprocess communication. Part I: Basic formalism. Distributed Comput., 1(2):77-85, 1986. URL: https://doi.org/10.1007/BF01786227.
  22. Leslie Lamport. On interprocess communication. Part II: Algorithms. Distributed Comput., 1(2):86-101, 1986. URL: https://doi.org/10.1007/BF01786228.
  23. Leslie Lamport. The TLA+ Hyperbook, August 2015. Available at http://lamport.azurewebsites.net/tla/hyperbook.html, accessed on 26 April 2023, see Chapter 7.8.4.
  24. Zohar Manna, Anuchit Anuchitanukul, Nikolaj Bjorner, Anca Browne, and Edward Chang. STeP: The Stanford Temporal Prover. Technical report, Stanford University Department of Computer Science, 1994. Google Scholar
  25. Zohar Manna and Amir Pnueli. An exercise in the verification of multi-process programs. Beauty is our business: a birthday salute to Edsger W. Dijkstra, pages 289-301, 1990. Google Scholar
  26. Radu Mateescu and Wendelin Serwe. A study of shared-memory mutual exclusion protocols using CADP. In International Workshop on Formal Methods for Industrial Critical Systems, pages 180-197. Springer, 2010. Google Scholar
  27. Gary L. Peterson. Myths about the mutual exclusion problem. Inf. Process. Lett., 12(3):115-116, 1981. URL: https://doi.org/10.1016/0020-0190(81)90106-X.
  28. Michel Raynal. Concurrent Programming: Algorithms, Principles, and Foundations. Springer Publishing Company, Incorporated, 2013. URL: https://doi.org/10.1007/978-3-642-32027-9.
  29. Cheng Shao, Jennifer L. Welch, Evelyn Pierce, and Hyunyoung Lee. Multiwriter consistency conditions for shared memory registers. SIAM Journal on Computing, 40(1):28-62, 2011. URL: https://doi.org/10.1137/07071158X.
  30. Myrthe Spronck and Bas Luttik. Process-algebraic models of multi-writer multi-reader non-atomic registers, 2023. URL: https://arxiv.org/abs/2307.05143.
  31. Boleslaw K. Szymanski. A simple solution to Lamport’s concurrent programming problem with linear wait. In Jacques Lenfant, editor, Proceedings of the 2nd international conference on Supercomputing, ICS 1988, Saint Malo, France, July 4-8, 1988, pages 621-626. ACM, 1988. URL: https://doi.org/10.1145/55364.55425.
  32. Boleslaw K. Szymanski. Mutual exclusion revisited. In Joshua Maor and Abraham Peled, editors, Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, Jerusalem, October 22-25, 1990, pages 110-117. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/JCIT.1990.128275.
  33. Boleslaw K. Szymanski and Jose M. Vidal. Automatic verification of a class of symmetric parallel programs. In IFIP Congress (1), pages 571-576, 1994. 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 Imprint Privacy Contact