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

Fingerprint

Message passing
DSL
Network protocols
Program processors

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

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
Scalas, Alceste ; Yoshida, Nobuko ; Benussi, Elias. / Effpi: Verified Message-Passing Programs in Dotty. Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019. ACM, 2019. pp. 27-31 (Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019).
@inproceedings{0fd5a7f8c0ec4662b04a1bfb5f9aa0e3,
title = "Effpi: Verified Message-Passing Programs in Dotty",
abstract = "We present Effpi: an experimental toolkit for strongly-typedconcurrent and distributed programming in Dotty, withverification capabilities based on type-level modelchecking. Effpi addresses a main challenge in creating andmaintaining 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 atfinding them early, when code is written and compiled. Effpiprovides:(1) a set of Dotty classes for describing communication protocols as types;(2) an embedded DSL for concurrent programming, with process-based andactor–based abstractions;(3) a Dottycompiler plugin to verify whether protocols and programs enjoydesirable properties,such as deadlock-freedom; and(4) an efficient run-time system for executing Effpi’s DSL-basedprograms.The combination of (1) and (2) allows the Dottycompiler to check whether an Effpi program implements a desiredprotocol/type; and this, together with (3), means that manytypical concurrent programming errors are found and ruled out atcompile-time. Further, (4) allows to run highly concurrent Effpiprograms with millions of interacting processes/actors, byscheduling them on a limited number of CPU cores. In this paper,we give an overview of Effpi, illustrate its design and mainfeatures, and discuss its future.",
keywords = "Actors, Behavioural types, Dependent types, Dotty, Model checking, Processes, Scala, Temporal logic",
author = "Alceste Scalas and Nobuko Yoshida and Elias Benussi",
note = "{\circledC} 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.",
year = "2019",
month = "7",
day = "17",
doi = "10.1145/3337932.3338812",
language = "English",
isbn = "978-1-4503-6824-7",
series = "Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019",
publisher = "ACM",
pages = "27--31",
booktitle = "Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019",
address = "United States",

}

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. Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019, ACM, pp. 27-31, Tenth ACM SIGPLAN Scala Symposium, London, United Kingdom, 17/07/19. https://doi.org/10.1145/3337932.3338812

Effpi: Verified Message-Passing Programs in Dotty. / Scalas, Alceste; Yoshida, Nobuko; Benussi, Elias.

Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019. ACM, 2019. p. 27-31 (Scala 2019 - Proceedings of the 10th ACM SIGPLAN International Symposium on Scala, Part of ECOOP 2019).

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

TY - GEN

T1 - Effpi: Verified Message-Passing Programs in Dotty

AU - Scalas, Alceste

AU - Yoshida, Nobuko

AU - Benussi, Elias

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

PY - 2019/7/17

Y1 - 2019/7/17

N2 - We present Effpi: an experimental toolkit for strongly-typedconcurrent and distributed programming in Dotty, withverification capabilities based on type-level modelchecking. Effpi addresses a main challenge in creating andmaintaining 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 atfinding them early, when code is written and compiled. Effpiprovides:(1) a set of Dotty classes for describing communication protocols as types;(2) an embedded DSL for concurrent programming, with process-based andactor–based abstractions;(3) a Dottycompiler plugin to verify whether protocols and programs enjoydesirable properties,such as deadlock-freedom; and(4) an efficient run-time system for executing Effpi’s DSL-basedprograms.The combination of (1) and (2) allows the Dottycompiler to check whether an Effpi program implements a desiredprotocol/type; and this, together with (3), means that manytypical concurrent programming errors are found and ruled out atcompile-time. Further, (4) allows to run highly concurrent Effpiprograms with millions of interacting processes/actors, byscheduling them on a limited number of CPU cores. In this paper,we give an overview of Effpi, illustrate its design and mainfeatures, and discuss its future.

AB - We present Effpi: an experimental toolkit for strongly-typedconcurrent and distributed programming in Dotty, withverification capabilities based on type-level modelchecking. Effpi addresses a main challenge in creating andmaintaining 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 atfinding them early, when code is written and compiled. Effpiprovides:(1) a set of Dotty classes for describing communication protocols as types;(2) an embedded DSL for concurrent programming, with process-based andactor–based abstractions;(3) a Dottycompiler plugin to verify whether protocols and programs enjoydesirable properties,such as deadlock-freedom; and(4) an efficient run-time system for executing Effpi’s DSL-basedprograms.The combination of (1) and (2) allows the Dottycompiler to check whether an Effpi program implements a desiredprotocol/type; and this, together with (3), means that manytypical concurrent programming errors are found and ruled out atcompile-time. Further, (4) allows to run highly concurrent Effpiprograms with millions of interacting processes/actors, byscheduling them on a limited number of CPU cores. In this paper,we give an overview of Effpi, illustrate its design and mainfeatures, and discuss its future.

KW - Actors

KW - Behavioural types

KW - Dependent types

KW - Dotty

KW - Model checking

KW - Processes

KW - Scala

KW - Temporal logic

UR - https://dl.acm.org/citation.cfm?doid=3337932.3338812

UR - http://www.scopus.com/inward/record.url?scp=85074451337&partnerID=8YFLogxK

U2 - 10.1145/3337932.3338812

DO - 10.1145/3337932.3338812

M3 - Conference contribution

SN - 978-1-4503-6824-7

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

SP - 27

EP - 31

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

PB - ACM

ER -

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