Automated Analysis of MUTEX Algorithms with FASE

TL;DR

This paper uses the FASE tool to analyze the liveness of MUTEX algorithms modeled in a process algebra, highlighting the impact of non-blocking behaviors on system correctness.

Contribution

It demonstrates the application of FASE to real examples and explores how non-blocking behaviors affect the modeling of concurrent systems.

Findings

FASE effectively verifies liveness properties in MUTEX models

Non-blocking behaviors influence the detection of catastrophic cycles

Comparison shows advantages of the proposed approach

Abstract

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.