Matthew Hennessy
Robin Milner
Abstract
Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behavior of a program part, that is, its meaning, is defined to be its observation congruence class.
The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
- 1 GORDON, M. J.l'tte Denotational Description oJ Programming Languages. Springer-Verlag, New York, 1979. Google Scholar
- 2 HENNESSY, M., AND MILNER, R.On observing nondeterminism and concurrency. In Proceedings of the 7th Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 85. Springer-Vedag, New York, Berlin, Heidelberg, 1980, pp. 299-309. Google Scholar
- 3 HENNESSY, M., AND PLOTKIN, G. D.Full abstraction for a simple parallel programming language. In Proceedings of the 8th MFCS Conference (Olomouc, Czechoslovakia). Lecture Notes in Computer Science, vol. 74. Springer-Verlag, New York, 1979, pp. 108-121.Google Scholar
- 4 MILNE, G., AND MILNER, R.Concurrent processes and their syntax. J. ACM 26, (1979), 302-321. Google Scholar
- 5 MILNER, R.Synthesis of communicating behaviour. In Proceedings of the 7th MFCS Conference (Zacopane, Poland). Lecture Notes in Computer Science, vol. 64. Springer-Vedag, New York, 1978, pp. 71-83.Google Scholar
- 6 MILNER, R.A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer-Verlag, New York, 1980. Google Scholar
- 7 PLOTKIN, G. D.A powerdomain construction. SIAM J. Comput. 5, 3 (1976), 452-487.Google Scholar
- 8 PNUELI, A.The temporal logic of programs. In Proceedings of the 19th Annual Symposium on Foundations of Computer Science (Providence, R.I.). IEEE, New York, 1977, pp. 46-57.Google Scholar
- 9 PRATT, V.R.Semantical considerations of Floyd-Hoare logic. In Proceedings of the 17th Annual Symposium on Foundations of Computer Science. IEEE, New York, 1976, pp. 109-121.Google Scholar
- 10 SMYTH, M. Powerdomains. J. Comput. Syst. Sci. 15, 1 (1978), 23-36.Google Scholar
- 11 STOY, J.E.Denotational Semantics: The Scott Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Mass., 1977. Google Scholar
Index Terms
- Algebraic laws for nondeterminism and concurrency
Recommendations
Nondeterminism in Constructive Z
The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, ...
Nondeterminism in Constructive Z
The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, ...
An Algebraic Theory for Shared-State Concurrency
Programming Languages and SystemsAbstractWe present a monadic denotational semantics for a higher-order programming language with shared-state concurrency, i.e. global-state in the presence of interleaving concurrency. Central to our approach is the use of Plotkin and Power’s algebraic ...
Reviews
A. Prasad Sistla
Giving precise and well-defined meanings to programs and programming languages allows implementors of programming languages to prove the correctness of their implementations with respect to their specifications. For sequential programs, the meaning of a program is a partial function from the input domain to the output domain. In the case of concurrent programs, the meaning of a program should also capture the intermediate behavior of the program. The languages CSP [1] and CCS [2] have been introduced as formalisms for describing the behavior of concurrent programs. The main feature of these languages is that processes do not use any shared variables; they communicate through synchronization on common actions. These formalisms have influenced the later development of practical programming languages such as Ada and OCCAM. For this reason it is important to give precise semantics of CCS and CSP programs. Both of the papers under review have made important contributions to the semantics of CCS and CSP, and they take different approaches. <__?__Pub Lcl partst="bold-italic" pindent="0pt" paboveskip="10pt">Hennessy and Milner This paper presents the semantics of processes in terms of an equivalence relation between processes called <__?__Pub Fmt italic>observational congruence;<__?__Pub Fmt /italic> it gives complete algebraic axiom systems for proving observational congruence of finite processes defined by simple languages of CCS terms. In order to define observational congruence, the operational meaning of a process is assumed to be given by the relations ? &agr; for each action a ?M , where <__?__Pub Fmt italic>M<__?__Pub Fmt /italic> is an alphabet of actions. Intuitively, <__?__Pub Fmt italic>p<__?__Pub Fmt /italic><__?__Pub Fmt kern Amount="4pt">? &agr; <__?__Pub Fmt kern Amount="4pt"><__?__Pub Fmt italic>q<__?__Pub Fmt /italic> means that process <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> permits the action &agr; after which it behaves like process <__?__Pub Fmt italic>q.<__?__Pub Fmt /italic> Observational congruence is defined in terms of the relation <__?__Pub Fmt italic>observational equivalence.<__?__Pub Fmt /italic> Observational equivalence is the largest equivalence relation ? that satisfies the following property: p?q if for all a ?M , for all p ?, p?p ? a implies that for some q ?, q?q ? a and p ??q ? ; similarly, for all q ?, q?q ? a implies that for some p ?, p?p ? a and<__?__Pub Fmt hardspace> <__?__Pub Caret1> p ??q ? . Processes <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> and <__?__Pub Fmt italic>q<__?__Pub Fmt /italic> are <__?__Pub Fmt italic>observationally congruent<__?__Pub Fmt /italic> if<__?__Pub Fmt hardspace>in all process contexts, substituting <__?__Pub Fmt italic>p<__?__Pub Fmt /italic>, <__?__Pub Fmt italic>q<__?__Pub Fmt /italic> respectively results in processes that are observationally equivalent. This paper defines the semantics of a process as the observational congruence class of the process. The paper also introduces a simple modal logic and shows that when the relations ? &agr; are image finite, two processes satisfy the same formulas of the logic if and only if they are observationally equivalent. Thus, observational equivalence can also be characterized in terms of logic. The paper considers processes defined by CCS expressions over three operator sets S 1, S 2, and S 3, where S 1 contains a unary operator corresponding to each member in <__?__Pub Fmt italic>M<__?__Pub Fmt /italic>, the non-deterministic choice operator, and the special process NIL; S 2 contains all the operators of S 1 together with the parallel composition operator; and S 3 contains all the operators of S 2 together with renaming operators. The alphabet <__?__Pub Fmt italic>M<__?__Pub Fmt /italic> contains a special action t denoting an internal action of a process. For each of the above operator sets, two kinds of observational congruences are considered by treating t as an observable action or as an unobservable action, resulting in six different cases. For all six cases, the authors present complete algebraic axioms for proving observational congruence. It turns out that when t is treated as an observable action, observational congruence coincides with observational equivalence. <__?__Pub Lcl partst="bold-italic" pindent="0pt" paboveskip="10pt">Brookes, Hoare, and Roscoe The authors present a mathematical domain for specifying the semantics of communicating sequential processes. As above, the authors assume that the only thing observable about a process is its interactions with the external world. The observation of a process is a finite experiment that can be carried out on the process; two processes are identical if they cannot be distinguished by an experiment. As in the previous paper, the operational semantics of a process is assumed to be given by the relations ? &agr; . The denotational semantics of a process is defined in terms of the failures of the process. For a sequence of actions given by <__?__Pub Fmt italic>s<__?__Pub Fmt /italic>, and for a subset of actions <__?__Pub Fmt italic>X<__?__Pub Fmt /italic>, the pair (<__?__Pub Fmt italic>s,X<__?__Pub Fmt /italic><__?__Pub Fmt kern Amount="1.2pt">) is a failure of the process <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> if <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> can engage in the sequence of actions given by <__?__Pub Fmt italic>s<__?__Pub Fmt /italic> and then refuse all the actions in <__?__Pub Fmt italic>X<__?__Pub Fmt /italic>. For a process <__?__Pub Fmt italic>p<__?__Pub Fmt /italic>, the denotation of <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> is given by failures(<__?__Pub Fmt kern Amount="1.2pt"><__?__Pub Fmt italic>p<__?__Pub Fmt /italic>), the set of all failures of <__?__Pub Fmt italic>p<__?__Pub Fmt /italic>. This semantics maintains more information than the trace-based semantics in which the semantics of a process is given by the set of traces that it can engage in. For instance, the failure-based semantics has enough information to detect the possibility of deadlocks. Process <__?__Pub Fmt italic>p<__?__Pub Fmt /italic> is said to be more deterministic than process <__?__Pub Fmt italic>q<__?__Pub Fmt /italic> if failures(<__?__Pub Fmt kern Amount="1.2pt"><__?__Pub Fmt italic>p<__?__Pub Fmt /italic>) ? failures(<__?__Pub Fmt italic>q<__?__Pub Fmt /italic>). The authors show that this defines a complete partial order on the set of processes. The paper introduces many operators on processes, including nondeterministic choice, sequential composition, various parallel compositions, hiding, renaming, and recursion operators. The semantics of all the operators are defined as functions that map failure sets to failure sets. All the operators are shown to be continuous. As a consequence, recursive equations have solutions; and the semantics for the recursion operator is given in terms of the least fixed points of equations. The paper illustrates the main ideas with many examples. <__?__Pub Lcl partst="bold-italic" pindent="0pt" paboveskip="10pt">Related Work The semantics of processes based on observational equivalence as given in Hennessy and Milner are stronger than the failure semantics of Brookes, Hoare, and Roscoe. Two processes that are observationally equivalent have the same failure semantics; however, simple processes exist that are identified by the failure semantics but are not observationally equivalent. While Hennessy and Milner do not consider divergence, Brookes, Hoare, and Roscoe handle divergence by identifying a process that diverges with a special process called CHAOS that can engage in any sequence of actions but that can refuse to accept any action after this. Brookes and Roscoe [3] give an improved failure semantics that handles divergence in a more sophisticated manner. One of the earliest semantics of CSP using computation trees was given in Francez et al. [4]. A later paper presents a semantics of CSP that uses traces of communications and special states called expectation sets to characterize potential deadlocks. Milner introduced the notion of bisimulation, which is similar to observational equivalence [2]. DeNicola and Hennessy [6] present three different notions of the equivalence of CCS processes based on testing. They present complete axiom systems for proving the three notions of test equivalence of processes and give a denotational semantics based on tree representations. Pneuli [7] gives an elegant classification of the various semantics according to the approaches they take: semantics by equivalence classes, exterior semantics, and semantics by logics. He further classifies them according to the view they take: a branching view or a linear view. In this classification, the observational congruence considered in Hennessy and Milner is semantics by equivalence that takes a branching view, while the failure semantics of Brookes, Hoare, and Roscoe is exterior semantics based on a linear view. The semantics given by DeNicola and Hennessy [6] is based on equivalence classes taking a linear view. The semantics of Francez, Lehmann, and Pnueli [5] and Francez et al. [4] are exterior semantics that take linear and branching views, respectively. Olderog and Hoare give a uniform framework for presenting semantics of communicating processes by defining four denotational models that capture different levels of detail about process behaviors that handle divergence in different ways [8]. They give four models, called the counter model, the trace model, the readiness model, and the failures model. The counter model is the weakest of these. The failure model is similar to the model of Brookes, Hoare, and Roscoe but it handles divergence by having a special symbol ? to denote divergence. The readiness model defines a process semantics as a set of elements of the form <__?__Pub Fmt italic>s<__?__Pub Fmt /italic>, (<__?__Pub Fmt italic>s,X<__?__Pub Fmt /italic>) where <__?__Pub Fmt italic>s<__?__Pub Fmt /italic> is the sequence of actions that the process can engage in and <__?__Pub Fmt italic>X<__?__Pub Fmt /italic> is the set of actions that the process can accept after engaging in <__?__Pub Fmt italic>s<__?__Pub Fmt /italic>; if the process can diverge after engaging in <__?__Pub Fmt italic>s<__?__Pub Fmt /italic>, then this ability is captured by having the element <__?__Pub Fmt italic>s<__?__Pub Fmt /italic> ? in the semantics; readiness semantics is similar to the semantics of Francez, Lehman, and Pnueli [5] and is shown to be equivalent to the failure semantics.
Alfs T. Berztiss
This is a clearly written paper that combines motivation, intuitive exposition, and rigorous formulation in excellent balance. The authors set themselves the task of capturing the meaning of complicated processes, in which phenomena such as deadlock can arise. They do so by introducing the concepts of equivalence (two processes are equivalent if no observations can distinguish them) and congruence (two modules are congruent if substitution of one for the other preserves equivalence in all contexts). These concepts are precisely made; the meaning of a module is defined as its congruence class; and congruence is axiomatized for a sequence of algebraic languages. Finally, the approach is related to Milner's work [1].
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments