Effpi: Verified Message-Passing Programs in Dotty


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 a main challenge in creating and maintaining concurrent programs: errors like protocol violations, deadlocks, and livelocks are often spotted late, at run-time, when applications are tested or (worse) deployed. Effpi aims at finding them early, when code is 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 give an overview of Effpi, illustrate its design and main features, and discuss its future.

Publication DOI: https://doi.org/10.1145/3337932.3338812
Divisions: College of Engineering & Physical Sciences
Additional Information: © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM. This is the author’s version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Tenth ACM SIGPLAN Scala Symposium (Scala ’19), July 17, 2019, London, United Kingdom, https://doi.org/10.1145/3337932.3338812.
Event Title: Tenth ACM SIGPLAN Scala Symposium
Event Type: Other
Event Dates: 2019-07-17 - 2019-07-17
Uncontrolled Keywords: Actors,Behavioural types,Dependent types,Dotty,Model checking,Processes,Scala,Temporal logic,Computational Theory and Mathematics,Computer Science Applications,Software
ISBN: 978-1-4503-6824-7, 9781450368247
Last Modified: 13 Jun 2024 07:44
Date Deposited: 15 Jul 2019 08:22
Full Text Link:
Related URLs: https://dl.acm. ... 3337932.3338812 (Publisher URL)
http://www.scop ... tnerID=8YFLogxK (Scopus URL)
PURE Output Type: Conference contribution
Published Date: 2019-07-17
Accepted Date: 2019-05-24
Authors: Scalas, Alceste (ORCID Profile 0000-0002-1153-6164)
Yoshida, Nobuko
Benussi, Elias



Version: Accepted Version

| Preview

Export / Share Citation


Additional statistics for this record