Effpi

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

• A brief overview of Effpi (tool paper accepted at the Scala Symposium 2019);
• A. Scalas, N. Yoshida, E. Benussi. Verifying message-passing programs with dependent behavioural types (also available here). PLDI 2019. This paper describes the theoretical foundations of Effpi, and evaluates its implementation. Effpi has been reviewed and accepted as companion artifact of the paper.

Implementation

• Effpi's source code on GitHub
• Instructions and requirements: how to build Effpi, its software dependencies, how to reproduce the benchmarks in the PLDI'19 paper, and how to navigate Effpi's source code.
• A ready-to-use virtual machine with all Effpi's software dependencies. For details, please read the instructions above.