Modelling Mutual Exclusion in a Process Algebra with Time-outs

TL;DR

This paper demonstrates that mutual exclusion with starvation-freedom can be accurately modeled in a process algebra with time-outs without fairness assumptions, by sacrificing speed independence, even with atomic memory access.

Contribution

It introduces a method to model mutual exclusion in process algebra with time-outs that ensures starvation-freedom without fairness, challenging previous assumptions.

Findings

Mutual exclusion can be modeled with starvation-freedom without fairness.

Speed independence must be sacrificed for correct modeling.

Atomic memory access does not prevent starvation-freedom in the model.

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.