Time and fairness in a process algebra with non-blocking reading

We introduce the first process algebra with non-blocking reading actions for modelling concurrent asynchronous systems, and we do it in two different ways: one is more flexible, the other is simpler since it needs only one type of transitions. We study the impact this new kind of actions have on fairness, liveness and the timing of systems, using Dekker's mutual exclusion algorithm we already considered in earlier work as running example. Regarding some actions as reading, this algorithm satisfies MUTEX liveness already under the assumption of fairness of actions. We demonstrate an interesting correspondence between liveness and the catastrophic cycles that we introduced before when studying the performance of pipelining. Finally, our previous result on the correspondence between timing and fairness scales up to the extended language