Top-Down = Bottom-Up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
\emph{Multiparty session types} (MPST) are a type discipline for
concurrent and distributed systems, designed to ensure not only type
safety and deadlock-freedom, but also \emph{liveness} of typed
communicating processes. Two main MPST methodologies, top-down and
bottom-up, have been proposed and are integrated into a wide range of
programming languages and tools. The \emph{top-down} strategy starts
by specifying the overall choreography of the protocol (called a
global type), from which a set of local types that satisfy safety and
liveness are generated by endpoint projection (EPP). Once each
participant is type-checked against a generated local type, liveness
of the set of typed processes is automatically ensured \emph{by
construction}. The \emph{bottom-up} strategy directly checks whether
local types inferred from processes satisfy liveness in order to
enforce liveness of processes. Since the top-down strategy depends on
global types and the EPP algorithms, it has often been considered that
the top-down system offers \emph{strictly less typability} than the
bottom-up system. Our paper negates this belief. We prove that, using
the precise subtyping for the subsumption rule, the top-down strategy
offers \emph{exactly the same typability} as the bottom-up system.
More precisely, a multiparty session $M$ is typable and verified to be
live by the bottom-up typing system if and only if $M$ is typable by
the top-down typing system. The key to the proof is the development
of a \emph{principal global type inference algorithm} which builds a
\emph{principal} global type from an arbitrary set of live local
types. We have implemented the global type inference algorithm
together with projection, process type checking and local type
inference algorithms, and built a toolchain for both the top-down and
bottom-up strategies. We evaluated our toolchain with representative
examples from the literature, confirming that the top-down approach is
more efficient than the bottom-up approach.
Tue 6 OctDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00 | Session Types and ConcurrencyOOPSLA at Junior Ballroom 1&2 Chair(s): Peter Thiemann University of Freiburg | ||
13:30 18mTalk | Speak Now: Safe Actor Programming with Multiparty Session Types OOPSLA DOI | ||
13:48 18mTalk | Mixed Choice in Asynchronous Multiparty Session Types OOPSLA Laura Bocchi University of Kent, Raymond Hu Queen Mary University of London, Adriana Laura Voinea University of Glasgow, Simon Thompson University of Kent DOI | ||
14:06 18mTalk | Top-Down = Bottom-Up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols OOPSLA DOI | ||
14:24 18mTalk | A Design Space Exploration of Async/Await OOPSLA DOI Pre-print | ||