Wed 17 Jul 2019 15:40 - 16:10 at Epernay - Compilation and verification

We present Effpi: an experimental toolkit for strongly-typed concurrent and distributed programming in Dotty, with verification capabilities based on type-level model checking.

Effpi addresses one of the main challenges in developing and maintaining concurrent programs: many concurrency errors (like protocol violations, deadlocks, livelocks) are often spotted late, at run-time, when applications are tested or (worse) deployed in production. Effpi aims at finding such problems early, when programs are written and compiled.

Effpi provides: (1) a set of Dotty classes for describing communication protocols as types; (2) an embedded DSL for concurrent programming, with process-based and actor-based abstractions; (3) a Dotty compiler plugin to verify whether protocols and programs enjoy desirable properties, such as deadlock-freedom; and (4) an efficient run-time system for executing Effpi’s DSL-based programs. The combination of (1) and (2) allows the Dotty compiler to check whether an Effpi program implements a desired protocol/type; and this, together with (3), means that many typical concurrent programming errors are found and ruled out at compile-time. Further, (4) allows to run highly concurrent Effpi programs with millions of interacting processes/actors, by scheduling them on a limited number of CPU cores. In this paper, we provide an overview of Effpi; then, we illustrate its design and main features, and discuss its future developments.

Wed 17 Jul
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:40 - 17:20: Compilation and verificationScala at Epernay
15:40 - 16:10
Alceste ScalasAston University, Birmingham, UK, Nobuko YoshidaImperial College London, Elias BenussiFaculty Science Ltd
16:10 - 16:30
16:30 - 16:50
Alen Stojanov, Tiark RompfPurdue University, Markus PüschelETH Zürich