CaltechTHESIS
  A Caltech Library Service

Synchronizing processes

Citation

Hofstee, H. Peter (1995) Synchronizing processes. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/G620-GG65. https://resolver.caltech.edu/CaltechETD:etd-10112007-083903

Abstract

In this monograph we develop a mathematical theory for a concurrent language based on angelic and demonic nondeterminism. An underlying model is defined with sets of sets of sequences of synchronization actions. A refinement relation is defined for the model, and equivalence classes under this relation are identified with processes. Processes, together with the refinement relation, form a complete distributive lattice. We define a language with parallel composition, sequential composition, angelic and demonic nondeterminism, and an operator that connects pairs of synchronization actions into synchronization statements and hides these actions from observation. Also, angelic and demonic iteration are defined. All operators are monotonic with respect to the refinement ordering. Many algebraic properties are proven from these definitions. We study duals of processes and prove that they can be related to the most demonic environment in which a process will not deadlock. We give a simple example to illustrate the use of duals. We study classes of programs for which angelic choice can be implemented by probing the environment for its next action. To this end specifications of processes are extended with simple conditions on the environment. We give a more elaborate example to illustrate the use of these conditions and the compositionality of the method. Finally we briefly introduce an operational model that describes implementable processes only. This model mentions probes explicitly. Such a model may form a basis for a language that is less restrictive than ours, but that will also have less attractive algebraic properties.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:formal methods, concurrency, synchronization, process algebra
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Van de Snepscheut, Jan L. A. (advisor)
  • Chandy, K. Mani (advisor)
Thesis Committee:
  • Van de Snepscheut, Jan L. A. (chair)
  • Martin, Alain J.
  • Seitz, Charles L.
  • Chandy, K. Mani
  • Bagrodia, Rajive
  • Abu-Mostafa, Yaser S.
Defense Date:30 September 1994
Non-Caltech Author Email:hofstee (AT) us.ibm.com
Record Number:CaltechETD:etd-10112007-083903
Persistent URL:https://resolver.caltech.edu/CaltechETD:etd-10112007-083903
DOI:10.7907/G620-GG65
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:4036
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:25 Oct 2007
Last Modified:21 Dec 2019 04:32

Thesis Files

[img]
Preview
PDF (Hofstee_hp_1995.pdf) - Final Version
See Usage Policy.

4MB

Repository Staff Only: item control page