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
Say we have a program that implements party
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
Here is a tiny language of local types.
The projections for
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
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
We can now write a type like
which would suffice for the start of a commit protocol.
Notice that
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
but interacts with every member of , the quantifier should remain in the local type , which correctly captures the multicast. - when we project with respect to the set of participants, since our arbitrary participant is in
, it is involved in only one , so the quantifier should disappear.
Here is the projection function for
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
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
That is, a universal quantification is just the parallel composition of "what
The solution is thus to project the parallel composition instead,
with respect to the party
For explicitness, we'll refine
There are two cases for
-
If
but , i.e. it is possible that the quantifier involves , we first apply the lemma above, which separates the behavior of from that of everyone else in , then recursively project on both sides. Intuitively, the left arm is what
does, while the right is what other parties do to . is involved in both sides of the 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! -
Otherwise (if
or ), we keep the quantifier and project under it, for the same reason as before: may interact with the parties of role .
The extension for
Let's walk through an example.
The type in (1) represents a protocol where every party in role
In (2),
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
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.