Lecture Notes in Computer Science 527 Edited by G. Goos and J. Hartmanis Advisory Board: W. Brauer D. Gries J. Stoer .J M. C. Baeten .J E Groote (Eds.) CONCUR '91 2nd International Conference on Concurrency Theory Amsterdam, The Netherlands, August 26-29, 1991 Proceedings :ucn~ ! galreV-regnirpS Berlin Heidelberg NewYork London Paris Tokyo Hong Kong Barcelona Budapest Series Editors Gerhard Goos Juris Hartmanis GMD Forschungsstelle Department of Computer Science Universit~t Karlsruhe Cornell University Vincenz-Priessnitz-StraBe 1 Upson Hall W-7500 Karlsruhe, FRG Ithaca, NY 14853, USA Volume Editors Jos C. M. Baeten Department of Software Technology, CWI Kruislaan 413, 1098 SJ Amsterdam, The Netherlands and Programming Research Group, University of Amsterdam Kruislaan 403, 1098 SJ Amsterdam, The Netherlands Jan Frisco Groote Department of Software Technology, CWI Kruislaan 413, 1098 SJ Amsterdam, The Netherlands CR Subject Classification (1991): F.1.2, D.1.3, D.3.1, D.3.3, F.3.1 ISBN 3-540-54430-5 Springer-Verlag Berlin Heidelberg New York ISBN 0-387-54430-5 Springer-Verlag New York Berlin Heidelberg This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilomrs in other ways, and storage in data banks. Duplication of this publication or parts thereof is only permitted under the provisions of the German Copyright Law of September 9, 1965, in its current version, and a copyright fee must always be paid. Violations fall under the prosecution act of the German Copyright Law. © Springer-Verlag Berlin Heidelberg 1991 Printed in Germany Typesetting: Camera ready by author Printing and binding: Druckhaus Beltz, Hemsbach/Bergstr. 2145/3140-543210 - Printed on acid-free paper Preface CONCURS91 is the second international conference on concurrency theory, organised in association with the NFI project Transfer. It is a sequel of the CONCURt90 conference. Its basic aim is to communicate ongoing work in concurrency theory. This year 71 papers were submitted, 17 more than last year. From these, 30 papers were selected for presentation at the conference. The selected papers appear in these proceedings, together with four papers oifn vited speakers. Furthermore, abstracts of the other invited lectures are included. CONCURf91 received support from CWI, the University of Amsterdam, and ERCIM, the European Research Consortium for Informatics and Mathematics. The editors want to thank the members of the program committee and the subreferees for their careful selection of the submitted papers. Thanks also go to CWI for hosting the conference, and to the organising committee for all their efforts. Amsterdam, July 1991 The Editors Program Committee (general chair) J.C.M. Baeten Section Process Algebras Section Tools and Probabilities R.J. van Glabbeek E. Madelaine (chair) K.G. Larsen F. MoUer (chair) W.P. Weijland S.A. Smolka Section Logics and Model Checking Section Programming Languages (chair) H. Barringer J.W. de Bvkker J.-J.Ch. Meijer G.L. Burn (chair) C.P. Stirling L. Monteiro Section Applications and Specification Languages (chair) M. Broy J. Sifakis F.W. Vaandrager Orgauislng Committee Section Models and Net Theory (chair) E. Best (chair) R. De Nicola J.A. Bergstra L. PomeUo M. Drolschbach J.F. Groote Section Design and Real-Time S. Manw (chair) C.A.R. Hoare A. Ollongren W.P. de Roever F. Snijders C.A. Vissers List of Referees Andreoli J.-M. R. Gerth .L Monteiro A. Azcorra .S Gilmore .Y Ortega-Mallen J.C.M. Baeten R.J. van Glabbeek .C Palamidessi .E.J Barnes R. ireirroG I.C.C. Phillips H. Barringer Goltz U. A. Poignd Bergstra J.A. G.D. Gough .L Pomello .L Bernardinello Gritzner T.F. .A Ponse A. Bertoni .F.J Groote D.J. Pym E. Best W.H. Hesselink J. Quemada G. Boudol C.A.R. Hoare G. Reggio .P.J Bowen J.J.M. Hooman W. Reisig .C.J dleifdarB M. van Hulst A. Rensink A. Brogi A. rittddsf16gnI W.-P. de Roever M. Broy D.M. Jackson .M Ronsangue G. Bruns M. Jantzen J.J.M.M. Rutten G.L. Burn .L Jategaonkar S.A. Schneider .P Caspi He Jifeng K. Seidel F. de Cindio M.B. Josephs .N Sabadini K.L. Clark Y.-J. Joung J. Sifakis W.R. Cleaveland W.T.M. Kars .H Simmons A. Corradini A.S. Klusener A. Skou .G Costa W.P. Koole S.A. Smolka M.F. Dam H.P. Korver C.P. Stirling Ph. Darondeau H.-J. Kreowski Torts C. J. Davies .A Labella G.J. Tretmans F. Dedericks C. Laneve .I Ulidowski .G De Michelis R. Langerak F.W. Vaandrager .C Dendorfer K.G. Larsen R. Valk R. De Nicola .G Linde .D Vergamini R. Deniot E. Madelaine C.A. Vissers J.-C. Fernandez .G Mauri K. Voss .G Ferrari J.-J.Ch. Meyer .R Weber D. Escrig Frutos C.A. Middelburg W.P. Weij land M. Fuchs F. Moller J. Winkowski H. Garavel .B Monahan J. Zwiers P.H.B. Gardiner Table of Contents Invited Lectures P. America Formal Techniques for Parallel Object-Oriented Languages A. Bouali, R. de Simone Causal Models for Rational Algebraic Processes 18 R. De Nicola Action and State-based Logics for Process Algebras 02 J.-C. Fernandez, L. Mounier A Tool Set for Deciding Behavioral Equivalences 32 .U Goltz Causality Based Models for the Design of Concurrent Systems 34 R. Milner, J. Parrow; .D Walker Modal Logics for Mobile Processes 45 E.-R. 01derog Towards a Design Calculus for Communicating Programs 16 Selected Presentations L. Ace~o, A. ritt6dsi16gnI A Theory fo Testing rof ACP 87 J.C.M. Baeten, J.A. Bergstra Real Space Process Algebra 69 F.S. de Boer, J.N. Kok, .C Palamidessi, J.J.M.M. Rutten The Failure of Failures in a Paradigm for Asynchronous Communication 111 F.S. de Boer, .C Palamidessi Embedding as a Tool for Language Comparison: On the CSP Hierarchy 721 J. Camilleri A Conditional Operator for CCS 142 N.J. Drost Algebraic Formulatioonfs Trace Theory 751 J. Esparza, M. Silva Compositional Synthesis of Live and Bounded Free Choice Petri Nets 271 Viii G.L. Ferrari, .U Montanari The Observation Algebra of Spatial Pomsets 881 .rh Francez, LR. Forman Synchrony Loosening Transformations for Interacting Processes 302 K.J. Goldman A Compositional Model for Layered Distributed Systems 220 J.F. Groote, A. Ponse Process Algebra with Guards 532 O. Grumberg, D.E. Long Model Checking and Modular Verification 052 J. Gunawardena Geometric Logic, Causality and Event Structures 662 J.-M. Jacquet, L. Monteiro Extended Horn Clauses: the Framework and some Semantics 182 W. Janssen, M. Poel, J. Zwiers Action Systems and Action Refinement in the Development of Parallel Systems 892 R. Janicki, M. Koutny Invariant Semantics of Nets with Inhibitor Arcs 317 A. Jeffrey Abstract timed Observation and Process Algebra 233 B. Jonsson Simulations between Specifications of Distributed Systems 643 R. Kaivola, A. Valmari Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models 163 A.S. Klusener Completeness in Real Time Process Algebra 376 P. Krishnan Distributed CCS 393 M. Merritt, F. Modugno, M.R. Ta~tle Time-Constrained Automata 408 F. Moller, C. Torts Relating Processes With Respect to Speed 424 D. Murphy Testing, Betting and Timed True Concurrency 439 XI D. Nolte, .L Priese ssenriaF ni Models with True Concurrency 455 H. Qin Efficient Verification of Determinate Processes 074 Ph. Schnoebelen Experiments on Processes with Backtracking 084 P. Spruit~ R. Wieringa Some Finite-graph Models for Process Algebra 594 K. St¢len A Method for the Development of Totally Correct Shared-State Parallel Programs 015 A. Valmari, M. C/egg Reduced Labelled Transition Systems Save Verification Ei~ort 625 Author Index 145 Techniques Formal rof Parallel Object-Oriented Languages Pierre America Philips Research P.O. Box 80.000 5600 JA Eindhoven The Netherlands Abstract This paper is intended to give an overview of the formal techniques that have been developed to deal with the parallel object-oriented language POOL and several related languages. We sketch a number of semantic descriptions, using several formalism: operational semantics, de- notational semantics, and a new approach to semantics, which call we layered semantics. Then we summarize the progress that has been made in formal proof systems to verify the correctness of parallel object-oriented programs. Finally we survey the techniques that we are currently developing to describe the behaviour of objects independently of their implementation, leading to linguistic support for behaviourai subtyping. 1 Introduction Over the last few years, object-oriented programming has gained widespread use and considerable popularity. Until now, the use of object-oriented techniques for parallel programming is mainly restricted to research environments, but nevertheless it holds considerable promises to contribute to the solutions of many problems associated with the programming of parallel computers. At the Philips Research Laboratories in Eindhoven, the Netherlands, several research projects in this area have been carried out. The DOOM project (Decentralized Object-Oriented Machine) was a subproject of ESPRIT project 415: 'Parallel Architectures and Languages for Advanced Information Processing -- a VLSI-directed Approach' [AHO+90]. This ESPRIT project aimed at improving the performance of computers in the area of symbolic applications by the use of large-sc~e parallelism. Several approaches were explored in different subprojects, which were tied together at a disciplinary level by working groups [Bak89, Tre90]. The DOOM subproject had chosen an object-oriented approach [AHg0]. This subproject developed a paralld object-oriented programming language POOL in which applications can be written, together with a parallel machine architecture suitable to execute programs in this language. A number of example applications have been developed as well. Another project, PRISMA (PaRallel Inference and Storage MAchine), built on the same object- oriented principles as the DOOM project. It aimed at developing a system that is able to handle very large amounts of knowledge and data, again usingp arallelism to reach a high performance. One tohfe concrete results of this project is a prototype relational database machine which can automatically exploit parallelism in evaluating the users' queries [AHH+90]. Together with the DOOM project, a prototype computer, POOMA (Parallel Object-Oriented Machine Architecture), has been built, on which the software developed in these projects is running. It comprises 100 processor nodes, each with its own local memory, and connected by a high-speed packet switching network. This paper saw written in the context of ESPRIT Basic hcraeseR Action :0203 Integration. The language POOL (Parallel Object-Oriented Language) used in these projects has been the subj~t of extensive theoretical studies. In the present paper, we give a survey of the results of these studies, and we shall try to assess their influence on the design and the use of the language. In fact, the name POOL stands for a family of languages, developed over a period of seven years. The most important one is POOL2 lAme88], the language that was implemented on the POOMA machine. Whenever the exact member of the POOL family does not matter, we shall just use the name POOL. Section 2 gives an introduction to the language POOL itself. Section 3 gives an overview of the techniques that have been used to describe the semantics of POOL in a formal way. Then section 4 sketches the research that has been done in the areao f formal verification of POOL programs. Finally, in section 5 we describe the typically object-oriented phenomena of inheritance and subtyping, and show how formal techniques can hdp to darify many of the issues involved. 2 An overview of the language POOL This section gives a summary of the most important ingredients of the POOL language. For more details, we refer the reader to [Ame89b], or to the official language definition lAme88]. In POOL, a system is described as a collection of objects. An object can be thought of as a kind of box, containing some data and having the ability to perform some actions on these data. An object uses variables to store its data. A variable contains a reference to another object (or, possibly, to the object containing the variable itself). The object's ability to perform operations on its internal data lies in two mechanisms: First, an object can have a set of methods, a kind of procedures, which can access and change the values of the variables. (Up to this point, the mechanisms that we have described are generally present in object-oriented languages.) Second, an object has a so-caUed ,ydob a local process that can execute in parallel with the bodies of all the other objects in the system. This is specific for POOL; it constitutes the main source of parallelism in POOL programs. A very important principle in object-oriented programming is encapsulation: The variables of one object are not directly accessible to other objects. In fact, the only way for objects to interact is by sending messages. A message is a request to the receiving object to execute one of its methods. The sending object explicitly mentions the receiver and the method name. It can also pass some parameters (again references to objects) to the method. The sender blocks until the receiver has answered its message. The receiver also explicitly states when it is prepared to answer a message. However, it does not specify the sender but only lists a set of possible method names. As soon as synchronization between sender and receiver takes place, the receiver executes the required method, using the parameters that the sender gave. The method returns a result (once again, a reference to an object), which is then passed back to the sender. After that~ sender and receiver both continue their own processing in parallel. Because of the above mechanisms, the only parallelism in the system is caused by the parallel execution of the bodies of the different objects. Inside each object everything happens sequentially and deterministically, so that the object is protected from the parallel and nondeterministic (and therefore 'dangerous') outside world. The interesting thing in POOL is that, like in other object- oriented languages, new objects can be created dynamically in arbitrary high numbers. In POOL, where as soon as an object is created, its body starts executing, this means that also the degree of parallelism can be increased dynamically. (Objects are never destroyed explicitly; rather, useless objects are removed by a garbage collector working behind the screens). In order to describe these dynamica~y evolving systems of objects in a static program, the objects are grouped into classes. All the objects in one class (the instances of the class) have the same names and types for their variables (of course, each has its own private set of variables) and they execute the same methods and body. In a program, a class definition is used to describe this internal structure of the objects. Whenever a new object is to be cre~ted, a class is named which serves as a blueprint.