Speak Now: Safe Actor Programming with Multiparty Session Types
Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. \emph{Multiparty session types} (MPSTs) rule out communication errors early in the development process, but until now, the many-sender, single-receiver nature of actor communication has made it difficult for actor languages to benefit from session types.
This paper introduces Maty, the first actor language design supporting both \emph{static} multiparty session typing and the full power of actors taking part in \emph{multiple sessions}. Maty therefore combines the error prevention mechanism of session types with the scalability and fault tolerance of actor languages. Our main insight is to enforce session typing through a flow-sensitive effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will a session get stuck because an actor is waiting for a message that will never be sent. We extend Maty to support Erlang-style supervision and cascading failure, and show that this preserves Maty's strong metatheory. We implement Maty in Scala using an API generation approach, and demonstrate the expressiveness of our model by implementing a representative sample of the widely-used Savina actor benchmark suite; an industry-supplied factory scenario; and a chat server.
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 | ||