@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(A Denotational Framework for Fair Communicating Processes)
@heading(CMU-CS-96-204)
@center(@b(Susan Older))
@center<December 1996 - Ph.D. Thesis (Pure and Applied Logic)>
@center(FTP: CMU-CS-96-204.ps)
@blankspace(1)
@begin(text)

The behavior of a parallel system depends not only on the properties of the
individual components running in parallel, but also on the @i{interactions}
among those components. These interactions in turn depend on external factors
(such as the relative speed of processors or the particular scheduler
implementation) whose details can be complex or even unknown. By introducing
appropriate @i{fairness assumptions}@y(M)which, roughly speaking, states that
every sufficiently enabled component eventually proceeds@y(M)we can abstract
away from these details without ignoring them completely. However, modeling
fairness for communicating processes is especially difficult; synchronization
requires the cooperation and active participation of multiple processes, and
hence the enabledness of a process depends on the ability of other processes
to synchronize with it. 

This dissertation introduces a general framework for modeling fairness for 
communication processes, based on the notion of @i{fair traces}. Intuitively,
a fair trace is an abstract representation of a fair computation, providing
enough structure to capture the important essence of the computation (e.g.,
the sequences of states encountered or the communications made along it) as
well as any contextual information necessary for compositionality. Within
this framework, the meaning of a command is simply the set of fair traces
that correspond to its possible fair computations. For each construct of
the language, we define a corresponding operation on trace sets that
reflects its operational behavior.

The use of traces provides a strong connection between the language's
operational semantics and its denotational semantics, allowing operational
intuition to guide formal, syntax-directed reasoning. Moreover, this trace
framework is remarkably robust. By varying the structure of the traces, we
can construct several different semantics that reflect different types of
fairness assumptions for the same language of communicating processes.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Denotational semantics, fairness, communicating processes,
traces, concurrency, full abstraction>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(170 pages)])