  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.

Logic in Computer Science;Distributed, Parallel, and Cluster Computing