Source-linked AI summary
Parameterised Multiparty Session Types
Pierre-Malo Denielou, Nobuko Yoshida, Andi Bejleri, Raymond Hu
TL;DR
Protocols for distributed applications and parallel algorithms may have participant counts or interaction structures that are unknown until run time. The paper combines dependent types with multiparty sessions and projects parameterised global types onto generic endpoint generators. It reports decidable type checking and type safety and deadlock freedom for well-typed processes.
Problem
Many protocols have participant counts, message counts, or interaction structures that are not fixed at design time.
Source: §1 · pp. 1–2Method
The paper uses dependent types, including primitive recursion, and projects parameterised global types onto generic endpoint generators for typing processes.
Source: §1 · p. 3, §2.1 · p. 4Results
The system provides decidable type checking and guarantees type safety and deadlock freedom for well-typed processes in parameterised multiparty protocols.
Source: §1 · p. 3Takeaways & Limitations
Examples include process topologies from parallel algorithms, including a butterfly network, and an asynchronous session-initialisation extension applied to Web services.
Source: §1 · p. 3The process example takes the range of n to be n ≥2.
Source: §2.5 · p. 9
Abstract
from arXiv · showhide
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from G\"odel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
1. Introduction
The introduction motivates parameterised multiparty session types for protocols whose participants and interaction structures may vary at run time. It proposes dependent types and a projection method to specify these protocols and statically check their implementations.
1. Introduction
- The motivating settings include parallel algorithms such as FFT and Web services involving arbitrary numbers of participants.Communication topology or available threads may vary with machine resources.Source: §1 · pp. 1–2
- Global protocol specifications can be composed sequentially and iterated a parameterised number of times to build families of interactions.The paper illustrates iteration with foreach(i < n){G1; G2}.Source: §1 · p. 2
- Indexed participants such as W[i] describe protocol families whose participant count and message exchanges may be unknown until run-time parameter instantiation.The introduction gives a sequence from W[n] to W[0] as an example.Source: §1 · p. 2
- Projection must type-check endpoints before the concrete topology is known, even when parameter values produce different communication roles or no communication.For n ≥2, the example has initiator, middle-worker, and last-worker patterns; n = 1 and n = 0 differ.Source: §1 · pp. 2–3
- The type system aims to ensure type safety and deadlock freedom for well-typed processes following parameterised multiparty protocols.The paper also claims decidable type checking and applies the framework to process topologies including a butterfly network.Source: §1 · pp. 2–3
- The framework combines dependent type theories derived from Gödel’s System T and indexed dependent types with multiparty session types.Its contributions also include flexible projection using a generic endpoint generator and mergeability of branching types.Source: §1 · p. 3
2. Types and processes for parameterised multiparty sessions
The section combines global interaction types, dependent indices, and primitive recursion to describe protocols and processes whose participants and interaction counts can be instantiated at run time. It presents parameterised topology examples, process syntax and semantics, and implementations including an FFT.
2.1. Global types.
- The recursor repeats a protocol body by decreasing its index to zero, while composition, repetition, product, and test operators are defined from it.Composition appends one protocol to another, but composition and repetition do not necessarily impose sequentiality.Source: §2.1 · pp. 4–5
2.2. Examples of parameterised global types.
- Ring, multicast, and mesh examples describe communication patterns over indexed workers, including a mesh flow from W[n][m] toward W[0][0].The ring uses n + 1 workers with n ≥ 2; multicast sends from Alice through W[0] to W[n−1], and the mesh is parameterised by row and column counts n and m.Source: §2.2 · pp. 5–6
2.3. Process syntax.
- Process syntax includes indexed participants evaluated during reductions, asynchronous session initiation, message and label exchange, branching, recursion, and primitive recursion.A queue stores asynchronous messages in transit.Source: §2.3 · pp. 6–7
2.4. Semantics.
- Session initialisation creates a private session and an initially empty queue; sends enqueue messages, while receives consume matching queued messages.The semantics also permits reordering messages with different senders or receivers and garbage-collects unused empty queues.Source: §2.4 · pp. 7–8, §2.3 · p. 7
2.5. Processes for parameterised multiparty protocols.
- Recursors generate parameterised processes, including repeated message exchanges and workers assigned distinct mesh roles according to their positions.For the sequence example, n = 0 exchanges no message; otherwise the recursor creates n − 1 workers in the main loop and spawns the initial and final workers.Source: §2.5 · pp. 8–10
2.6. Fast Fourier Transform.
- The section presents a radix-2 Cooley–Tukey FFT over a butterfly network, then gives its global session type and an implementation as interacting processes.The FFT computes the discrete Fourier transform of a vector of complex numbers.Source: §2.6 · p. 10
N (b) FFT diagram
The FFT diagram represents computation across machines in successive butterfly steps. Each machine exchanges values with a partner differing in one bit of its number, while dotted edges mark values sent to itself for later steps.
N (b) FFT diagram
- Each diagram row represents one machine at one algorithm step, and each edge represents a value sent between machines.Dotted edges denote messages a machine sends to itself to retain a value for the next step.Source: N (b) FFT diagram · p. 11, Figure 8 · p. 11
- Successive butterflies pair machines whose numbers differ in one bit, with a different bit selected at each step.The input uses bit-reversed ordering: machine p initially receives the element indexed by the bit-reversal of p.Source: N (b) FFT diagram · p. 11
- At step l, the session type pairs machine indices differing in bit n − l; its network size is parameterised by n.The repeated communications encode the four edges of each butterfly pattern.Source: N (b) FFT diagram · p. 12
- The machine processes perform n butterfly steps, exchange values with the partner obtained by flipping the selected bit, then send calculated values to external channels.The two branches test the selected bit and use partner indices p + 2^(n−l−1) or p − 2^(n−l−1).Source: N (b) FFT diagram · p. 12
3. Typing parameterised multiparty interactions
The type system projects parameterised global protocols to run-time-dependent endpoint types and uses dependent environments, kinding, equivalence, and process-typing rules to type individual participants. Mergeable branching and recursor-aware equivalence accommodate varied interaction patterns while preserving algorithmic checking, with a meta-logical extension available at a decidability cost.
3.1. End-point types and end-point projections.
- Generic projection represents the family of endpoint types a participant may satisfy at runtime, before the concrete participant characteristics are known.For each communication prefix, projection outputs, inputs, or skips according to the target participant's relation to the sender and receiver.Source: §3.1 · p. 13, Figure 10 · p. 13
- Mergeability permits branch endpoints to differ on distinct labels, enabling projections that the original rule rejects, such as W[2]'s ok and quit branches.The paper states this projection is sound up to branching subtyping.Source: §3.1 · pp. 13–14
3.2. Type system (1): environments, judgements and kinding.
- Session environments may contain dependent process types, while interdependent well-formedness and kinding rules validate types, environments, and recursor-based families.Recursor kinding adjusts the index range to the predecessor range used by index substitution.Source: §3.2 · pp. 14–15
3.3. Type system (2): type equivalence.
- Decidable type equivalence compares well-formed types via common weak-head forms, with recursors handled structurally or by finite-index reduction; structural handling also covers infinite index sets.The structural recursor rule has priority, while staged base and application rules avoid infinite rule application.Source: §3.3 · pp. 15–17, Figure 15 · p. 18
- A meta-logical equivalence rule removes the finite-index requirement by allowing proofs that recursor-based types are extensionally equivalent, at a cost to decidability.The paper uses this technique to type several examples.Source: §3.3 · p. 17, Figure 16 · p. 18
3.4. Typing processes.
- Process typing checks recursor families by base and inductive cases, and session initiation and acceptance against global-type projections, with acceptance requiring full instantiation.The inductive case uses the predecessor type as its induction hypothesis.Source: §3.4 · pp. 17–19, Figure 17 · p. 19
4. Properties of typing
This section establishes typing stability and substitution properties, along with sound mergeability, typing preservation, and conditional progress for multiparty sessions. It also proves termination of equality and annotated-process type checking under explicit decidability assumptions, including restrictions on index predicates or domains.
4.1. Basic properties.
- Permutation and weakening preserve judgments, while strengthening permits removal of an unused variable from a typing context.The strengthening condition excludes the removed variable from the free variables of the remaining context and judgment.Source: §4.1 · p. 20
- Agreement and exchange preserve judgments across well-formed environments and equivalent types, indices, or process mappings.The basic properties also ensure that judgments entail their associated environment or kinding well-formedness.Source: §4.1 · p. 20
- Substitution preserves well-typedness for indices, process variables, term variables, and session channels, providing a key foundation for subject reduction.Index substitution may change session types and environments.Source: §4.1 · pp. 21–22
4.2. Termination of equality checking and type checking.
- Global and end-point type reduction is strongly normalizing and confluent on well-formed kindings, yielding a unique weak-head normal form.The proof uses strong normalization of System T and Newman’s Lemma for confluence.Source: §4.2 · p. 22
- Type-equality checking terminates if the predicates appearing in its derivations are decidable.The proof relies on a lemma showing that each rule premise has lower weight than its conclusion.Source: §4.2 · pp. 24–25
- Annotated-process type-checking terminates when the predicates used in kinding, equality, projection, and typing derivations are decidable.The theorem applies to annotated processes checked against the empty process environment.Source: §4.2 · p. 26
- Termination of typing judgments can be ensured by restricting predicates to decidable arithmetic, such as linear equalities over naturals without multiplication, or by using finite index domains.Source: §4.2 · p. 27
4.3. Type soundness and progress.
- Mergeability is sound for branching subtyping: the merge of two compatible projections is their greatest common subtype.This result supports replacing projection merge with a subtype-based formulation when proving subject reduction.Source: §4.3 · p. 27
- Typing is preserved under structural congruence and reduction when the session environment is coherent.Theorem 4.6 also requires the initial typing judgment and coherent session environment for its reduction result.Source: §4.3 · p. 28
- Communication safety and session fidelity follow as corollaries of the subject congruence and reduction theorem [24].Source: §4.3 · pp. 28, 30
- A well-linked, runtime-syntax-free program typed with an empty session environment either terminates or can take another reduction step.The paper notes progress in a single multiparty session despite asynchronous initiation.Source: §4.3 · p. 30
5. Typing examples
The examples demonstrate how parameterised global specifications are projected into endpoint types and checked for repetition, network topologies, FFT, and a Web service. They culminate in a type-safety and deadlock-freedom theorem for the FFT processes.
5.1. Repetition example - § 1 (1.1).
- The repetition example projects n repetitions of an Alice-to-Bob message into a recursor-based endpoint type, and the typing derivation uses the recursor rules.Bob and Carol's processes can be typed similarly.Source: §5.1 · p. 31
5.2. Sequence example - § 1 (1.2).
- In the sequence, the starter sends, the final worker receives, and middle workers receive then send; checking all indices uses finite-domain enumeration or meta-logic.Finite-domain checking terminates, while the meta-logic rule permits proving stronger properties about an implementation.Source: §5.2 · p. 32
5.3. Ring - Figure 3(a).
- The ring projection is checked like the sequence, using finite-domain equivalence when n is bounded or meta-logic otherwise.Users can type processes against a separately written endpoint type.Source: §5.3 · p. 32
5.4. Mesh pattern - Figure 3(b).
- For the mesh, the generator returns endpoint types matching the programmer-designed types for the top-left corner and the bottom-row case, as for the other cases.The demonstrated equivalence proof checks the top-left corner and bottom row; the remaining cases are left to the reader.Source: §5.4 · pp. 33–34
5.5. FFT example - Figure 8.
- For every m, Pfft m is typable and any reduction reaches processes sending the final values on the external channels.The theorem derives safety and deadlock-freedom from typing the processes under a single multiparty dependent session and the progress theorem.Source: §5.5 · p. 34
5.6. Web Service.
- The Quote Request specification composes parameterised supplier and manufacturer interactions, representing repeated exchanges, runtime-bounded participants, and recursive behaviour.It builds the protocol from modular global types and composes them using recursion; supplier endpoint projections use branching injection and mergeability.Source: §5.6 · pp. 36–37
6. Conclusion and related work
The paper combines indexed dependent types, recursors, and multiparty session types to describe parameterised protocols with decidable typing under an index-arithmetic assumption. It reports safety and deadlock-freedom guarantees and implementation examples, while distinguishing its static protocol families from work on dynamic session structures.
6. Conclusion and related work
- The theory combines indexed dependent types, dependent types with recursors, and multiparty session types, with decidable typing under an assumption about index arithmetic.The authors report implementations of Web services and parallel algorithms, and a performance benefit over binary-session versions from reducing multiple session-establishment overhead.Source: §6 · p. 38
6.1. Related work.
- Restricting dependency to index sorts reduces checking to index constraints, while primitive recursors represent sequences and support integration with full session types and general recursion.The paper states that decidability depends on the constraint-solving problem being decidable.Source: §6.1 · p. 38
- The related work identifies prior dependent-type studies that do not investigate families of global specifications and notes that soundness required careful treatment of simultaneous term and index instantiation.The paper says type soundness was left open in.Source: §6.1 · p. 38
- The authors contrast their parameterised global descriptions with binary-session web interactions and report integration with existing multiparty systems without changing runtime typing components.They also contrast their mesh and FFT example with the expressivity explored in, and discuss progress limitations of contracts.Source: §6.1 · p. 39
- Unlike work on dynamic session structures, this theory describes a family of protocols over arbitrary participant counts for runtime instantiation, with safety and progress for well-typed instantiations.The paper presents parameterisation, composition, and repetition as idioms in parallel algorithms and choreographic interactions.Source: §6.1 · pp. 39–40
Appendix A. Kinding and typing rules
The appendix supplies kinding and typing rules omitted from the main sections, including subtyping rules used to type runtime processes.
Appendix A. Kinding and typing rules
- The appendix provides definitions of kinding and typing rules omitted from the main sections.Source: Appendix A · p. 42
A.1. Kinding and subtyping.
- Figure 21 presents subtyping rules used for typing runtime processes; type isomorphism rules follow by replacing ≤ with ≈.Source: §A.1 · p. 42
A.1. Kinding and subtyping.
Figure 21 is titled “Subtyping.”
A.1. Kinding and subtyping.
- Figure 21 presents subtyping.Source: Figure 21 · p. 43
Appendix B. Typing system for runtime processes
Appendix B defines typing rules for runtime processes and queues, using generalized types to compose queued messages with process continuations. Coherence, equivalence, and queue-disjointness conditions govern these typings.
Appendix B. Typing system for runtime processes
- Generalized types represent sessions, queue messages, or a message sequence followed by a session, connecting queue contents to pure-process continuations.Message types describe sends or selections, and sequencing is associative.Source: Appendix B · p. 43
- Queue message sequences are equivalent under swaps of messages to different participants, and session-environment equivalence uses this relation while ignoring end entries.This equivalence is used by the process typing rules.Source: Appendix B · p. 44
- Queue typing starts from an empty environment and adds each message’s output type to the channel associated with its sender.The queue rules use sequencing to extend the channel’s current type.Source: Appendix B · p. 44
- The process judgement tracks queues by session name; GInit lifts queue-free processes, while GPar requires disjoint session-name sets and composes generalized types.Composition sequences message types with session types and fails for incompatible combinations.Source: Appendix B · pp. 44–45
- Restriction requires session-environment coherence, defined using projections and duality; projection preserves a participant’s branches and merges branches for other participants.Projection also acts recursively on recursive types and leaves variables and end unchanged.Source: Appendix B · pp. 45–46