Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page i 2008-10-24 #1 PROCESS ALGEBRA FOR PARALLEL AND DISTRIBUTED PROCESSING www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page ii 2008-10-24 #2 Chapman & Hall/CRC Computational Science Series SERIES EDITOR Horst Simon Associate Laboratory Director, Computing Sciences Lawrence Berkeley National Laboratory Berkeley, California, U. AIMS AND SCOPE This series aims to capture new developments and applications in the field of computational sci- ence through the publication of a broad range of textbooks, reference works, and handbooks. Books in this series will provide introductory as well as advanced material on mathematical, sta- tistical, and computational methods and techniques, and will present researchers with the latest theories and experimentation. The scope of the series includes, but is not limited to, titles in the areas of scientific computing, parallel and distributed computing, high performance computing, grid computing, cluster computing, heterogeneous computing, quantum computing, and their applications in scientific disciplines such as astrophysics, aeronautics, biology, chemistry, climate modeling, combustion, cosmology, earthquake prediction, imaging, materials, neuroscience, oil exploration, and weather forecasting.
PUBLISHED TITLES PETASCALE COMPUTING: Algorithms and Applications Edited by David A. Bader PROCESS ALGEBRA FOR PARALLEL AND DISTRIBUTED PROCESSING Edited by Michael Alexander and William Gardner www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page iii 2008-10-24 #3 PROCESS ALGEBRA FOR PARALLEL AND DISTRIBUTED PROCESSING EDITED BY MICHAEL ALEXANDER WILLIAM GARDNER www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page iv 2008-10-24 #4 Cover Image Credit: Intel Teraflops Research Chip Wafer from Intel, used with permission. Chapman & Hall/CRC Taylor & Francis Group 6000 Broken Sound Parkway NW, Suite 300 Boca Raton, FL 33487-2742 © 2009 by Taylor & Francis Group, LLC Chapman & Hall/CRC is an imprint of Taylor & Francis Group, an Informa business No claim to original U. Government works Printed in the United States of America on acid-free paper 10 9 8 7 6 5 4 3 2 1 International Standard Book Number-13: 978-1-4200-6486-5 (Hardcover) This book contains information obtained from authentic and highly regarded sources.
Reasonable efforts have been made to publish reliable data and information, but the author and publisher can- not assume responsibility for the validity of all materials or the consequences of their use. The authors and publishers have attempted to trace the copyright holders of all material reproduced in this publication and apologize to copyright holders if permission to publish in this form has not been obtained. If any copyright material has not been acknowledged please write and let us know so we may rectify in any future reprint. Except as permitted under U.
Copyright Law, no part of this book may be reprinted, reproduced, transmitted, or utilized in any form by any electronic, mechanical, or other means, now known or hereafter invented, including photocopying, microfilming, and recording, or in any information storage or retrieval system, without written permission from the publishers. For permission to photocopy or use material electronically from this work, please access www.com (http://www.com/) or contact the Copyright Clearance Center, Inc. (CCC), 222 Rosewood Drive, Danvers, MA 01923, 978-750-8400. CCC is a not-for-profit organization that pro- vides licenses and registration for a variety of users.
For organizations that have been granted a photocopy license by the CCC, a separate system of payment has been arranged. Trademark Notice: Product or corporate names may be trademarks or registered trademarks, and are used only for identification and explanation without intent to infringe. Library of Congress Cataloging-in-Publication Data Process algebra for parallel and distrubuted processing / editors, Michael Alexander and William Gardner. -- (Chapman & Hall/CRC computational science series) Includes bibliographical references and index.
Electronic data processing--Distributed processing. Alexander, Michael, 1970 Sept. Gardner, William, 1952- QA76.01’51--dc22 2008029295 Visit the Taylor & Francis Web site at http://www.com and the CRC Press Web site at http://www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page v 2008-10-24 #5 Contents Foreword vii Acknowledgments ix Introduction xi Editors xix Contributors xxi Part I Parallel Programming 1 1 Synthesizing and Verifying Multicore Parallelism in Categories of Nested Code Graphs 3 Christopher Kumar Anand and Wolfram Kahl 2 Semi-Explicit Parallel Programming in a Purely Functional Style: GpH 47 Hans-Wolfgang Loidl, Phil Trinder, Kevin Hammond, Abdallah Al Zain, and Clem Baker-Finch 3 Refinement of Parallel Algorithms 77 Fredrik Degerlund and Kaisa Sere Part II Distributed Systems 97 4 Analysis of Distributed Systems with mCRL2 99 Jan Friso Groote, Aad Mathijssen, Michel A. Usenko, and Muck van Weerdenburg 5 Business Process Specification and Analysis 129 Uwe Nestmann and Frank Puhlmann 6 Behavioral Specification of Middleware Systems 161 Nelson Souto Rosa v www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page vi 2008-10-24 #6 vi Contents 7 Abstract Machine for Service-Oriented Mobility 199 Hervé Paulino 8 Specifying and Implementing Secure Mobile Applications 235 Andrew Phillips Part III Embedded Systems 285 9 Calculating Concurrency Using Circus 287 Alistair A.
McEwan 10 PARS: A Process Algebraic Approach to Resources and Schedulers 331 MohammadReza Mousavi, Michel A. Reniers, Twan Basten, and Michel Chaudron 11 Formal Approach to Derivation of Concurrent Implementations in Software Product Lines 359 Sergio Yovine, Ismail Assayad, Francois-Xavier Defaut, Marcelo Zanconi, and Ananda Basu Index 403 www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page vii 2008-10-24 #7 Foreword This book brings together the state of the art in research on applications of process algebras to parallel and distributed processing. Process algebras constitute a successful field of computer science. This field has existed for some 30 years and stands nowadays for an extensive body of theory of which much has been deeply absorbed by the researchers in computer science.
Moreover, the theoretical achievements of the field are to a great extent justified by applications. The applications, in turn, strongly influence how the field evolves; some of the field’s success may be attributed to frequently addressing needs that arose in practice. Meanwhile, an explosion of complex systems of interacting components has been going on since the emergence of parallel and distributed processing. The complex- ity of the systems in question arises to a great extent from the many ways in which their components can interact.
In developing a complex system of interacting com- ponents, it is important to be able to describe the behavior of the system in a precise way at various levels of detail, and to analyze it on the basis of the descriptions. Pro- cess algebras were and are developed for that purpose. Roughly speaking, a process algebra provides a collection of operators, a collection of equational laws for these operators, and a mathematical model of these laws. The latter allows for the behavior of a system to be described as composed of the emergent behaviors of several inter- acting components and for the described behavior to be analyzed by mere algebraic calculations.
The advent of process algebras was marked by the introduction of CCS in the seminal monograph A Calculus of Communicating Systems by Milner, published as volume 92 of Springer’s Lecture Notes in Computer Science in 1980; the elaboration of CSP in the influential paper “A theory of communicating sequential processes” by Brookes, Hoare, and Roscoe, published in the Journal of the ACM in 1984; and the presentation of ACP as a strict algebraic theory in the paper “Process algebra for synchronous communication” by Bergstra and Klop, published in Information and Control in 1984. The very first applications of process algebras were mostly concerned with the description and analysis of communication protocols. Later on, the applications became more and more advanced. Often, they were concerned with the description and analysis of embedded systems, and more recently with Internet-based distributed systems.
The applications of process algebras led to a number of developments. The very first applications brought about the development of basic algebraic verifi- cation techniques, i., basic techniques to establish—on the basis of algebraic vii www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page viii 2008-10-24 #8 viii Foreword calculations—whether the actual behavior of a system is in agreement with its expected behavior. The construction of basic tools to facilitate description and anal- ysis followed. Later applications led to extensions of existing process algebras and the development of more advanced algebraic verification techniques.
Both make it easier to describe and analyze the behaviors of the systems often encountered in prac- tice nowadays: systems that may change their communication topology dynamically, systems that must react within a certain amount of time under certain circumstances, systems that exhibit at certain stages behavior that is stochastic in nature, systems that in their behavior depend on continuously changing variables other than time, etc. Experience with the existing process algebras led also to the development of spe- cial process algebras for the definition of the semantics of programming languages that support parallel programming or the design of microprocessors that utilize par- allelism to speed up instruction processing. It is difficult to foresee future developments and applications, yet some tendencies are noticeable. One area that is gaining momentum is specialized process algebras that are tailored to a certain paradigm for parallel or distributed computing or even to a certain technology for parallel or distributed computing.
This fits in with the tendency to apply process algebras to describe and analyze a prototype of a certain class of systems. Such applications can be useful in understanding certain aspects of the systems of an emerging class. However, the adequacy of the prototypes may be a major issue, because often drastic simplifications are needed to keep the description manageable. There is also a tendency to apply process algebras outside the realm of computing, which shows promise.
Many theoretical developments in the field of process algebras were collected by Bergstra, Ponse, and Smolka in the Handbook of Process Algebra, published in 2001. In 2005, a workshop was organized in Bertinoro, Italy, to celebrate the first 25 years of research in the field. Several special issues of the Journal of Logic and Algebraic Programming are devoted to this workshop. Despite the importance of applications of process algebras for the success of the field, both the handbook and these spe- cial issues concentrate strongly on the theoretical achievements.
This shortcoming is compensated for in a splendid way by this book, which brings together the state of the art in research on applications of process algebras. Kees Middelburg Programming Research Group University of Amsterdam, the Netherlands www.com Alexander/Process Algebra for Parallel and Distributed Processing C6486 C000 Finals Page ix 2008-10-24 #9 Acknowledgments The editors are very grateful to those listed below who served as peer reviewers for contributions to this book. Their diligent and conscientious efforts not only helped us to make the final selection of chapters but also provided numerous valuable sug- gestions to the authors, resulting in a high-quality collection. Luca Aceto John Derrick School of Computer Science Department of Computer Science Reykjavik University University of Sheffield Reykjavik, Iceland Sheffield, South Yorkshire, United Kingdom Lorenzo Bettini Dipartimento di Informatica Gaétan Hains Universita’ di Torino Laboratoire d’Algorithmique, Torino, Italy Complexité et Logique Tommaso Bolognesi University of Paris-Est CNR—Istituto di Scienza e Tecnologie Créteil, France dell’Informazione “A.
Faedo” and Pisa, Italy SAP Labs France Gerhard Chroust Mougins, France Systems Engineering and Automation Institute of Systems Sciences Michael G. Hinchey Johannes Kepler University of Linz Lero—The Irish Software Engineering Linz, Austria Research Centre Philippe Clauss University of Limerick Scientific Parallel Computing Limerick, Ireland and Imaging Université Louis Pasteur Thomas John Strasbourg, France Department of Information Systems Vienna University of Economics and Pedro R. D’Argenio Business Administration Department of Computer Science Vienna, Austria Facultad de Matemática, Astronomia y Fisica Kenneth B. Kent Universidad Nacional de Faculty of Computer Science Córdoba—CONICET University of New Brunswick Córdoba, Argentina Fredericton, New Brunswick, Canada ix www.