Giới thiệu về A Distributed Pi-Calculus (aDpi) cho các Hệ thống Phân tán và Tác tử Di động

This page intentionally left blank www.com A DISTRIBUTED pi-calculus Distributed systems are fast becoming the norm in computer science. Formal mathematical models and theories of distributed behaviour are needed in order to understand them. This book proposes a distributed pi-calculus called aDpi, for describing the behaviour of mobile agents in a distributed world. It is based on an existing formal language, the pi-calculus, to which it adds a network layer and a primitive migration construct.

A mathematical theory of the behaviour of these distributed systems is developed, in which the presence of types plays a major role. It is also shown how, in principle, this theory can be used to develop verification techniques for guaranteeing the behaviour of distributed agents. The text is accessible to computer scientists with a minimal background in discrete mathematics. It contains an elementary account of the pi-calculus, and the associated theory of bisimulations.

It also develops the type theory required by aDpi from first principles.com A DISTRIBUTED pi-calculus M ATT H E W HE NNE SSY www.com CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK Published in the United States of America by Cambridge University Press, New York www.org Information on this title: www.org/9780521873307 © Cambridge University Press, 2007 This publication is in copyright. Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published in print format 2007 ISBN-13 978-0-511-27564-7 eBook (NetLibrary) ISBN-10 0-511-27564-1 eBook (NetLibrary) ISBN-13 978-0-521-87330-7 hardback ISBN-10 0-521-87330-4 hardback Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate.com To the memory of John and Ray www.com Contents Preface ix Acknowledgements xvii 1 Inductive principles 1 1.3 Bisimulation equivalence 6 2 The asynchronous PI-CALCULUS 10 2.1 The language aPi 10 2.2 Reduction semantics for aPi 16 2.3 An action semantics for aPi 27 2.4 A coinductive behavioural equivalence for aPi 34 2.6 An observational lts for aPi 43 2.7 Justifying bisimulation equivalence contextually 47 2.8 Questions 52 3 Types for API 55 3.2 Typechecking with simple types 60 3.3 Properties of typechecking 65 3.4 Types as capabilities 72 3.5 Questions 93 4 Types and behaviour in aPi 96 4.1 Actions-in-context for aPi 98 4.2 Typed bisimulation equivalence 112 4.3 Questions 122 vii www.com viii Contents 5 A distributed asynchronous PI-CALCULUS 124 5.1 The language aDpi 127 5.2 Access control types for aDpi 139 5.3 Subject reduction for aDpi 159 5.4 Type safety for aDpi 169 5.5 Distributed consistency of local channels 185 5.6 Questions 191 6 Behavioural equivalences for aDpi 194 6.1 Actions-in-context for aDpi 195 6.2 Typed bisimulation equivalence for aDpi 200 6.4 Servers and clients 215 6.6 Typed contextual equivalences 226 6.7 Justifying bisimulation equivalence contextually in aDpi 230 6.8 Questions 242 Sources 244 List of figures 248 Notation 250 Bibliography 254 Index 257 www.com Preface From ATM machines dispensing cash from our bank accounts, to online shopping websites, interactive systems permeate our everyday life. The underlying technology to support these systems, both hardware and software, is well advanced.

However design principles and techniques for assuring their correct behaviour are at a much more primitive stage. The provision of solid foundations for such activities, mathematical models of system behaviour and associated reasoning tools, has been a central theme of theoretical computer science over the last two decades. One approach has been the design of formal calculi in which the fundamental concepts underlying interactive systems can be described, and studied. The most obvious analogy is the use of the λ-calculus as a simple model for the study of sequential computation, or indeed the study of sequential programming languages.

CCS (a Calculus for Communicating Systems) [28] was perhaps the first calculus proposed for the study of interactive systems, and was followed by numerous variations. This calculus consists of: • A simple formal language for describing systems in terms of their structure; how they are constructed from individual, but interconnected, components. • A semantic theory that seeks to understand the behaviour of systems described in the language, in terms of their ability to interact with users. Here a system consists of a finite number of independent processes that inter- communicate using a fixed set of named communication channels.

This set of channels constitutes a connection topology through which all communication takes place; it includes both communication between system components, and between the system and its users. Although successful, CCS can only describe a very limited range of systems. The most serious restriction is that for any particular system its connection topology is static. However modern interactive systems are highly dynamic, particularly when one considers the proliferation of wide area networks.

Here computational ix www.com x Preface entities, or agents, are highly mobile, and as they roam the underlying network they forge new communication links with other entities, and perhaps relinquish existing links. The pi-calculus [9, 29] is a development from CCS that seeks to address at least some dynamic aspects of such agents. Specifically it includes the dynamic generation of communication channels and thus allows the underlying connection topology to vary as systems evolve. Just as importantly it allows private communication links to be established and maintained between agents, which adds considerably to its expressive power.

Indeed the pi-calculus very quickly became the focus of intensive research, both in providing for it a semantic understanding, and in its promotion as a suitable foundation for a theory of distributed systems; see [39] for a comprehensive account. But many concepts fundamental to modern distributed systems, in particular those based on local area networks, are at most implicit in the pi-calculus. Perhaps the most obvious is that of domain, to be understood quite generally as a locus for computational activity. Thus one could view a distributed system as consisting of a collection of domains, each capable of hosting computational processes, which in turn can migrate between domains.

The aim of this book is to develop an extension of the pi-calculus in which these domains have an explicit representation. Of course when presented with such a prospect there is a bewildering number of concerns on which we may wish to focus. For example: • What is the role of these domains? • How are they to be structured? • How is interprocess communication to be handled? • How is agent migration to be described? • Can agents be trusted upon entry to a domain? Indeed the list is endless. Here our approach is conservative.

We wish to develop a minimal extension of the pi-calculus in which the concept of domain plays a meaningful, and non-trivial role. However their presence automatically brings a change of focus. The set of communication channels that in the pi-calculus determines the interprocess communication topology now has to be reconciled with the distribution topology. Following our minimalistic approach we decide on a very simple distribution topology, namely a set of independent and non-overlapping domains, and only allow communication to happen within individual domains.

This makes the communication channels of the pi-calculus into local entities, in the sense that they only have significance relative to a particular domain. Indeed we will view them as a particularly simple form of local resource, to be used by www.com Preface xi migrant agents. Thus we view our extension of the pi-calculus, called aDpi – for asynchronous Distributed pi-calculus, as a calculus for distributed systems in which • dynamically created domains are hosts to resources, which may be used by agents • agents reside in domains, and may migrate between domains for the purpose of using locally defined resources. Types and type inference systems now form an intrinsic part of computer science.

They are traditionally used in programming languages as a form of static analysis to ensure that no runtime errors occur during program execution. Increasingly sophisticated type-theoretic concepts have emerged in order to handle modern programming constructs [36]. However the application of type theory is very diverse. For example types can be used to • check the correctness of security protocols [12] • detect deadlocks and livelocks in concurrent programs [26] • analyse information flow in security systems [22].

In this book we also demonstrate how type systems can be developed to manage access control to resources in distributed systems. In aDpi we can view domains as offering resources, modelled as communication channels, to migrating agents. Moreover a domain may wish to restrict access to certain resources to selected agents. More generally we can think of resources having capabilities associated with them.

In our case two natural capabilities spring to mind: • the ability to update a resource, that is write to a communication channel • the ability to look up a resource, that is read from a communication channel. Then domains may wish to distribute selectively to agents such capabilities on its local resources. We could develop a version of aDpi in which the principal values manipulated by agents are these capabilities. But this would be a rather complex language, having to explicitly track their generation, management, and distribution.

Instead we show that these capabilities can be implicitly managed by using a typed version of aDpi. Moreover the required types are only a mild generalisation of those used in a type inference system for ensuring the absence of runtime errors, when aDpi systems are considered as distributed programs. The behavioural theory of processes originally developed for CCS [28] based on bisimulations, has been extended to the pi-calculus, and can be readily extended to aDpi. Indeed the framework is quite general.

The behaviour of processes can be described, independently of the syntax, in terms of their ability to interact with other processes, or more generally with their computing environment. The form www.com xii Preface these interactions take depend on the nature of the processes, and in general will depend on the process description language. They can be described mathematically as relations between processes, with l P −→ Q meaning the process P by interacting with its environment can be transformed into the process Q. The label l serves to record the kind of interaction involved, and perhaps some data used in the interaction.

For example one can easily imagine the behaviour of an ATM machine being described in this manner, in terms of its internal states, and the evolution between these states depending of the different kinds of interactions with a customer. Such a behavioural description is formalised as a labelled transition system, or lts, and often refered to as an operational semantics. The theory of bisimulations enables one to take such abstract behavioural descriptions of processes and generate a behavioural equivalence between processes. Intuitively P≈Q (1) will mean that no user, or computing environment, will be able to distinguish between P and Q using the interactions described in their behavioural descriptions.

However the use of types in aDpi has a serious impact on this general behavioural framework, particularly as these types implicitly represent the limited capabilities that agents have over resources. In other words these types limit the ways in which agents can interact with other agents. Consequently whether or not two agents are deemed equivalent will depend on the current distribution of the capabilities on the resources in the system. The third and final aim of this book is to address this issue.

We demonstrate that the general theory of bisimulations can be adapted to take the presence of types into account. We develop a relativised version of behavioural equivalence in which judgements such as (1) can never be made in absolute terms, but relative to a description of current capabilities. Moreover we will show that the proof techniques associated with standard bisimulations, based on coinduction, can be adapted to this more general framework, at least in principle.