Verifying message-passing programs with dependent behavioural types

Alceste Scalas, Nobuko Yoshida, Elias Benussi

    Research output: Chapter in Book/Published conference outputConference publication

    Abstract

    Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler reasoning w.r.t. shared-memory concurrency, but do not ensure that a program implements a given specification. To address this challenge, it would be desirable to specify and verify the intended behaviour of message-passing applications using types, and ensure that, if a program type-checks and compiles, then it will run and communicate as desired. We develop this idea in theory and practice. We formalise a concurrent functional language λπ, with a new blend of behavioural types (from π-calculus theory), and dependent function types (from the Dotty programming language, a.k.a. the future Scala 3). Our theory yields four main payoffs: (1) it verifies safety and liveness properties of programs via typeś level model checking; (2) unlike previous work, it accurately verifies channel-passing (covering a typical pattern of actor programs) and higher-order interaction (i.e., sending/receiving mobile code); (3) it is directly embedded in Dotty, as a toolkit called Effpi, offering a simplified actor-based API; (4) it enables an efficient runtime system for Effpi, for highly concurrent programs with millions of processes/actors.

    Original languageEnglish
    Title of host publicationPLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
    EditorsKathryn S. McKinley, Kathleen Fisher
    PublisherACM
    Pages502-516
    Number of pages15
    ISBN (Electronic)9781450367127
    DOIs
    Publication statusPublished - 8 Jun 2019
    Event40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States
    Duration: 22 Jun 201926 Jun 2019

    Conference

    Conference40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
    Country/TerritoryUnited States
    CityPhoenix
    Period22/06/1926/06/19

    Bibliographical note

    © ACM, 2019. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Verifying message-passing programs with dependent behavioural types'. Together they form a unique fingerprint.

    Cite this