A framework for fair communicating processes

This paper describes a general framework for modeling fairness for communicating processes, based on the notion of fair traces. Intuitively, a fair trace is an abstract representation of a fair computation, providing enough structure to capture the important essence of the computation (e.g., the sequences of states encountered or the communications made along it) as well as any contextual information necessary for compositionality. The key for determining this necessary contextual information is the introduction of parameterized fairness notions, which permit compositional characterizations of fairness. In contrast, most traditional treatments of fairness are based on operational semantics and do not lend themselves naturally to compositional reasoning. This trace framework is remarkably robust. By varying the structure of the traces, we can construct several different semantics that reflect different types of fairness assumptions for the same language of communicating processes. These semantics in turn support not only compositional reasoning about fair program behavior but also the comparison of different fairness notions and the semantic structure that they require.