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.
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 language | English |
|---|---|
| Title of host publication | Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019 |
| Publisher | ACM |
| Pages | 27-31 |
| Number of pages | 5 |
| ISBN (Electronic) | 9781450368247 |
| ISBN (Print) | 978-1-4503-6824-7 |
| DOIs | |
| Publication status | Published - 17 Jul 2019 |
| Event | Tenth ACM SIGPLAN Scala Symposium - London, United Kingdom Duration: 17 Jul 2019 → 17 Jul 2019 https://2019.ecoop.org/home/scala-2019 |
Publication series
| Name | Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019 |
|---|
Workshop
| Workshop | Tenth ACM SIGPLAN Scala Symposium |
|---|---|
| Abbreviated title | Scala '19 |
| Country/Territory | United Kingdom |
| City | London |
| Period | 17/07/19 → 17/07/19 |
| Internet address |
Bibliographical note
© 2019 Copyright held by the owner/author(s). Publication rights licensedto 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