Maxime Gamboni

We propose a general type notation, formal semantics and a sound, compositional, and decidable type system to characterise some liveness properties of distributed systems.

In the context of mobile processes, we define two concepts, activeness (ability to send/receive on a channel) and responsiveness (ability to reliably conduct a conversation on a channel), that make the above properties precise.

The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process.

Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or conversations (where the protocol may permit more than one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns.

Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.

In mobile processes, a channel can be active (able of sending/receiving) or responsive (provide a reply to, or parameters for, a request), or both. It has a multiplicity such as ω (usable arbitrarily many times) or plain (unrestricted behaviour).

The context the process will be running in is similarly described, specifying to what extent third-party processes may interfere.

We outline semantic definitions of the properties, and a sound, compositional, type system enjoying subject-reduction, which verifies that, in a given process, channels behave as specified, and indicates, when applicable, what should be provided to the process before the properties hold.

In this short presentation we outline our current research on integrating choice and responsiveness, which permits statically guaranteeing responsiveness on process constructs that are necessary for encoding data, but that could not be analysed by existing works. Moreover, conditional properties permit analysing components of a system individually. We are developing a general type notation, formal semantics and a sound type system which are able to recognise most common kinds of data encodings such as Booleans, numbers, lists, and so on, as well as any non-recursive function on them.

This presentation is about a number of type systems and algorithms designed to guarantee a number of desirable properties for a typical client-server interaction.

In particular, we want the server to be ready to handle arbitrarily many requests and at any time, all requests should eventually get answered, the processing of a request should eventually terminate, and given a protocol governing negotiation of resources between the client and the server, both parties should obey to it.

Having given and informal description of these properties as well as the language being used (the pi-calculus), I will describe and compare a number of type systems enforcing these properties in processes:

I will start by describing and demonstrating an existing implementation of a type system written by Naoki Kobayashi, "TyPiCal".

Secondly, I will describe the work António Ravara and I have been doing on the topic.

Finally, I will cover a number of other type systems (Deng and Sangiorgi's type system for termination, and Kobayashi and Sangiorgi's lock-freedom analysis), comparing their expressive power.

We propose a general type notation, formal semantics and a sound, compositional, and decidable type system that characterise some liveness properties of distributed systems supporting choice. When such systems are specified using mobile processes, it is important to provide a number of liveness guarantees, such as, from a client's point of view, ``If I send a request, will it eventually be received? Will it eventually be processed, and will I eventually obtain an answer?'', or, from a server's point of view, ``Will I eventually receive a request? Will my clients respect the protocol?''.

We define two concepts, activeness (ability of sending/receiving on a channel) and responsiveness (ability to reliably conduct a conversation), that make the above properties precise, in particular what ``eventually'' and ``respect the protocol'' mean. The semantic definitions are respected by the type system, in the sense that the logical statements it outputs are correct descriptions of the process, according to the semantics.

In process calculi, processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or of object-oriented style programming (where a call matches one method out of a set). Our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns.

Finally, compositionality features are offered through the use of conditional properties that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.

In this paper we propose a new way of writing channel and process types for the π-calculus, as well as a semantic description of two liveness properties of channels: activeness (whether the process is able to receive or send a request on the channel) and responsiveness (if a receiver is able to eventually reply to a request).

Any combination of these properties can be associated independently to input and output occurrences of names in a process and to their parameters (thus specifying what a name polar may expect from its complement).

The type notation we propose puts an emphasis on protocols: A channel type segregates the server (input) side behaviour from the client (output) behaviour, and the type for a process explicitly specifies how third-party processes are permitted to interact and interfere with it.

We conclude the paper with a survey of some works on related topics along with encodings of the various type notations.

In order to write encodings of complex data structures in π-calculus we need guarantees that certain fundamental properties of communication are preserved when interacting with encoded processes. These include non-interference of the data transmission subprocess, responsiveness for data decoding requests, unicity of the transmitted value and immutability of a transmitted value. We propose a type system of π-calculus processes for which any typable process satisfies the above requirements.

In this thesis I present a generic semantic framework and sound type system suited for analysing a wide variety of behavioural properties in π-calculus processes, both liveness properties such as activeness (a generalisation of receptiveness), termination and reachability, and safety properties such as determinism and isolation.

Dependency analysis is a central ingredient of this framework, implemented by dependency statements describing process properties conditional on some resources to be provided by third-party processes. Dependency statements are used as elementary ingredients of behavioural statements, logical statements that precisely characterise negotiation of resources between a process and its environment. Dependency analysis provides this framework with powerful compositionality: when arranging pre-analysed (typed) components together, the resulting process' type can be directly derived from those of the components, with no need to re-analyse the entire process. Behavioural statements also integrate primitives for describing selection (choices made by a process) and branching (choices offered by a process).

The type system, parametrised with elementary rules giving the essence of the desired properties and channel types giving communication protocols to be used on communication channels, automatically constructs a behavioural statement by automatically analysing processes.

We study the expressive power of asynchronous π-calculus with nested variants (π_a^v) and of TyCO by means of encodings.

TyCO can be seen as a sub-calculus of π_a^v, in that TyCO only allows one level of variants, the only difference being that π_a^v requires a separate construct for analysing an input while in TyCO input and value analysis are tightly bound. Still, we can give an encoding (embedding) that is fully abstract and good.

We propose a fully abstract encoding from π_a^v to TyCO.

Errata