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

Displayed time zone: Belfast change

15:40 - 17:20
Compilation and verificationScala at Epernay
Effpi: Verified Message-Passing Programs in Dotty
Alceste Scalas Aston University, Birmingham, UK, Nobuko Yoshida Imperial College London, Elias Benussi Faculty Science Ltd
Challenges of Optimizing Scala Programs
Stage Polymorphism Based on Types for a Typeless Language: MATLAB in LMS
Alen Stojanov , Tiark Rompf Purdue University, Markus Püschel ETH Zürich