Robust Communications in Erlang

Erlang is a dynamically-typed functional and concurrent programming language lauded by its proponents for its relatively simple syntax, process isolation, and fault tolerance. The functional aspect has rich features like pattern matching and tail-call optimisation, while the concurrent aspect uses isolated processes and asynchronous message passing to share state between system components. The two meet with pattern matching on mailboxes, which allows for a process to pick a message from its mailbox - potentially out of order - based on its structure, value, type, or a mixture thereof. A strongly and dynamically typed language like Erlang can experience many kinds of runtime errors, such as ill-typed operands to arithmetic operators. The interaction between Erlang's type system and process mailboxes can lead to a more subtle runtime error which is harder to detect: orphan messages. As the types of messages are not checked either at compile time or runtime, a process can be sent a message which it will never receive. Essentially, non-trivial type discrepancies in Erlang programs can cause subtle bugs when communication is involved. These problems can be hard to detect and fix, with current solutions such as extensive testing and exhaustive model checking. This thesis reports on work to detect communication-related type discrepancies in Erlang programs. A fragment of the Core Erlang intermediate format is modelled formally so that we can reason about the out-of-order communication in Erlang systems, particularly the dependencies between sent messages when determining whether orphan messages exist. Afterwards, a sub-typing relation based on Erlang's type system is introduced to clearly define the notion of an orphan message, forming the foundation of a system for automatic detection via a mix of static analysis and runtime verification. This culminates in automatic tooling to detect certain cases of communication discrepancies via static analysis, and automatic instrumentation of concurrent programs to detect and recover from more complicated cases at runtime.