Static checking of concurrent programs in Elixir using session types

Abstract

Message-passing concurrency is becoming increasingly popular, and is prevalently used in several programming languages, such as Go, Scala, Rust and Elixir. In message-passing concurrency, processes interact with each other by exchanging messages. If these messages are sent incorrectly, certain behavioural issues, such as communication mismatches and deadlocks, may arise. We employ session types, which are a form of behavioural types, to detect these kinds of communication errors at compile-time, in the context of the Elixir language. More concretely, session types are protocols used to define the whole message-based interaction between processes, by dictating the order and type of messages that can be sent and received. We use these protocols to annotate public functions in Elixir modules to formalise their expected behaviour in terms of the messages sent and received when executing the body of said functions. Then, we design a (session) type system that uses these protocols to statically analyse and determine whether the functions observe the session type specification. This type system is validated from a formal perspective, by showing that it follows the session fidelity property. Moreover, the type system is validated empirically, by being implemented as a tool, which automates typechecking for Elixir modules.