Recherche — Research

Dπ is a simple distributed extension of the π-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations.

In this paper we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes.

Passports allow locations to control incoming processes. This induces a major modification to the possible observations which can be made of agent-based systems. Using the type system we describe these observa- tions, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.

Dpi is a distributed version of the pi-calculus, in which processes are explicitly located, and a migration construct may be used for moving between locations. We argue that adding a recursion operator to the language increases significantly its descriptive power. But typing recursive processes requires the use of potentially infinite types.

We show that the capability-based typing system of Dpi can be extended to co-inductive types so that recursive processes can be successfully supported. We also show that, as in the pi-calculus, recursion can be implemented via iteration. This translation improves on the standard ones by being compositional but still requires co-inductive types and comes with a significant migration overhead in our distributed setting.

Résumé

Le calcul réparti est de plus en plus utilisé bien qu'il reste très mal maîtrisé. Cette thèse porte sur le Dpi-calcul, une extension simple du pi-calcul dans laquelle tous les processus sont placés dans des localités afin de décrire leur répartition. Dans ce calcul, les processus peuvent communiquer localement et migrer entre localités. À côté des canaux de communication et des localités, on identifie une nouvelle famille d'identifiants, les passeports, permettant un contrôle fin des migrations de processus : un processus doit disposer d'un passeport adéquat pour entrer dans une localité.

Afin de structurer le calcul, on met en place un système de types qui associe un type à chaque identifiant pour vérifier qu'un processus n'utilise que les droits qu'il possède. L'ordre de sous-typage sur les types est étendu aux types de passeports suivant les localités d'origine des processus migrant. On démontre que cet ordre admet des bornes inférieures sous certaines conditions. On prouve également que les processus se conformant à cette politique de typage conservent cette propriété au cours de leurs réductions.

On étudie aussi l'équivalence observationnelle : quand des processus exhibent-ils des comportements indiscernables pour un observateur ? En présence de passeports, il est indispensable d'imposer à l'observateur d'être loyal, c'est-à-dire d'exiger la possession de passeports pour observer les communications ayant lieu dans les localités correspondantes. Ces contraintes définissent une congruence dite barbue loyale. On développe ensuite un système de transitions étiquetées tel que la bisimilarité loyale engendrée coïncide avec cette congruence barbue loyale.

Abstract

Distributed computation is increasingly used even though it is still only loosely controlled. This thesis deals with the Dpi-calculus, a simple extension of the pi-calculus in which processes are located to describe distribution. In this calculus, processes can communicate locally and migrate between locations. Beside communication channels and locations, a new family of identifiers, passports, is added to provide a fine-grained control over process migrations: any process must own an appropriate passport to enter a location.

The calculus is structured through a type system which associate a type to every identifier and allows to check that a process uses only the rights it owns. The subtyping order over types is extended to passport types by considering the origin of migrating processes. The existence of greatest lower bounds is shown under some conditions. The fact that well-typed processes stay well-typed whenever they reduce is also proved.

Observational equivalence is also studied: when do process behave identically from the point of view of some observer? In a calculus equipped with passports, it is mandatory to ask the observer to play fair, i.e. to require that it owns some passports to observe any behaviour in the corresponding locations. These constraints define a fair barbed congruence. A labelled transition system is subsequently developed so that the bisimilarity it generates coincides with the fair barbed congruence.