Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes Stephen Brookes
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.
|
concur02@fi.muni.cz |