In this paper we study the liveness of several MUTEX solutions by representing them as processes in PAFAS s, a CCS-like process algebra with a specific operator for modelling non-blocking reading behaviours. Verification is carried out using the tool FASE, exploiting a correspondence between violations of the liveness property and a special kind of cycles (called catastrophic cycles) in some transition system. We also compare our approach with others in the literature. The aim of this paper is twofold: on the one hand, we want to demonstrate the applicability of FASE to some concrete, meaningful examples; on the other hand, we want to study the impact of introducing non-blocking behaviours in modelling concurrent systems.
Cite
@article{arxiv.1106.1231,
title = {Automated Analysis of MUTEX Algorithms with FASE},
author = {Federico Buti and Massimo Callisto De Donato and Flavio Corradini and Maria Rita Di Berardini and Walter Vogler},
journal= {arXiv preprint arXiv:1106.1231},
year = {2011}
}