In of ?nite pre?xes. Consequently these models did not

In these early models of CSP the focus is on ?nite behaviors, with in?nite traces either ignored or regarded as being present only by virtue of ?nite pre?xes. Consequently these models did not take fairness into account. Yet fairness assumptions, such as the guarantee that a process waiting for input will eventually be synchronized if another process is simultaneously (and persistently) waiting for a matching output, are vital when trying to reason about liveness properties 24, 23. As a result it can be argued that these models are, by their very design, less than ideally suited to reasoning about liveness. Although it is possible to develop straightforward variants of these models that incorporate in?nite traces 28, it is not obvious how to augment them in such a way that only fair traces get included. Indeed there is a plethora of distinct fairness notions in the literature 13, and it is not clear which (if any) of these notions are simultaneously a reasonable abstraction from network implementation and adaptable to CSP. Susan Older’s Ph.D. thesis 21 contains a detailed discussion of the problems that arise as well as a family of models tailored to speci?c fairness notions. Older’s modelscan be regarded as failures/divergences equipped with in?nite traces and book-keeping information about persistently enabled communication 6. As Older discovered, it can be very di?cult to ?gure out a suitable augmentation regime for extending failures/divergences to match a given notion of fairness, largely because of the fact that enabledness of communication for one process depends on enabledness of matching communication in another process. The di?culties seem less severe when dealing with asynchronous communication 5. The models described so far were developed speci?cally with TCSP in mind, and serve this role admirably. However, CSP is not the only paradigmatic parallel programming language and it is natural to compare the semantic framework built for CSP with the models developed over the years for shared memory parallel programs and for networks of asynchronously communicating processes. By the same token, TCSP is not the only process algebra, and the emphasis in CSP on deadlock and divergence is in sharp contrast to the focus on bisimulation in calculi based on Milner’s CCS 19,20. Unfortunately there is frustratingly little similarity in structure between the early semantic models developed for these other paradigms and these CSP models. For instance the resumptions of Hennessy and Plotkin 14, and the transition traces of Park 24 (later adapted by this author 4), originally proposed to model shared memory parallel programs, bear no obvious structural relationship with failures. These semantic disparities make it di?cult to apply techniques successful in one setting to similar problems occurring in the other settings. For instance, Older’s construction of fair models of CSP does not immediately suggest an analogous construction for a language of asynchronously communicating processes. A further disparity is caused by the emphasis (for obvious reasons) on state in traditional models of shared memory parallelism, in contrast to the prevailing tendency in process algebras such as CSP and CCS to abstract away from state 19,2. In a paper presented in tribute to the twentieth anniversary of CSP 7 this author proposed a semantic model based on transition traces, suitable for modelling both shared memory parallel programs and networks of processes communicating asynchronously on named channels. At that time it seemed unlikely that similar techniques would prove suitable for modelling synchronized communication, because of the di?culties encountered by Older in adapting failures to fairness in the synchronous setting. Nevertheless the author discovered later that essentially the same framework can also be made to work for synchronously communicating processes, provided a simple enough notion of fairness is adopted 8. This is a somewhat surprising turn of events given the prior history of separate development. More recently still, we realized that it is possible to modify this semantic framework in a natural way to handle race conditions, leading to an improved semantics in which assumptions about the granularity of atomic actions become less signi?cant 9. We will now summarize the main technical notions behind this semantics. The key turns out to involve the choice of a suitably general notion of trace, which can be presented in a process algebraic formulation and separately instantiated later in a state-dependent setting