Modelling and Verification of Starvation-Free Mutual Exclusion Algorithms based on Weak Semaphores
Franco Cicirelli, Libero Nigro
DOI: http://dx.doi.org/10.15439/2015F32
Citation: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 5, pages 773–779 (2015)
Abstract. This paper proposes an original framework for modelling and verification (M\&V) of starvation-free mutual exclusion algorithms based on weak semaphores, that are without a built-in waiting-process queue. The goal is to support the implementation of light-weight starvation-free semaphores useful in general concurrent systems like cyber physical systems. The M\&V approach depends on UPPAAL. First known weak semaphores are modelled. Then they are exploited for model checking classic algorithms. Known properties are retrieved but subtle new ones are discovered. As part of the developed approach, a new algorithm is proposed which uses two semaphores of the weakest type, N bits (N being the number of processes) and a counter. This algorithm too is proved to be correct.