Encoding fairness in a synchronous concurrent program algebra: extended version with proofs

TL;DR

This paper extends concurrent program algebra to include fairness, enabling formal reasoning about fair execution and parallelism in shared-memory concurrent programs, supported by algebraic theory and proofs.

Contribution

It introduces a formal encoding of fairness within a synchronous concurrent program algebra, with proofs and a theory supporting fair execution and parallelism.

Findings

Defined a fairness encoding in the algebra

Supported reasoning about fair execution of individual processes

Developed an algebraic theory for fairness and fair-parallelism

Abstract

Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example, it supports the rely/guarantee approach of Jones. The algebra makes use of a synchronous parallel operator motivated by Aczel's trace model of concurrency and with similarities to Milner's SCCS. This paper looks at defining a form of fairness within the program algebra. The encoding allows one to reason about the fair execution of a single process in isolation as well as define fair-parallel in terms of a base parallel operator, of which no fairness properties are assumed. An algebraic theory to support fairness and fair-parallel is developed.