Forwarders as Process Compatibility, Logically

TL;DR

This paper introduces forwarder logic, a new logical framework that generalizes arbiters in multiparty session types, providing a proof-theoretic characterization of system compatibility and deadlock freedom.

Contribution

It develops forwarder logic, extending coherence proofs, to characterize multiparty compatibility in concurrent systems within a logical framework.

Findings

Forwarder logic satisfies cut-elimination.

It generalizes coherence to multiparty protocols.

Provides an elegant proof-theoretic characterization of deadlock freedom.

Abstract

Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwarder logic, a fragment of classical linear logic still satisfying cut-elimination. Our main result is summarized as follows: forwarders generalize coherence and give an elegant proof-theoretic characterization of multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs.