Effpi

Verified message-passing programs in Dotty

Effpi is an experimental toolkit for strongly-typed message-passing programs in Dotty (a.k.a. the future Scala 3 programming language), with verification capabilities based on type-level model checking.

Features

  1. behavioural types, i.e., types that specify the protocol that a program is expected to follow: what messages it should send/receive, their intended destination/origin, and their order. For example:
    import effpi.channel.Channel
    import effpi.process.{In, Out, >>:}
    
    // Take two channels x and y carrying strings; use x to receive a message;
    // then, either forward the message on y, or send "Nope" on x
    type T = (x: Channel[String], y: Channel[String]) => (
      In[x.type, String, (msg: String) =>
        (Out[y.type, msg.type] | Out[x.type, "Nope"])
      ]
    )
  2. a Domain-Specific Language for writing message-passing programs with the behavioural types above. The DSL has two flavours: process-based (see example below) and actor-based (inspired by Akka Typed). DSL programs are type-checked by the Dotty compiler - and if a program compiles, then it correctly implements the intended type/protocol. For example:
    import effpi.process.dsl.{receive, send}
    import scala.concurrent.duration.Duration
    
    // This implicit timeout is used by receive() below
    implicit val timeout: Duration = Duration(30, "seconds")
    
    // Implement type/protocol T above. The type annotation ensures that
    // the implementation abides by protocol T: mistakes like
    // sending something unexpected on channels x or y, or forgetting to
    // forward the message or send "Nope", all cause compile-time errors
    val f: T = (x: Channel[String], y: Channel[String]) => {
      receive(x) { msg =>
        println(f"Received: ${msg}")
        if (msg.length > 42) {
          println(f"Forwarding message via channel y")
          send(y, msg)
        } else {
          println("Replying 'Nope'")
          send(x, "Nope")
        }
      }
    }
  3. an efficient interpreter for running programs written in the DSL above. The Effpi interpreter can run highly concurrent applications millions of interacting processes/actors;
  4. compile-time verification of behavioural properties: Effpi can check whether a (typed) program (or ensemble of programs) enjoys properties like deadlock-freedom. This is achieved through a compiler plugin that interfaces to the mCRL2 model checker. For example:
    // Define a bunch of protocols...
    type T1[...] = ...
    type T2[...] = ...
    
    // ...and with an "@effpi.verify(...)" annotation, check whether their
    // parallel composition ("Par") and their implementation ("impl") could
    // deadlock. If the verification succeeds at compile-time, then "impl"
    // will never get stuck at run-time.
    @effpi.verify(property="deadlock_free()")
    def impl(x: Channel[...], y: Channel[...]): Par[T1[...], T2[...]] = {
      ...
    }
    

Resources

This website is under construction. For now, please refer to the following materials.

Papers

Implementation

Authors

Effpi is developed by:

  • Alceste Scalas — DTU Compute, Technical University of Denmark
  • Elias Benussi — Faculty Science Ltd., UK

The theory behind Effpi is developed in collaboration with:

  • Nobuko Yoshida — Imperial College London, UK