Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Relaxed Choices in Bottom-Up Asynchronous Multiparty Session Types

Ivan Prokić, Simona Prokić, Silvia Ghilezan, Alceste Scalas, Nobuko Yoshida

TL;DR

The paper extends bottom-up asynchronous multiparty session types to support multi-recipient input/output, enabling accurate modelling of decentralised federated learning protocols. It introduces an extended calculus with a concurrent input construct and preserves essential properties—safety, deadlock-freedom, liveness, and session fidelity—via a robust typing system and subtyping relation. The results demonstrate how multi-recipient communication can be analysed and verified within a bottom-up framework, bridging a gap between theoretical session types and real-world distributed protocols. The work lays a foundation for applying typing-based verification to federated learning and related async, multi-party communication scenarios, with future directions including model-checking typing environments and exploring decidable approximations of key properties.

Abstract

Asynchronous multiparty session types provide a formal model for expressing the behaviour of communicating processes and verifying that they correctly implement desired protocols. In the ``bottom-up'' approach to session typing, local session types are specified directly, and the properties of their composition (e.g. deadlock freedom and liveness) are checked and transferred to well-typed processes. This method allows expressing and verifying a broad range of protocols, but still has a key limitation: it only supports protocols where every send/receive operation is directed towards strictly one recipient/sender at a time. This makes the technique too restrictive for modelling some classes of protocols, e.g. those used in the field of federated learning. This paper improves the session typing theory by extending the asynchronous ``bottom-up'' approach to support protocols where a participant can choose to send or receive messages to/from multiple other participants at the same time, rather than just one at a time. We demonstrate how this extension enables the modeling and verification of real-world protocols, including some used in federated learning. Furthermore, we introduce and formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system, revealing interesting dependencies between these properties in the presence of a subtyping relation.

Relaxed Choices in Bottom-Up Asynchronous Multiparty Session Types

TL;DR

The paper extends bottom-up asynchronous multiparty session types to support multi-recipient input/output, enabling accurate modelling of decentralised federated learning protocols. It introduces an extended calculus with a concurrent input construct and preserves essential properties—safety, deadlock-freedom, liveness, and session fidelity—via a robust typing system and subtyping relation. The results demonstrate how multi-recipient communication can be analysed and verified within a bottom-up framework, bridging a gap between theoretical session types and real-world distributed protocols. The work lays a foundation for applying typing-based verification to federated learning and related async, multi-party communication scenarios, with future directions including model-checking typing environments and exploring decidable approximations of key properties.

Abstract

Asynchronous multiparty session types provide a formal model for expressing the behaviour of communicating processes and verifying that they correctly implement desired protocols. In the ``bottom-up'' approach to session typing, local session types are specified directly, and the properties of their composition (e.g. deadlock freedom and liveness) are checked and transferred to well-typed processes. This method allows expressing and verifying a broad range of protocols, but still has a key limitation: it only supports protocols where every send/receive operation is directed towards strictly one recipient/sender at a time. This makes the technique too restrictive for modelling some classes of protocols, e.g. those used in the field of federated learning. This paper improves the session typing theory by extending the asynchronous ``bottom-up'' approach to support protocols where a participant can choose to send or receive messages to/from multiple other participants at the same time, rather than just one at a time. We demonstrate how this extension enables the modeling and verification of real-world protocols, including some used in federated learning. Furthermore, we introduce and formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system, revealing interesting dependencies between these properties in the presence of a subtyping relation.
Paper Structure (16 sections, 22 theorems, 19 equations, 5 figures)

This paper contains 16 sections, 22 theorems, 19 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Modelling an aynchronous decentralised federated learning protocol.
  3. Contributions and outline of the paper.
  4. The Calculus
  5. Syntax
  6. Session Reductions and Properties
  7. Types and Typing Environments
  8. Typing Environment Reductions and Properties
  9. Subtyping
  10. The Typing System and Its Properties
  11. Properties of our typing system.
  12. Related and Future Work
  13. Related work.
  14. Conclusions and future work.
  15. Proofs of \ref{['sec:tsu']}
  16. ...and 1 more sections

Key Result

Proposition 11

If $\Gamma$ is safe/deadlock-free/live and $\Gamma \longrightarrow \Gamma'$, then $\Gamma'$ is safe/deadlock-free/live.

Figures (5)

  • Figure 1: An execution of the generic decentralised one-shot federated learning algorithm.
  • Figure 2: Syntax of sessions, processes, and queues.
  • Figure 3: Reduction relation on sessions.
  • Figure 4: Structural (pre)congruence rules for queues, processes, and sessions.
  • Figure 5: Typing rules for values, queues, and for processes and sessions.

Theorems & Definitions (41)

  • Example 1: Concurrent input
  • Example 2: Modelling a centralised FL protocol implementation
  • Example 3: Modelling a decentralised FL protocol implementation
  • Definition 4: Session behavioral properties
  • Example 5: A safe but non-live session
  • Example 6: A live but unsafe session
  • Definition 7
  • Definition 8: Typing environment reduction
  • Definition 9: Typing environment behavioral properties
  • Example 10
  • ...and 31 more