Formal specification and analysis of asynchronous mutual exclusion algorithms

• Wenya An

We specify and analyse of two very well known asynchronous mutual exclusion algorithms, namely the Dijkstra's Mutex algorithm and the Bakery algorithm due to Lamport, on the light of the thesis for concurrent algorithms and the new formal notion of concurrent run recently introduced [?]. Our formal specification as multi-agent ASMs with concurrent runs resulted in a completely rigorous presentations which we believe meets the criteria to be considered both reasonably short and intuitively understandable. In the process, we made all the usual assumptions in the pseudo-code versions of these algorithms explicit. We discovered that in order to be able to specify the intended behaviour, it is necessary to incorporate the notion of partial update as studied in the synchronous parallel setting [?, ?, ?]. Otherwise, the concurrent ASMs of the respective algorithms have the potential to produce concurrent runs which end with an inconsistent set of updates. This unintended behaviour of the algorithms is probably due to the fact they were designed a long time ago, when actual concurrent systems which allow for such problematic type of concurrent runs did not existed in practice. In fact and probably due to the same reason, both algorithms work under the assumption that the set of processes if fixed, i.e., it does not change during the run of the algorithm. Nowadays, this assumption is not common in practice, where the set of processes in concurrent systems is usually considered dynamic. We therefore propose an update of both algorithms so that they can cope with dynamic sets of processes where new processes can be added to and old process deleted from the set of processes which can request access to the critical resource manage by the algorithm. It is noteworthy the fact that proposed modified versions of Dijkstra's Mutex algorithm and the Bakery algorithm also make use of the concept of partial updates and satisfy exactly the same formal properties as the original ones.