A Denotational Framework for Fair Communicating Processes.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1996
- Accession Number
- ADA326211
Entities
People
- Susan Older
Organizations
- Carnegie Mellon University