Modelling and Verification of Mutual Exclusion Algorithms

This paper proposes modelling and exhaustive verification of mutual exclusion algorithms using timed automata (TA) and the popular UPPAAL toolbox. The proposal allows to check all the properties of a mutual clusion algorithm also along the time dimension. Both the classic case of atomic read/write operations on memory cells and the non determinism of reading a memory cell during one or multiple write operations on it as it may occur in modern multi-port memories are considered. The approach is then applied to some algorithms proposed in the literature of which known properties are confirmed but also new ones are revealed.