DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA326211
Title:
A Denotational Framework for Fair Communicating Processes.
Descriptive Note:
Doctoral thesis,
Corporate Author:
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Report Date:
1996-12-01
Pagination or Media Count:
169.0
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 languages operational semantics and its denotational semantics, allowing operational intuition to guide formal, syntax directed reasoning. Moreover, this trace framework is remarkably robust.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE
