Implementing Linking in Multiparty Sessions (Extended Abstract)

TL;DR

This paper introduces a novel implementation of linking in multiparty session types based on linear multirole logic, including new concepts like two-way and three-way linking, enhancing communication protocols in service-oriented programming.

Contribution

It generalizes linear logic to multirole logic, formulates a multiparty session type system, and implements advanced linking mechanisms for multiparty sessions in shared memory.

Findings

Developed a multiparty session type system based on LMRL.

Implemented linking mechanisms including two-way and three-way linking.

Linked multiple channels in multiparty sessions effectively.

Abstract

The fast growth of service-oriented programming (SOP) is evident in this day and age of the Internet, and handling communication is of paramount importance in SOP. Session types are a formalism that is proposed to specify interactions between communicating processes. In essence, a session type system is a kind of type system designed to enforce (through type-checking) that the involved processes communicate according to a chosen protocol specified as a session type. It is well-known that linear logic plays a pivotal role in the study of session types. For instance, various inference rules in linear logic can be interpreted as ways for constructing channels (used by communicating processes to send/receive messages.) A particularly interesting case is the cut-rule in linear logic, which can be interpreted as a way for connecting the ends of two matching channels to form a single new channel. This form of channel construction is often referred to as linking or (bi-directional) forwarding. We have generalized classical linear logic into classical linear multirole logic (LMRL), where the former can be seen as a special case of the latter involving only two roles. In LMRL, there is a cut-rule involving multiple sequents (instead of exactly two), which we call multiparty cut (mp-cut). We have also formulated a novel multiparty session type system directly based on LMRL. When implementing it, we need to find a way of connecting multiple channels that corresponds to mp-cut. In this paper, we describe an implementation of linking for multiparty sessions in the setting of shared memory. We also describe two novel concepts, two-way linking with residual and three-way linking, which can only be formulated in the setting of multiparty sessions. Notably, linking for binary sessions can be thought of as a specially optimized version of what is implemented for multiparty sessions.