MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Verifying message-passing programs with dependent behavioural types
Alceste SCALAS, Nobuko YOSHIDA, Elias BENUSSI
To appear in
Programming Language Design and Implementation (PLDI 2019)

Concurrent and distributed programming is notoriously hard. Modern languages and toolkits address the challenge by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler reasoning w.r.t. shared-memory concurrency, but do not ensure that a program implements a given specification. To address this challenge, it would be desirable to specify and verify the intended behaviour of message-passing applications using types, and ensure that, if a program type-checks and compiles, then it will run and communicate as desired. We develop this idea in theory and practice. We formalise a concurrent functional language $\lambda^{\pi}_{\leq}$, with a new blend of behavioural types (from $\pi$-calculus theory), and dependent function types (from the Dotty programming language, a.k.a. the future Scala 3). This theory yields four main payoffs: (1) it verifies safety and liveness properties of programs via type– level model checking; (2) unlike previous work, it accurately verifies channel-passing (covering a typical pattern of actor programs) and higher-order interaction (i.e., sending/receiving mobile code); (3) it is directly embedded in Dotty, as a toolkit called Effpi, offering a simplified actor-based API; (4) it enables an efficient runtime system for Effpi, for highly concurrent programs with millions of processes/actors.

@inproceedings{SYB2019,
  author = {Alceste Scalas and Nobuko Yoshida and Elias Benussi},
  title = {{Verifying message-passing programs with dependent behavioural types}},
  booktitle = {Programming Language Design and Implementation},
  pages = {--},
  year = 2019
}
@inproceedings{SYB2019,
  author = {Alceste Scalas and Nobuko Yoshida and Elias Benussi},
  title = {{Verifying message-passing programs with dependent behavioural types}},
  booktitle = {Programming Language Design and Implementation},
  pages = {--},
  year = 2019
}