Research directions

INRIA Rocquencourt has worked in the following directions.

• Distributed Join-Calculus.

  Version 1.04 has been released in June by Fournet and Maranget. This prototype includes a distributed implementation of the join-calculus, which is about 20000 lines of Caml-light code. The system comprises a byte-code compiler, a run-time interpreter, an on-line documentation, a tutorial and many examples. As demo programs, we have a distributed calculation of the Mandelbrot set and several games. An article on the type-inference algorithm and a demo were presented at CONCUR'97 [FLMR97] and at TACS'97 [Le97]. The system is available at http://www.pauillac.inria/join/.

• Equivalences in the Join-Calculus

  A new theory of bisimulation has been developed by Boreale (Roma), Fournet (INRIA) and Laneve (Bologna). They consider open terms of the join calculus, and define two bisimulation, weak and asynchronous, which are both refinments of the observational equivalence. This gives a compositional sense to the interaction of the terms of the join-calculus with contexts, and is a start point to logical systems for reasoning on join-terms. An article has been submitted to a conference, the work has been presented at the Confer Workshop in Amsterdam [BFL98].

  More generally, many equivalences have been proposed for process algebra for the study of convergence, security or fairness. Gonthier started a comparison of equivalences used both in the pi and join calculus, mostly based on reduction semantics, observation of barbs and preservation by contexts. Many variants appear according to the way these elementary constructs are combined. But fortunately many lead to a same result. One shows that fair-testing is connected to coupled bisimulation, or that omega-limit bisimulation is also related to single-barb gfp bisimulation. This provides new proof techniques and a better understanding of process calculi. An article is in preparation, the work has been presented at the Confer Workshop in Amsterdam [Gon98].

• Concurrency and Security

  Secure implementation of communication in the join calculus has been developed by Abadi (DEC/SRC), Fournet and Gonthier. It is easy to write secure protocols when lexical scope is guaranteed, but one needs cryptographic means to enforce a secure lexical scope discipline. By compositionality, two protocols can be considered: one based on the redefinition of secure emission/reception primitives, another one based on firewalls for some locations. The correctness proofs are based on bisimulation techniques.

  A presentation by Fournet has been made at the DARPA workshop on Foundations for Secure Mobile Code, March 26-28 mars in Monterey [Fou97], and at the Confer meeting in Amsterdam. An article is in preparation [AFG98].

• Distributed Garbage Collection

  F. le Fessant designed and implemented a scalable distributed GC algorithm which can collect cycles. It is a feasible implementation of an old idea by Hughes. An article has been sent to a conference [leF97].

• Expressivity and types

  The $\pi$-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the $\pi$-calculus with asynchronous output and no choice. Palamidessi recently proved that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. However there are `good' encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice. One can investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all criteria, but various `good' candidates for the third encoding -- inspired by an existing distributed implementation -- invalidate one or the other criterion. This study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes [Ne97a].

  We investigated confluence properties for concurrent systems of message-passing processes, because such properties have proved to be useful for a variety of applications, ranging from reasoning about concurrent objects to mobile and high-speed telecommunication protocols. Confluence means that for every two computations starting from a common system state, it is possible to continue the computations, so to reach a common state again. In order to prove confluence for a given system, we are required to demonstrate that for all states reachable by computation from the starting state, the 'flowing together' of possible computations is possible. However, it is possible to prove confluence properties for concurrent systems without having to generate all reachable states by use of a type system that supports a static analysis of possible sources of non-confluence. In message-passing systems, confluence is invalidated whenever two processes compete for communication with another process. We may statically check the occurrence of such situations by reducing them to the concurrent access on a shared communication port. For the technical development, we focus on the setting of a polarized pi-calculus, where we formalize the notion of port-uniqueness by means of overlapping-free context-redex decompositions. We then present a type system for port-uniqueness that, taking advantage of a subject reduction property, yields a sufficient criterion for guaranteeing confluence. This work is published in the Proceedings of FMICS'97 [NS97].