Susan Older

Thesis Title: A Denotational Framework for Fair Communicating Processes
Degree Type: Ph.D. in Pure and Applied Logic
Advisor(s): Stephen Brookes
Graduated: December 1996

Abstract:

The behavior of a parallel system depends not only on the properties of the individual components running in parallel, but also on the 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 fairness assumptions—which, roughly speaking, states that every sufficiently enabled component eventually proceeds—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 communicating processes, based on the notion of 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.

Thesis Committee:
Stephen Brookes (Chair)
Edmund Clarke
Jeannette Wing
Prakash Panangaden (McGill University)

James Morris, Head, Computer Science Department
Raj Reddy Dean, School of Computer Science

Keywords:
Denotational semantics, fairness, communicating processes, traces, concurrency, full abstraction