Effpi: Verified Message-Passing Programs in Dotty

Alceste Scalas, Nobuko Yoshida, Elias Benussi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationScala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019
PublisherACM
Pages27-31
Number of pages5
ISBN (Electronic)9781450368247
ISBN (Print)978-1-4503-6824-7
DOIs
Publication statusPublished - 17 Jul 2019
EventTenth ACM SIGPLAN Scala Symposium - London, United Kingdom
Duration: 17 Jul 201917 Jul 2019
https://2019.ecoop.org/home/scala-2019

Publication series

NameScala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019

Workshop

WorkshopTenth ACM SIGPLAN Scala Symposium
Abbreviated titleScala '19
CountryUnited Kingdom
CityLondon
Period17/07/1917/07/19
Internet address

Bibliographical note

© 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.

Keywords

  • Actors
  • Behavioural types
  • Dependent types
  • Dotty
  • Model checking
  • Processes
  • Scala
  • Temporal logic

Fingerprint Dive into the research topics of 'Effpi: Verified Message-Passing Programs in Dotty'. Together they form a unique fingerprint.

  • Cite this

    Scalas, A., Yoshida, N., & Benussi, E. (2019). Effpi: Verified Message-Passing Programs in Dotty. In Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019 (pp. 27-31). (Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019). ACM. https://doi.org/10.1145/3337932.3338812