Composition and Decomposition of Multiparty Sessions

Description

Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty sessions enjoy lock-freedom. We look at multiparty sessions as open systems by allowing one to compose multiparty sessions by transforming two of their participants into a pair of coupled gateways, forwarding messages between the two sessions. Gateways need to be compatible. We show that the session resulting from the composition can be typed, and its type can be computed from the global types of the starting sessions. As a consequence, lock-freedom is preserved by composition. Compatibility between global types is necessary, since systems obtained by composing sessions with incompatible global types have locks (or they are not sessions). We also define direct composition, which allows one to connect two global types without using gateways. Finally, we propose a decomposition operator, to split a global type into two, which is the left inverse of direct composition. Direct composition and decomposition on global types prepare the ground for a novel framework allowing for the modular design and implementation of distributed systems.

Abstract

International audience

Additional details