next up previous contents
Next: Basic properties and types Up: Calculi Previous: Calculi

New Calculi for mobile and distributed processes

Boudol introduced the blue calculus [Bou97a]. It proposes a synthesis of the lambda-calculus and the pi-calculus. This calculus contains a new type system which incorporates both the notion of functional type and that of sort for communication channels. This type system has been further studied by Dal-Zilio in [Dal97], where it is shown to extend naturally to an implicit polymorphic type system à la ML.

These types only express very weak properties of the behaviour of processes. For instance, one cannot guarantee the absence of deadlock; here we mean by deadlock that a process calls a resource that will never become available. To overcome this lack of expressiveness, G. Boudol has proposed in [Bou97b] a more refined notion of type, which incorporates a part of Hennessy-Milner logic: a resource declaration is given a modal type indicating that a value of a certain type is available on a certain name. This new type system is shown to enjoy the subject reduction property. This research will be hopefully extended with a proof that typability implies the absence of deadlock.

In [Am97] Amadio presents a model of mobility based on the pi-calculus. He relies on an elementary typing, which ensures that in a system, at every moment, to a given name there corresponds a unique resource (whose state can change from one call to another, however). In this way, one can consider a site - or a locality - as a name associated to a resource whose state is either `alive' or `dead'. Amadio develops on this basis a formalism to speak about migration and failures, and he provides reasoning methods which use a notion of bisimulation.

In [RieHen97a] Riely and Hennessy studied in detail location failure for distributed processes. A language is defined in which threads are run at distributed locations, and from this a semantic theory is developed using the basic notions of observer and experiment . Roughly, an observer interacts with a distributed process either by synchronizing with one of its threads or by halting one of its locations; two programs are equivalent if they present the same structure of observations, evolving over time. The main result of this work is to provide an alternative characterization of this observational equivalence which is suitable to automatic verification. This is done using a temporal logic to characterize the interdependence between synchronization events and failures.

In [RieHen97b] Riely and Hennessy present a more expressive language, which includes agent migration, location failure and a rich system of capabilities used to tag communicated data. Intuitively, when the name, say, of a location is communicated, a set of capabilities for that location is communicated at the same time; these may include the capability to read data, to write data, to halt the location, to migrate to it, or to allocate fresh resources at it. We present a series of type systems for this language and show, through examples, that very expressive type systems are necessary in order to be able to type many important practical programs.

Lavatelli works on the definition of an algebraic semantics of $\lambda_r$ based on approximants, in the flat scenario (where both abstractions and deadlock are observable), which turns out to be sound. Work in progress concerns completeness. The aim is to use these results as intermediate steps in the characterization of the flat semantics through an intersection type system. Another work in progress, by Lavatelli and Curien, concerns the use of techniques of logical relations to compare the inequational theories of two models of $\lambda_r$ that have arisen naturally when trying to give a semantics to $\lambda_r$.

Now, Parrow and Victor have also developed the update-calculus where processes can perform update actions with side effects, and a scoping operator controls the extent of the effects [PV97]. In this way it incorporates fundamental concepts from imperative languages, concurrent constraints and from functional formalisms. Structurally it is similar to but simpler than the pi-calculus; it has only one binding operator and a symmetry between inpout and output.

Finally, in [SWP97], Sewell, Wojciechowski and Pierce have proposed a simple calculus of agents that can migrate between sites and can interact by both location dependent and location independent message passing. It has a precise reduction semantics. Implementations of the location independent primitives can be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. This allows the algorithms to be stated and understood precisely, a clean implementation strategy for prototype languages (such an encoding can be realized as one phase of a compiler), and reasoning. It also provides a setting in which multiple communication mechanisms can coexist gracefully.

[[Am97]] R. Amadio.
An asynchronous model of locality, failure, and process mobility.
In Proc. Coordination 97, Springer Lect. Notes in Comp. Sci. 1282, 1997.

[[AmCou97]] R. Amadio and S. Coupet-Grimal.
Analysis of a guard condition in type theory (preliminary report).
Technical Report TR 1997.245. Also RR-3300 INRIA, Université de Provence (LIM), 1997.

[[Bou97a]] G. Boudol.
The pi-calculus in direct style.
In Proceedings POPL'97, 1997.

[[Bou97b]] G. Boudol.
Typing the use of resources in a concurrent calculus.
In Proceedings ASIAN'97, LNCS 1345, 1997.

[[Dal97]] S. Dal-Zilio.
Implicit polymorphic type system for the blue calculus.
Technical Report RR-3244, INRIA, 1997.

[[RieHen97a]] J. Riely and M. Hennessy.
Distributed processes and location failures.
Technical Report 2/97, 1997.
Extended abstract presented at ICALP97.

[[RieHen97b]] J. Riely and M. Hennessy.
A typed language for distributed mobile processes.
In Proc. POPL'98, ACM Conference on Principle of Programming Languages, San Diego.

[[PV97]] J. Parrow and B. Victor.
The update calculus (full version).
Technical Report DoCS 97/93, Department of Computer Systems, Uppsala University, Sweden, Sept. 1997.
Extended abstract to appear in the proceedings of AMAST'97.

[[SWP97]] Peter Sewell, Pawe\l 
 T. Wojciechowski, and Benjamin C. Pierce.
Location independence for mobile agents.
Submitted for publication, 1997.

next up previous contents
Next: Basic properties and types Up: Calculi Previous: Calculi