Analysing Mutual Exclusion using Process Algebra with Signals

Abstract

In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counter-intuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.

In Proceedings EXPRESS/SOS 2017, arXiv:1709.00049

References in corpus (5)

• A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV
• CCS: It's not Fair! Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Progress, Fairness and Justness in Process Algebra
• Automated Analysis of MUTEX Algorithms with FASE
• Read Operators and their Expressiveness in Process Algebras

Cited by in corpus (9)

• Progress, Justness and Fairness
• Ensuring Liveness Properties of Distributed Systems: Open Problems
• Tutorial: Designing Distributed Software in mCRL2
• A process algebra with global variables
• Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
• Justness: A Completeness Criterion for Capturing Liveness Properties
• Fair Mutual Exclusion for N Processes (extended version)
• A Lean-Congruence Format for EP-Bisimilarity
• Modelling Mutual Exclusion in a Process Algebra with Time-outs