Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes
We provide a trace-based semantics for synchronously communicating processes, assuming a form of weakly fair parallel execution. The semantics is fully abstract: processes have the same trace sets if and only if their communication behaviors, including potential for deadlock, are identical in all program contexts. We avoid the traditional use of book-keeping information such as refusal sets, failures, and divergence traces; instead traces include the relevant information directly. The semantics can easily be adapted to model blocking or non-blocking communication guards, asynchronous communication and shared-memory parallelism. Thus we obtain a flexible model with a simple yet adaptable structure which emphasizes the underlying similarities between parallel paradigms. We also provide a compositional partial-order description of trace sets, adapting ideas from pomset semantics to incorporate fairness and synchronization. The pomset semantics can also be adapted easily to model alternative forms of guard, asynchronous communication and shared memory. In each case the trace set of a process can be recovered from the pomset semantics by taking all fair interleavings consistent with the partial order. We illustrate the utility of our semantics by analyzing the behavior of a number of examples, and by listing some laws of semantic equivalence which rely on fairness and can be used in analyzing process behavior.