Keep it fair: equivalence and composition (Q2423741)

Since E. W. Dijkstra introduced the concept of fairness in 1987, various fairness notions for different models have been introduced, discussed and compared. Roughly speaking, fairness excludes infinite executions of distributed systems or programs where a local component does not progress or does not execute a certain activity, although this activity is persistently or infinitely often enabled to occur. Fairness is not a semantical property of a distributed system, but is rather used as an assumption, restricting the relevant behavior to executions respecting fairness. Each notion of semantics of a formal modeling language for distributed systems induces an equivalence notion on models, expressing semantical equivalence of models, i.e., the same behavior according to this semantics. Unfortunately, fairness is not always respected by this equivalence. The first contribution of this paper is an equivalence spectrum in which fairness assumptions are preserved. Modeling languages for distributed systems are equipped with a composition operator, inducing parallel composition of component executions. The paper also analyses parallel composition operators and their synchronization mechanisms with respect to fairness.