Document Open Access Logo

Just Verification of Mutual Exclusion Algorithms

Authors Rob van Glabbeek , Bas Luttik , Myrthe S. C. Spronck

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.17.pdf
  • Filesize: 0.8 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Concurrency
  • Theory of computation → Verification by model checking
Keywords
  • Mutual exclusion
  • safe registers
  • regular registers
  • overlapping reads and writes
  • atomicity
  • safety
  • liveness
  • starvation freedom
  • justness
  • model checking
  • mCRL2

Metrics

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

Abstract

We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.

Cite As Get BibTex

Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck. Just Verification of Mutual Exclusion Algorithms. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.17

Author Details

Rob van Glabbeek
  • School of Informatics, University of Edinburgh, UK
  • School of Computer Science and Engineering, University of New South Wales, Sydney, Australia
Bas Luttik
  • Eindhoven University of Technology, The Netherlands
Myrthe S. C. Spronck
  • Eindhoven University of Technology, The Netherlands

Funding

  • van Glabbeek, Rob: Supported by Royal Society Wolfson Fellowship RSWF\R1\221008.

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Frédéric Haziza, and Lukáš Holík. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer, 18(5):495-516, 2016. URL: https://doi.org/10.1007/s10009-015-0406-x.
  2. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Handling parameterized systems with non-atomic global conditions. In Francesco Logozzo, Doron A. Peled, and Lenore D. Zuck, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI'08), volume 4905 of Lecture Notes in Computer Science, pages 22-36. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78163-9_7.
  3. K. Alagarsamy. Some myths about famous mutual exclusion algorithms. SIGACT News, 34(3):94-103, 2003. URL: https://doi.org/10.1145/945526.945527.
  4. James H. Anderson. A fine-grained solution to the mutual exclusion problem. Acta Informatica, 30(3):249-265, 1993. URL: https://doi.org/10.1007/BF01179373.
  5. Krzysztof R. Apt and Ernst-Rüdiger Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3(1):65-100, 1983. URL: https://doi.org/10.1016/0167-6423(83)90004-7.
  6. Alex A. Aravind. Yet another simple solution for the concurrent programming control problem. IEEE Transactions on Parallel and Distributed Systems, 22(6):1056-1063, 2011. URL: https://doi.org/10.1109/TPDS.2010.172.
  7. Alex A. Aravind and Wim H. Hesselink. Nonatomic dual bakery algorithm with bounded tokens. Acta Informatica, 48(2):67-96, 2011. URL: https://doi.org/10.1007/s00236-011-0132-0.
  8. Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, and Martin T. Vechev. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11), pages 487-498. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926442.
  9. Hagit Attiya and Jennifer L. Welch. Distributed computing - fundamentals, simulations, and advanced topics (2nd ed.). Wiley series on parallel and distributed computing. Wiley, 2004. Google Scholar
  10. Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A tutorial on uppaal. In Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, (SFM-RT'04), volume 3185 of Lecture Notes in Computer Science, pages 200-236. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30080-9_7.
  11. Mordechai Ben-Ari. Principles of the Spin model checker. Springer, 2008. URL: https://doi.org/10.1007/978-1-84628-770-1.
  12. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability in parameterized verification. SIGACT News, 47(2):53-64, 2016. URL: https://doi.org/10.1145/2951860.2951873.
  13. Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. Regular model checking. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 403-418. Springer, 2000. URL: https://doi.org/10.1007/10722167_31.
  14. 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.
  15. 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. URL: https://doi.org/10.1002/cpe.3659.
  16. 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 - improvements in expressivity and usability. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS'19), Part II, volume 11428 of Lecture Notes in Computer Science, pages 21-39. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_2.
  17. James E. Burns and Nancy A. Lynch. Bounds on shared memory for mutual exclusion. Information and Computation, 107(2):171-184, 1993. URL: https://doi.org/10.1006/inco.1993.1065.
  18. Flavio Corradini, Maria Rita Di Berardini, and Walter Vogler. Time and fairness in a process algebra with non-blocking reading. In Mogens Nielsen, Antonín Kucera, Peter Bro Miltersen, Catuscia Palamidessi, Petr Tuma, and Frank D. Valencia, editors, SOFSEM'09: Theory and Practice of Computer Science, 35th Conference on Current Trends in Theory and Practice of Computer Science, volume 5404 of Lecture Notes in Computer Science, pages 193-204. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-95891-8_20.
  19. Edsger W Dijkstra. Over de sequentialiteit van procesbeschrijvingen (ewd-35). Center for American History, University of Texas at Austin, 1962. URL: http://www.cs.utexas.edu/users/EWD/ewd00xx/EWD35.PDF.
  20. Edsger W. Dijkstra. Solution of a problem in concurrent programming control. Communications of the ACM, 8(9):569, 1965. URL: https://doi.org/10.1145/365559.365617.
  21. Victor Dyseryn, Rob J. van Glabbeek, and Peter Höfner. Analysing mutual exclusion using process algebra with signals. In Kirstin Peters and Simone Tini, editors, Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS'17), volume 255 of Electronic Proceedings in Theoretical Computer Science, pages 18-34, 2017. URL: https://doi.org/10.4204/EPTCS.255.2.
  22. Dana Fisman and Amir Pnueli. Beyond regular model checking. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science (FST&TCS'01), volume 2245 of Lecture Notes in Computer Science, pages 156-170. Springer, 2001. URL: https://doi.org/10.1007/3-540-45294-X_14.
  23. Rob J. van Glabbeek. Is speed-independent mutual exclusion implementable? (Invited talk). In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR'18), volume 118 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.3.
  24. Rob J. van Glabbeek. Justness - A completeness criterion for capturing liveness properties (extended abstract). In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures (FOSSACS'19), held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS'19), volume 11425 of Lecture Notes in Computer Science, pages 505-522. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_29.
  25. Rob J. van Glabbeek. Modelling mutual exclusion in a process algebra with time-outs. Information and Computation, 294:105079, 2023. URL: https://doi.org/10.1016/j.ic.2023.105079.
  26. Rob J. van Glabbeek and Daniele Gorla. On the notions of bounded bypass, and how to make any deadlock-free mutex protocol satisfy one of them, 2025. To appear. Google Scholar
  27. Rob J. van Glabbeek and Peter Höfner. Progress, justness, and fairness. ACM Computing Surveys, 52(4), 2019. URL: https://doi.org/10.1145/3329125.
  28. Rob J. van Glabbeek, Bas Luttik, and Myrthe S.C. Spronck. Just verification of mutual exclusion algorithms, 2025. Full version of the present paper. URL: https://doi.org/10.48550/arXiv.2507.13198.
  29. Jan Friso Groote and Jeroen J. A. Keiren. Tutorial: Designing distributed software in mCRL2. In Kirstin Peters and Tim A. C. Willemse, editors, 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, volume 12719, pages 226-243, Cham, 2021. Springer. URL: https://doi.org/10.1007/978-3-030-78089-0_15.
  30. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2014. URL: https://doi.org/10.7551/mitpress/9946.001.0001.
  31. Wim H. Hesselink. Mechanical verification of lamport’s bakery algorithm. Science of Computer Programming, 78(9):1622-1638, 2013. URL: https://doi.org/10.1016/j.scico.2013.03.003.
  32. Wim H. Hesselink. Mutual exclusion by four shared bits with not more than quadratic complexity. Science of Computer Programming, 102:57-75, 2015. URL: https://doi.org/10.1016/j.scico.2015.01.001.
  33. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, 1985. Google Scholar
  34. Joep L. W. Kessels. Arbitration without common modifiable variables. Acta Informatica, 17:135-141, 1982. URL: https://doi.org/10.1007/BF00288966.
  35. Donald E. Knuth. Additional comments on a problem in concurrent programming control. Communications of the ACM, 9(5):321-322, 1966. URL: https://doi.org/10.1145/355592.365595.
  36. Leslie Lamport. A new solution of dijkstra’s concurrent programming problem. Communications of the ACM, 17(8):453-455, 1974. URL: https://doi.org/10.1145/361082.361093.
  37. Leslie Lamport. The mutual exclusion problem: Part I - a theory of interprocess communication. J. ACM, 33(2):313-326, 1986. URL: https://doi.org/10.1145/5383.5384.
  38. Leslie Lamport. The mutual exclusion problem: Part II - statement and solutions. J. ACM, 33(2):327-348, 1986. URL: https://doi.org/10.1145/5383.5385.
  39. Leslie Lamport. On interprocess communication. Part I: basic formalism. Distributed Comput., 1(2):77-85, 1986. URL: https://doi.org/10.1007/BF01786227.
  40. Leslie Lamport. On interprocess communication. Part II: algorithms. Distributed Comput., 1(2):86-101, 1986. URL: https://doi.org/10.1007/BF01786228.
  41. Leslie Lamport. The TLA+ Hyperbook, 2015. chapter 7.8.4: The Real Bakery Algorithm. URL: http://lamport.azurewebsites.net/tla/hyperbook.html.
  42. Daniel Lehmann, Amir Pnueli, and Jonathan Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming (ICALP'81), volume 115 of Lecture Notes in Computer Science, pages 264-277. Springer, 1981. URL: https://doi.org/10.1007/3-540-10843-2_22.
  43. Radu Mateescu and Wendelin Serwe. Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Science of Computer Programming, 78(7):843-861, 2013. Special section on Formal Methods for Industrial Critical Systems (FMICS 2009 + FMICS 2010) & Special section on Object-Oriented Programming and Systems (OOPS 2009), a special track at the 24th ACM Symposium on Applied Computing. URL: https://doi.org/10.1016/j.scico.2012.01.003.
  44. Libero Nigro. Verifying mutual exclusion algorithms with non-atomic registers. Algorithms, 17(12), 2024. URL: https://doi.org/10.3390/a17120536.
  45. Libero Nigro, Franco Cicirelli, and Francesco Pupo. Modeling and analysis of Dekker-based mutual exclusion algorithms. Computers, 13(6):133, 2024. URL: https://doi.org/10.3390/computers13060133.
  46. Gary L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115-116, 1981. URL: https://doi.org/10.1016/0020-0190(81)90106-X.
  47. Gary L. Peterson. A new solution to lamport’s concurrent programming problem using small shared variables. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(1):56-65, 1983. URL: https://doi.org/10.1145/357195.357199.
  48. Michel Raynal. Concurrent Programming - Algorithms, Principles, and Foundations. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-32027-9.
  49. 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.
  50. Myrthe S. C. Spronck and Bas Luttik. Process-algebraic models of multi-writer multi-reader non-atomic registers. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory (CONCUR'23), volume 279 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Full version available at https://arxiv.org/abs/2307.05143. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.5.
  51. Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, justness and fairness in modal μ-calculus formulae. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory (CONCUR'24), volume 311 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.38.
  52. 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'88), pages 621-626. ACM, 1988. URL: https://doi.org/10.1145/55364.55425.
  53. 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, pages 110-117. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/JCIT.1990.128275.
  54. Gadi Taubenfeld. Synchronization algorithms and concurrent programming. Pearson Education, 2006. Google Scholar
  55. Lenore D. Zuck and Amir Pnueli. Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures, 30(3):139-169, 2004. URL: https://doi.org/10.1016/j.cl.2004.02.006.
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