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. We study the impact this new kind of actions has on fairness, liveness and the timing of systems, using as application Dekker’s mutual exclusion algorithm we already considered in [4]. 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 in [6] when studying the performance of pipelining. Finally, our previous result on the correspondence between timing and fairness [4] scales up to the extended language.