Processes and the Denotational Semantics of Concurrency

摘要

A framework allowing a unified and rigorous definition of the semantics of concurrency is proposed. The mathematical model introduces processes as elements of process domains which are obtained as solutions of domain equations in the sense of Scott and Plotkin. Techniques of metric topology as proposed, e.g., by Navat are used to solve such equations. Processes are then used as meanings of statements in languages with concurrency. Three main concepts are treated, viz. parallellism - arbitrary interleaving of sequences of elementary actions, synchronization, and communication. These notions are embedded in languages which also feature classical sequential concepts such as assignment, tests, iteration or recursion, and guarded commands. In the definitions, a sequence of process domains of increasing complexity is used. The languages discussed include Milner's calculus for communicating systems and Hoare's communicating sequential processes. The paper concludes with a section with brief remarks on miscellaneous notions in concurrency, and two appendices with mathematical details.