The mutual exclusion problem is one of the cornerstones of distributed computing. It deals with parallel processes that need to perform tasks that may not interfere with each other, such as updating records in a shared database. The sensitive parts of each process' code are collected in so-called critical sections, and the task of a mutual exclusion protocol is to make sure that two or more of the processes can never be in their critical section at the same time. Many mutual exclusion protocols have been proposed since this problem was posed in 1965, and it is generally believed that thereby the mutual exclusion problem has been solved.
Yet, whether a mutual exclusion protocol operates correctly depends on the hardware on which it will be running. Today I will formulate 6 alternative assumptions that one could make on the way the hardware implements shared registers, and check to what extent classical solutions to the mutual exclusion problem actually yield correct mutual exclusion protocols under each of these assumptions. I report both on automated verification and on theoretical work. Regarding the latter, I will show that under those assumptions that were made in the original paper posing the mutual exclusion problem (namely, speed independence and atomicity) no correct mutual exclusion protocol is possible. This observation contradicts 50 years of research on mutual exclusion. I also show how mutual exclusion can be achieved when dropping any of these assumptions.
Regarding the automated verification, we employed a model checker to exhaustively analyse the state space of more than a dozen of the most popular mutual exclusion protocols, and automatically verify their correctness under each of the six hardware assumptions discussed. It turns out that several well-known algorithms do not live up to their promises, and have subtle flaws, that never showed up during their behavioural analysis, yet were found by our model checker.
28/05/2025
Location: Aula Magna (Palazzina C) - Viale Regina Elena 295
Date and time:
Wednesday, May 28, 12:15-13:15
Photo
Rob van Glabbeek has been active as a research scientist in the field of Formal Methods since 1984, of which five years were spent at CWI in Amsterdam and twelve years at Stanford University. In addition he has had visiting appointments at the Technical University of Munich, GMD in Bonn, INRIA in Sophia Antipolis, the University of Edinburgh, the University of Cambridge, and l’Université de la Méditerranée in Marseilles. He has also been active as a consultant for Ricoh Innovations, California, in the area of workflow modelling. From 2003 to 2016 he worked for NICTA, Sydney, Australia, and from July 2016 until October 2021 he was Chief Research Scientist at Data61, CSIRO in Sydney.
Currently he is a Royal Society Wolfson Fellow at the School of Informatics, University of Edinburgh, Scotland. He also is a Adjunct Professor at the School of Computer Science and Engineering at the University of New South Wales, and a Research Affiliate at the Concurrency Group in the Computer Science Department of Stanford University.