Modelling Mutual Exclusion in a Process Algebra with Time-outs

Abstract

I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or justness, even when one makes the problem more challenging by assuming memory accesses to be atomic. This can be achieved only when dropping the requirement of speed independence.

Mild revision in response to I&C reviewing, with added conclusion. arXiv admin note: text overlap with arXiv:2008.13357

References in corpus (9)

• Progress, Justness and Fairness
• CCS: It's not Fair! Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Abstract Processes of Place/Transition Systems
• Analysing Mutual Exclusion using Process Algebra with Signals
• Progress, Fairness and Justness in Process Algebra
• Ensuring Liveness Properties of Distributed Systems: Open Problems
• Automated Analysis of MUTEX Algorithms with FASE
• Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
• Failure Trace Semantics for a Process Algebra with Time-outs