Compiling the Mailbox Calculus
Supervisor: Dr Simon Fowler
School: Computing Science
Software underpins everything from safety-critical industrial control systems to toothbrushes. This ubiquity brings with it the challenge of software correctness. Although a malfunctioning toothbrush is tolerable, other errors carry catastrophic consequences: for example, a software error caused the failure of the $125 million 1998 Mars Climate Orbiter, and a concurrency error in the Therac-25 radiotherapy machine delivered fatal radiation doses to patients.
The age of sequential programs running on a single computer is over, requiring developers to write concurrent and distributed applications. Concurrency and distribution introduces many challenges, including ensuring protocol conformance and safe access to shared resources, and resilience to failures. Actor-based programming languages tame this complexity by structuring an application as a collection of lightweight processes which communicate using message passing. Erlang is an industry-strength actor language famed for performance and reliability, and is used by leading technology firms such as WhatsApp, Klarna, and Ericsson to serve millions of customers while remaining resilient to failures.
Actor-based languages alleviate many concurrency problems, but remain susceptible to errors such waiting for a message which will never arrive, or receiving a message which cannot be handled. Such errors are hard to diagnose and fix, resulting in hours of wasted developer productivity.
Static type systems allow lightweight software verification, catching common programming errors before they occur at runtime. However, very few type systems are available for mainstream actor languages, and those which do exist cannot rule out communication errors. The Mailbox Calculus is a typed core formal model which can detect protocol violations in actor-like systems. In the context of the EPSRC-funded STARDUST project, we have designed a programming language based on the Mailbox Calculus, and have implemented a type system which rules out many incorrect concurrent programs.
The aim of this project is to compile our programming language into Core Erlang, which is an intermediate representation of the Erlang programming language. In turn, the project will enable developers to avail themselves of the additional safety guarantees given by our type system, while enjoying the industry-leading performance afforded by the Erlang runtime system. The project blends theory and practice, involving the research task of developing an appropriate compilation strategy, and then implementing the compiler. Concretely, the outcomes of the project will be:
• A formal description of a compilation scheme from the mailbox calculus into Core Erlang
• A tool implementing the compilation pass, integrating with our existing toolchain
• A collection of example applications