Automated Analysis Of Mutex Algorithms With Fase

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.