$\gdef\kwproj{\mathbin{\upharpoonright}}$ $\gdef\gall#1#2#3{\forall #1 : #2 \cdot #3}$ $\gdef\galls#1#2#3#4{\forall #1 : #2 \setminus #3 \cdot #4}$ $\gdef\galle#1#2#3#4{\forall #1 : #2 \setminus \{#3\} \cdot #4}$ $\gdef\gtransmit#1#2#3{#1 \to #2:#3}$ $\gdef\kwpar{\mathrel{||}}$ $\gdef\spar#1#2{#1 \kwpar #2}$ $\gdef\lsend#1#2{\mathit{send}\ #1\ #2}$ $\gdef\lrecv#1{\mathit{recv\ #1}}$

Session types are a neat and fascinating formalism. Intuitively, they are small languages for describing communication protocols. Viewing these protocols as types, a type system may be used to check that a program implements a protocol correctly and has other nice properties, such as deadlock-freedom. Unlike types which constrain data, session types are behavioral specifications and constrain what programs can do.

Multiparty session types concern more than two communicating parties and are usually written in "Alice & Bob notation", specifying a protocol from a so-called global perspective.

Here's the syntax of a tiny MPST language.

We can write a type such as

which specifies a protocol where party $a$ sends the message $m$ to party $b$, and $b$ then replies with message $n$.

Say we have a program that implements party $a$, and we want to check it against the protocol.

function a(m) {
    Send(b, m);
    let n = Receive(b);
}

One approach is to split the global type into two local halves, then check the program against the half for $a$. This splitting operation is called projection because we are keeping only a slice or subpart of the behavior of the overall system, or some subsequences of its execution traces, etc.

Here is a tiny language of local types.

The projections for $a$ and $b$ would be:

How do we compute such a projection?

The rules are very simple for this tiny language: projection is "pushed through" sequential composition, and if we are projecting $\to$ with respect to a given party $p$ and we see $p$ is the sender, the result is a $\mathit{send}$, otherwise it is a $\mathit{recv}$.

Multicasts

It would be amazing if we could model a real-world protocol like Raft as a type and have the conformance of an implementation checked automatically and decideably!

We are still quite a long way off. One major missing ingredient is the ability to express a multicast, the first step in leader election.

Let's extend our language of multiparty session types with a way to talk about communication that happens uniformly across a set of parties, which we'll call a role. We'll use the symbol $\forall$ for it, as an analogy to universal quantification. We'll also add parallel composition $||$.

We can now write a type like

which would suffice for the start of a commit protocol. Notice that $\forall$ is just n-ary parallel composition for each party in the role.

Projection should give us

which matches our intuition neatly:

• when we project with respect to the set of coordinators, we want to get a local type which says what one arbitrary coordinator does. Since this coordinator isn't in $ps$ but interacts with every member of $ps$, the quantifier should remain in the local type $L_c$, which correctly captures the multicast.
• when we project with respect to the set of participants, since our arbitrary participant is in $ps$, it is involved in only one $\mathit{recv}$, so the quantifier should disappear.

Here is the projection function for $\forall$, which is now defined with respect to a role $S$.

Self-sends

For leader election, however, we quickly run into a problem.

The rules from before don't help us much - do we keep the quantifier or not? Also, it seems that a server should both $\mathit{send}$ and $\mathit{recv}$, but since there is only one role to project with respect to, we can only have one of those.

We call this sort of intra-role communication a self-send.

The paper Dynamic Multirole Session Types (2013) proposes an elegant solution, based on the following observation, or lemma: given an arbitrary party $z$ in role $S$, the following types are equivalent.

That is, a universal quantification is just the parallel composition of "what $z$ does" and "what everyone else does".

The solution is thus to project the parallel composition instead, with respect to the party $z$, instead of "an arbitrary party of role $S$". Before, these were equivalent because we didn't need to be sensitive to which party in a role we were concerned with.

For explicitness, we'll refine $\forall$ with a set of exclusions $e$, which may be empty.

There are two cases for $\forall$.

1. If $z \in S$ but $z \notin e$, i.e. it is possible that the quantifier involves $z$, we first apply the lemma above, which separates the behavior of $z$ from that of everyone else in $S$, then recursively project on both sides.

   $$(\forall x:S\setminus e\cdot G) \kwproj z \equiv (G[z/x] \kwproj z) \kwpar (\forall x:S\setminus (\\{z\\}\cup e)\cdot (G \kwproj z))$$

   Intuitively, the left arm is what $z$ does, while the right is what other parties do to $z$. $z$ is involved in both sides of the $\kwpar$ precisely because members of the same set being quantified over are interacting. If we were projecting a protocol without a self-send, the right arm would be unobservable and disappear, and we would the same result as the projection function from the previous section!

2. Otherwise (if $z \notin S$ or $z \in e$), we keep the quantifier and project under it, for the same reason as before: $z$ may interact with the parties of role $S$.

   $$(\forall x:S\setminus e\cdot G) \kwproj z \equiv \forall x:S\setminus e\cdot (G \kwproj z)$$

The extension for $\to$ is simple: since we are projecting with respect to $z$, we can just check if an occurrence of communication involves $z$ directly. If it involves $z$ as both sender and receiver, we correspondingly produce both $\mathit{send}$ and $\mathit{recv}$.

Let's walk through an example.

The type in (1) represents a protocol where every party in role $C$ pings every other, sending a message and receiving a reply.

In (2), $z$ could be in $C$, so we apply $\forall$ case 1. In the left arm, we push the projection inward until we are able to project the communication into a $\mathit{send}$ (4). In the right arm, we add $z$ to the set of exclusions for the quantifier for $x$ and continue (3), but since $y$ may also be $z$, we find ourselves having to apply case 1 again (4). The left arm there projects to a receive (5), while the right is a no-op, as the communication between $x$ and $y$ is unobservable to $z$. This gives us the protocol at (6), which says exactly what we started out with.

The title of the paper mentioned earlier should make sense now. Protocols with self-sends and universal quantification are "multirole" because parties may act as both sender and receiver, and have two distinct classes of behaviors.

The paper uses "dynamic" in the sense that parties can join and leave, and the $\forall$ thus specifies the behavior of a possibly infinite set of parties. We aren't (yet?) concerned with this aspect. We are, however, concerned with two different senses of "dynamic", which is that roles may be computed in the course of the protocol, or dynamic changes; we return to this shortly.

Choreographic PlusCal

This is the heart of the projection function that is implemented in Choreographic PlusCal, a choreographic specification language I worked on.

It brings the succinctness and clarity of session types to a much more expressive specification language, one which scales up to real-world distributed protocols, which compute and branch, and are much closer to algorithms than sequences of transmissions.

The tradeoff is that Choreographic PlusCal models cannot be verified by simple type checking. Even properties such as deadlock-freedom cannot be guaranteed with things like await FALSE; in the language. Fortunately, being a PlusCal dialect, it has access to TLC, making it an exceedingly practical point in the design space.