Strong fairness and recursive communicating processes

Fairness - the guarantee that every process enabled sufficiently often will eventually make progress - provides a convenient and often useful abstraction from timing details that affect how parallel processes interact with one another. For processes that communicate via synchronous message passing, strong fairness is generally accepted as the most reasonable notion of fairness. This paper describes a strongly fair, trace-based semantics for a CCS-like language of communicating processes with full recursion. The semantics is a generalization of previous semantics for fair, imperative communicating processes. Unlike those earlier semantics, however, this semantics is not fully abstract: the combination of synchronous communication, fairness, and full recursion is extremely problematic. We outline the general difficulties encountered and discuss why the fair-trace approach is unlikely to yield full abstraction for this combination of features.