Formal verification of mutual exclusion algorithms in anonymous memory

i

This article has been updated. A Correction to this article was published on .

i

The Original Article was published on

i

The Original Article was published on

i

This article has been updated

i

This article was retracted on

i

This article has been updated

Abstract

This paper applied a formal method based on timed automata and the Uppaal toolbox to the specification and verification of mutual exclusion algorithms operating on anonymous memory. Anonymous memory is a challenging variation of shared memory where common variables (registers) do not have globally agreed-upon names. Instead, each process has its own view and naming for the shared registers. In addition, the cooperating/competing processes are supposed to be symmetric, that is, they execute the same code, and process identifiers are unknown. A recent proposal of Taubenfeld’s mutual exclusion algorithm with m ≥7 (m odd) shared anonymous registers was chosen as a concrete case study. Such an algorithm was informally studied by the authors together with the establishment of some possibility and impossibility results. This paper's first contribution was to confirm the correctness of the algorithm for N = 2 processes when atomic registers are used. The solution no longer holds for a smaller number of registers, e.g., m = 5, or when non-atomic registers are used. The paper also showed that for N > 2, the algorithm violates the mutual exclusion. To extend the use of the algorithm to N > 2 processes, this paper developed a novel organization where the basic solution for two processes is used as the arbitration unit in a binary, standard state-of-the-art tournament tree. Some timed variations of the model were considered, which permit the study of the algorithm under model checking and/or statistical model checking, for various values of the number N of processes.

Keywords

concurrency / anonymous shared memory / mutual exclusion / atomic/non-atomic registers / timed automata / Uppaal / model checking / statistical model checking

CHANGE HISTORY

A Correction to this paper has been published:
https://doi.org

The Retraction Note was updated to reflect reception of statements of disagreement from all authors.

This article has been retracted.Please see the Retraction Notice for more detail:
https://doi.org

References

[1] L. Lamport, The mutual exclusion problem: part I, In: Concurrency: the works of Leslie Lamport, New York: Association for Computing Machinery, 2019, 227-245. https://doi.org/10.1145/3335772.3335937

[2] L. Lamport, The mutual exclusion problem: part II, In: Concurrency: the works of Leslie Lamport, New York: Association for Computing Machinery, 2019, 247-276. https://doi.org/10.1145/3335772.3335938

[3] M. Raynal, D. Beeson, Algorithms for mutual exclusion problem, Cambridge: The MIT Press, 1986.

[4] M. Raynal, G. Taubenfeld, A visit to mutual exclusion in seven dates, Theor. Comput. Sci., 919 (2022), 47-65. https://doi.org/10.1016/j.tcs.2022.03.030

[5] M. Raynal, Concurrent programming: algorithms, principles, and foundations, Berlin: SpringerVerlag, 2013. https://doi.org/10.1007/978-3-642-32027-9

[6] E. Dijkstra, About the sequentiality of process descriptions, University of Texas at Austin, 1962.

[7] E. Dijkstra, Co-operating sequential processes, In: The origin of concurrent programming, New York: Springer, 1968, 65-138. https://doi.org/10.1007/978-1-4757-3472-0_2

[8] T. Dekker, History of Dekker’s algorithm for mutual exclusion, In: Tales of electrologica: computers, software and people, Cham: Springer Nature, 2022, 111-120. https://doi.org/10.1007/978-3-031-13033-5_6

[9] B. Szymanski, A simple solution to Lamport’s concurrent programming problem with linear wait, Proceedings of the 2nd international conference on Supercomputing, 1988, 621-626. https://doi.org/10.1145/55364.5542

[10] B. Szymanski, Mutual exclusion revisited, Proceedings of the 5th Jerusalem Conference on Information Technology, 1990, 110-117. https://doi.org/10.1109/JCIT.1990.128275

[11] L. Nigro, F. Cicirelli, F. Pupo, Modeling and analysis of Dekker-based mutual exclusion algorithms, Computers, 13 (2024), 133. https://doi.org/10.3390/computers13060133

[12] L. Nigro, F. Cicirelli, Property assessment of Peterson’s mutual exclusion algorithms, Appl. Comput. Intell., 4 (2024), 66-92. https://doi.org/10.3934/aci.2024005

[13] L. Lamport, Concurrent reading and writing, Commun. ACM, 20 (1977), 806-811. https://doi.org/10.1145/359863.359878

[14] P. Buhr, D. Dice, W. Hesselink, Highperformance Nthread software solutions for mutual exclusion, Concurr. Comp.-Pract. E., 27 (2015), 651-701. https://doi.org/10.1002/cpe.3263

[15] M. Spronck, B. Luttik, Process-algebraic models of multi-writer multi-reader non-atomic registers, Proceedings of the 34th International Conference on Concurrency Theory (CONCUR), 2023, 1-29.

[16] L. Nigro, Verifying mutual exclusion algorithms with non-atomic registers, Algorithms, 17 (2024), 536. https://doi.org/10.3390/a17120536

[17] L. Frenzel, Dual-port SRAM accelerates smart-phone development, Electronic Design, 2004. Available from: https://www.electronicdesign.com/technologies/industrial/boards/article/21774041/dual-port-sram-accelerates-smart-phone-development.

[18] Z. Wang, Q. Zuo, J. Li, An intelligent multi-port memory, Proceedings of International Symposium on Intelligent Information Technology Application Workshops, 2008, 251-254. https://doi.org/10.1109/IITA.Workshops.2008.231

[19] M. Raynal, G. Taubenfeld, Fully anonymous shared memory algorithms, arXiv: 1909.05576. https://doi.org/10.48550/arXiv.1909.05576

[20] G. Taubenfeld, Anonymous shared memory, J. ACM, 69 (2022), 24. https://doi.org/10.1145/3529752

[21] Z. Aghazadeh, D. Imbs, M. Raynal, G. Taubenfeld, P. Woelfel, Optimal memory-anonymous symmetric deadlock-free mutual exclusion, Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, 2019, 157-166. https://doi.org/10.1145/3293611.3331594

[22] G. Taubenfeld, Memory-anonymous starvation-free mutual exclusion: possibility and impossibility results, arXiv: 2309.11337. https://doi.org/10.48550/arXiv.2309.11337

[23] S. Rashid, G. Taubenfeld, Z. Bar-Joseph, The epigenetic consensus problem, In: Structural information and communication complexity, Cham: Springer, 2021, 146-163. https://doi.org/10.1007/978-3-030-79527-6_9

[24] W. Hesselink, Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos, Acta Inform., 50 (2013), 199-228. https://doi.org/10.1007/s00236-013-0178-2

[25] C. Baier, J. Katoen, Principles of model checking, Cambridge: MIT Press, 2008.

[26] J. Groote, J. Keiren, B. Luttik, E. de Vink, T. Willemse, Modelling and analyzing software in mCRL2, In: Formal aspects of component software, Cham: Springer, 2020, 25-48. https://doi.org/10.1007/978-3-030-40914-2_2

[27] R. Alur, D. Dill, A theory of timed automata, Theor. Comput. Sci., 126 (1994), 183-235. https://doi.org/10.1016/0304-3975(94)90010-8

[28] G. Behrmann, A. David, K. Larsen, A tutorial on UPPAAL, In: Formal methods for the design of real-time systems, Berlin: Springer, 2004, 200-236. https://doi.org/10.1007/978-3-540-30080-9_7

[29] E. Clarke, W. Klieber, M. Nováček, P. Zuliani, Model checking and the state explosion problem, In: Tools for practical software verification, Berlin: Springer, 2012, 1-30. https://doi.org/10.1007/978-3-642-35746-6_1

[30] Uppsala University, Aalborg University, Uppaal on-line, Uppaal tool, 2025. Available from: https://uppaal.org.

[31] Uppaal Tutorial, 1999. Available from: https://www.cis.upenn.edu/~lee/09cis480/lec-part-3-uppaal-inside.pdf.

[32] W. Zhou, Y. Zhao, Y. Zhang, Y. Wang, M. Yin, A comprehensive survey of UPPAAL-assisted formal modeling and verification, Softw. Pract. Exp., 55 (2025), 272-297.

[33] I. Grobelna, K. Gajewski, A. Karatkevich, Systematic review on the applications of Uppaal, Sensors, 25 (2025), 3484. https://doi.org/10.3390/s25113484

[34] G. Agha, K. Palmskog, A survey of statistical model checking, ACM Trans. Model. Comput. Simul., 28 (2018), 6. https://doi.org/10.1145/3158668

[35] A. David, K. Larsen, A. Legay, M. Mikučionis, D. Poulsen, Uppaal SMC tutorial, Int. J. Softw. Tools Technol. Transf., 17 (2015), 397-415. https://doi.org/10.1007/s10009-014-0361-y

[36] L. Nigro, F. Cicirelli, Formal modeling and verification of embedded real-time systems: an approach and practical tool based on Constraint Time Petri Nets, Mathematics, 12 (2024), 812. https://doi.org/10.3390/math12060812

[37] J. Kessels, Arbitration without common modifiable variables, Acta Inform., 17 (1982), 135-141. https://doi.org/10.1007/BF00288966

[38] W. Hesselink, Tournaments for mutual exclusion: verification and concurrent complexity, Form. Asp. Comp., 29 (2017), 833-852. https://doi.org/10.1007/s00165-016-0407-x

[39] H. Bowman, R. Gomez, L. Su, A tool for the syntactic detection of zeno-timelocks in timed automata, Electronic Notes in Theoretical Computer Science, 139 (2005), 25-47. https://doi.org/10.1016/j.entcs.2005.09.006

[40] L. Nigro, Parallel theatre: an actor framework in Java for high performance computing, Simul. Model. Pract. Th., 106 (2021), 102189. https://doi.org/10.1016/j.simpat.2020.102189