Strong fairness and full abstraction for communicating processes

We construct several denotational semantics for communicating processes that incorporate assumptions of strong (process) fairness. Strong fairness is the guarantee that every process enabled infinitely often will make progress infinitely often. Modeling fairness compositionally requires care: generally speaking, the fair computations of a command cannot be defined only in terms of the fair computations of its component commands. For this reason, we introduce the notion of parameterized fairness, which generalizes fairness sufficiently to admit a compositional characterization. In each of these semantics, a command's meaning is simply the set of fair traces representing its fair computations; each fair trace records the steps made along a computation as well as additional information made explicit by the definition of parameterized fairness. Each semantics obtains full abstraction with respect to a natural notion of strongly fair program behavior: two terms are given identical meanings precisely when they exhibit the same behaviors in all program contexts.