Scribble-Scala: Tutorial and Demo Artifact

Alceste Scalas, Ornela Dardha, Raymond Hu, Nobuko Yoshida

Table of Contents

Overview

This is a tutorial and demo of the Scribble-Scala tool for specifying and validating multiparty protocols, and Scala API generation for endpoint implementation.

This tutorial is accompanied by a demo artifact, published along with a paper on this work to appear in the proceedings of ECOOP '17. These are available online at the following:

The artifact contains a VirtualBox image for a ready-to-use, streamlined Ubuntu 16.04.2 operating system (thanks to OSBoxes.org), plus an installation of Scribble and lchannels (see above) with their dependencies.

See here for instructions on how to build Scribble-Scala from source.

In a nutshell, the interplay between Scribble and lchannels is the following:

  1. the Scribble tool can read a global protocol specification, describing the interactions between several roles (see Figure 9 in the paper), and validate it against various communication errors;
  2. then, for each role r in the protocol, our Scala extension to Scribble can generate a set of Scala class definitions, dubbed multiparty session classes: their API consists of typed send()/receive() methods, and guides the type-safe implementation of programs playing role r;
  3. internally, the multiparty session classes perform their communications through typed binary channels, using the lchannels library. The theory that allows Scribble-Scala to decompose the source multiparty protocols into typed binary channels is developed in the paper (from §2 to §6).

This tutorial presents several Scribble global protocols, and their Scala implementations. The Scala endpoint programs use the multiparty session classes generated by Scribble.

Quick Start (Kick-the-Tires)

In this section we provide basic instructions to setup the VirtualBox image, and try out the demos.

Setting Up and Running the VirtualBox Image

The following instructions have been tested using VirtualBox version 4.3.36 (on Ubuntu 14.04) and version 5.1.18 (on Windows 10 and Mac OS X). Start VirtualBox, and:

You can now start the newly-added VM, by selecting it and clicking "Start". To log in, use the following credentials:

Trying Out the Demos

After logging in, double-click on the "ECOOP'17 artifact demo" icon on the desktop, and follow the instructions.

Each demo will:

  1. show its Scribble global protocol specification;
  2. run Scribble, and show its output: i.e., the Scala multiparty session classes corresponding to the global protocol;
  3. launch an example implementation based on the multiparty session classes above (at this point, one or more terminals will pop up).

All demos should run without troubles. You might occasionally see a log message similar to the following, which is harmless: 

[ERROR] [04/11/2017 17:09:16.721] [GreetingServerSys-akka.remote.default-remote-dispatcher-2] [akka.tcp://GreetingServerSys@127.0.0.1:31337/system/endpointManager/reliableEndpointWriter-akka.tcp%3A%2F%2FGreetingClientSys%40127.0.0.1%3A31338-0/endpointWriter] AssociationError [akka.tcp://GreetingServerSys@127.0.0.1:31337] <- [akka.tcp://GreetingClientSys@127.0.0.1:31338]: Error [Shut down address: akka.tcp://GreetingClientSys@127.0.0.1:31338] [
akka.remote.ShutDownAssociation: Shut down address: akka.tcp://GreetingClientSys@127.0.0.1:31338
Caused by: akka.remote.transport.Transport$InvalidAssociationException: The remote system terminated the association because it is shutting down.

If you do not encounter other issues, then the artifact should be working, and ready for further evaluation.

Contents of the VirtualBox Image

These are the main contents of the VirtualBox image, and their locations:

How to run Scribble (command line)

The Scribble tool can be used to check the well-formedness of MPST protocols. In this artifact, we present an extended version that also allows to generate the Scala APIs for implementing the protocol endpoints.

Once logged in the VM, you can:

A concrete example: 

./scribblec-linmp.sh modules/linmp-scala/src/test/scrib/Greeting.scr Proto

For an explanation of Scribble syntax and the tool output, see the Greeting protocol tutorial.

Scribble Tutorial: Greeting Protocol

We now give an overview of Scribble syntax and the Scribble-Scala tool output, using the "Greeting protocol" example originally described in this ECOOP'16 paper.

Specifying an MPST Protocol in Scribble

Scribble provides a user-friendly, Java-inspired notation for defining structured "global protocols" among multiple participants. Such global protocols correspond to global types in MPST theory (cf. section "Global Types" in the paper, page 10).

The Scribble specification of the Greeting protocol is available in: /home/osboxes/scribble/modules/linmp-scala/src/test/scrib/Greeting.scr (and also here): 

module Greeting;

type <java> "java.lang.String" from "rt.jar" as String;

global protocol Proto(role c, role s) {
    choice at c {
        Greet(String) from c to s;
  choice at s {
            Hello(String) from s to c;
      do Proto(c, s);
        } or {
            Bye(String) from s to c;
        }
    } or {
        Quit() from c to s;
    }
}

The above defines a simple protocol between two participants, or roles: c (client) and s (server). The protocol can be read as follows:

For reference, the formal notation for the corresponding global type (see p.10, section "Global Types" in the paper) is: 

μX.c⟶s{
  Greet(String).s⟶c{ Hello(String).X, Bye(String).end },
  Quit(Unit).end
}

We now briefly explain the various elements appearing in the above Scribble specification:

NOTE: just like formal global types, this version of Scribble supports action prefixing: i.e., sequential composition of role-to-role message passing actions followed by other message actions, do statements or choice statements. However, sequential composition following a do or a choice is not permitted.

Running the Scribble-Scala tool on the Greeting protocol

Using the command line script: 

cd ~/scribble
./scribblec-linmp.sh modules/linmp-scala/src/test/scrib/Greeting.scr Proto

The output will be a set of Scala class definitions, similar to the following: 

// Global type (from modules/linmp-scala/src/test/scrib/Greeting.scr)
//    μ(Greeting_Proto___c__s_).c->s{Greet(String).s->c{Hello(String).Greeting_Proto___c__s_, Bye(String).end}, Quit(Unit).end}

// -----------------------------------------------------
// Local type for role s:
//    μ(Greeting_Proto___c__s_).c&{Greet(String).c⊕{Hello(String).Greeting_Proto___c__s_, Bye(String).end}, Quit(Unit).end}
package test.proto.s

import scala.concurrent.duration.Duration
import lchannels._

// Input message types for multiparty sessions
sealed abstract class MsgMPGreetOrQuit
case class Greet(p: String, cont: MPByeOrHello) extends MsgMPGreetOrQuit
case class Quit(p: Unit) extends MsgMPGreetOrQuit

// Output message types for multiparty sessions
case class Hello(p: String)
case class Bye(p: String)

// Multiparty session classes
case class MPGreetOrQuit(c: In[binary.GreetOrQuit]) {
  def receive(implicit timeout: Duration = Duration.Inf) = {
    c.receive(timeout) match {
      case m @ binary.Greet(p) => {
        Greet(p, MPByeOrHello(m.cont))
      }
      case m @ binary.Quit(p) => {
        Quit(p)
      }
    }
  }
}
case class MPByeOrHello(c: Out[binary.ByeOrHello]) {
  def send(v: Bye) = {
    val cnt = c ! binary.Bye(v.p)
    ()
  }
  def send(v: Hello) = {
    val cnt = c !! binary.Hello(v.p)_
    MPGreetOrQuit(cnt)
  }
}

// Classes representing messages (with continuations) in binary sessions
package object binary {
  sealed abstract class GreetOrQuit
  case class Greet(p: String)(val cont: Out[ByeOrHello]) extends GreetOrQuit
  case class Quit(p: Unit) extends GreetOrQuit

  sealed abstract class ByeOrHello
  case class Bye(p: String) extends ByeOrHello
  case class Hello(p: String)(val cont: Out[GreetOrQuit]) extends ByeOrHello
}
// -----------------------------------------------------

// -----------------------------------------------------
// Local type for role c:
//    μ(Greeting_Proto___c__s_).s⊕{Greet(String).s&{Hello(String).Greeting_Proto___c__s_, Bye(String).end}, Quit(Unit).end}
package test.proto.c

// ... [OMITTED]

// -----------------------------------------------------

We now explain the elements of the above tool output, and how the generated Scala APIs may be used to implement the session endpoints.

Note that an analogous set of classes (for input/output messages, multiparty sessions, binary channels) is also generated for the other roles of the global protocol. In this example, the only other role is s (for which we have omitted the resulting classes, in lines 59-63).

Using the Scribble-Generated Multiparty Session Classes

Now, the classes in the binary package could be used directly with lchannels (as described here) to implement type-safe point-to-point interactions between each pair of roles involved in a multiparty session. However, doing so has two drawbacks:

  1. a programmer would be (partly) exposed to the continuation-passing-style of lchannels, and
  2. if a multiparty session has n participants, a programmer implementing one of its participants would need to handle up to n-1 point-to-point channels, without any guidance on their usage order: this can introduce deadlocks (see §7 of the paper). This is not a problem for the greeting protocol (that only has two participants), but will be relevant, e.g., for the Game and ThreeBuyer examples later on.

These issues are addressed by the multiparty session classes MPGreetOrQuit and MPByeOrHello (seen above): they offer a simplified interface where a programmer only uses the input/output message classes Greet, Quit, Bye and Hello (seen above), without visible continuations. The binary classes (and their continuations) are handled internally by MPGreetOrQuit and MPByeOrHello, following the formalisation in §5 of the paper. Moreover, if a session involves more than two participants, the interface ensures that the interactions will not result in a deadlock.

Here is an implementation of the greeting protocol server, based on the multiparty session classes above. 

def server(c: MPGreetOrQuit)
          (implicit timeout: Duration): Unit = {
  c.receive match {
    case Greet(whom, cont) => {
      val c2 = cont.send(Hello(whom)) // Use "cont" to continue the session
      server(c2) // The return value of .send above allows to keep interacting
    }
    case Quit(()) => {
      () // The session is terminated
    }
  }
}

The code should be pretty self-explanatory. Note that all send calls are type-safe, and the Scala compiler will warn if a .receive match { ... } does not cover all possible input messages (depending on the state of the session). Also note that the multiparty session objects have the same runtime linearity usage rules of the underlying linear channels: i.e., the programmer is supposed to use each instance exactly once to send/receive a message. If .send()/.receive() is called twice on the same object, lchannels will throw a runtime exception (see the ECOOP'16 paper for more details).

One remaining question is: how does one produce an instance of MPGreetOrQuit, to invoke the server function above? Here is an example: 

// Create channel for local client/server interaction...
val (in, out) = LocalChannel.factory[binary.GreetOrQuit]
// ...and spawn server and client (note: we wrap channels in sesison objs)
val sf = Future { server(MPGreetOrQuit(in)) }
val cf = Future { client(...(out)) }

In other words, the caller creates a pair of linear channel endpoints connecting the client to the server, uses one of them to instantiate MPGreetOrQuit(in), and passes it to the server function. Note that the type of the parameter of MPGreetOrQuit constrains the carried type of the binary channel, that on line 2 must be binary.GreetOrQuit (or a subtype).

The example above uses LocalChannels for inter-thread communication, but a similar approach can be used with socket-based or Akka actor-based channels (both provided by lchannels), thus allowing server to interact with a remote client (indeed, the server code is independent from the message transport).

Implementation

An implementation of the greeting protocol, based on the Scribble-generated multiparty session classes, is available in ScribbleGreeting.scala. The file contains the autogenerated classes for both roles s and c, enclosed in different namespaces to avoid clashes.

The artifact demo script launches a greeting server and client interacting remotely, using Akka actor-based channels. The implementation, however, includes more examples, with the the greeting client/server launched as interacting threads, or the client talking through a socket with a simple server written in Python. If you want to try them, you can go to the lchannels installation directory and follow the lchannels documentation.

NOTE: the ScribbleGreeting.scala example is functionally equivalent to the pre-existing Greeting.scala example; the difference is that the latter interacts directly via lchannels without using Scribble-generated multiparty session classes.

HTTP (GET fragment)

This example implements fragment of the HTTP/1.1 protocol, focused on the GET method. The purpose is to show that our artifact is flexible enough to handle non-trivial "real-world" protocols, and produce endpoint code that is interoperable with existing (compliant) implementations of such protocols (in this example, existing Web browsers).

Similarly to the greeting protocol in the tutorial above, HTTP is a binary protocol --- i.e., a multiparty protocol with two roles (client and server). Its Scribble specification is available in /home/osboxes/scribble/modules/linmp-scala/src/test/scrib/Http.scr (and also here). Its only new feature is a recursive protocol block, that behaves as expected: 

rec X {
    choice at c {
        Host(String) from c to s;
        continue X;
    } or {
        UserAgent(String) from c to s;
        continue X;
    } or {
        ...
    } or {
        RequestBody(Body) from c to s;
        do Response(c, s);
    }
}

To generate the session classes from the Scribble HTTP specification, you can run: 

cd ~/scribble
./scribblec-linmp.sh modules/linmp-scala/src/test/scrib/Http.scr Http

Implementation Details

The Scribble-generated classes have been integrated in the HTTP server implementation. More in detail:

Running the HTTP Server

To run the HTTP server, you can launch the artifact demo script or follow the lchannels documentation. While the server is running, you can connect to http://127.0.0.1:8080/ with your browser. You can also "stress test" the implementation by recursively downloading all the files being served: 

cd /tmp
wget -l 100 -r http://127.0.0.1:8080/

NOTE: wget might report some transient read errors ("Connection reset by peer"), because our HTTP server does not currently observe the client's keep-alive requests. Still, the download will proceed through a new connection.

Example: Peer-to-Peer Game

This is the main running example in the paper (first introduced in §1), that concisely leverages all MPST features (session with more than two roles, branching, selection, recursion, delegation, inter-role dependencies, projection, merging). Its Scribble specification (corresponding to Figure 9 in the paper) is available in /home/osboxes/scribble/modules/linmp-scala/src/test/scrib/Game.scr (and also here).

Unlike the greeting protocol and HTTP examples, the game protocol involves three roles. Moreover, it features session delegation: 

global protocol ClientA(role p, role q) {
    PlayA(Game@a) from q to p;
}

global protocol ClientB(role p, role q) {
    PlayB(Game@b) from q to p;
}

global protocol ClientC(role p, role q) {
    PlayC(Game@c) from q to p;
}

global protocol Game(role a, role b, role c) {
    ...
}

Above, the message PlayA(Game@a) carries as payload a multiparty session channel: it allows the recipient to join an instance of the the Game protocol, by playing the role a. Here, "@" is the projection operator, and is one of our main additions to Scribble, based on the theory of our paper. It means that the type of the payload of PlayA(Game@a) is determined by projecting Game onto role a (cf. p.10 and §A.2 in the paper; note that before being projected, Game is first converted into the formal syntax for global types). The same intuition applies for messages PlayB(Game@b) and PlayC(Game@c). As one might expect, the projection of a Scribble global protocol G onto a role r is only allowed if r appears in G's declaration; e.g., in this example, Game can only be projected onto a, b and c.

Generating and Using the Session Classes

The Scribble specification above contains multiple global protocols, and each one can be used to generate multiparty protocol classes. Assume that we want to implement a Scala program that talks to the game server, and then plays role a: to do so, we can generate the session classes for the global protocol ClientA, and write our program using those pertaining to role p (recall that, from §1 of the paper, p is the client that receives the game delegation, while q is the game server). 

cd ~/scribble
./scribblec-linmp.sh modules/linmp-scala/src/test/scrib/Game.scr ClientA

Similarly, to implement roles b and c, we can specify respectively the global protocls ClientB and ClientC, and in both cases, use the Scribble-generated classes for the client role p to write our code.

Instead, if we want to implement the server, we will need all the Scribble-generated session classes obtained from ClientA, ClientB and ClientC --- but this time, we will need to write our code using those pertaining to the server role q. The reason is intuitive: the game server will need to interact with clients willing to play any role in the game; therefore, the server must implement the server-side of all the necessary protocols.

Implementation Details

Running the Game Example

To run the game example, you can launch the artifact demo script or follow the lchannels documentation. Note that the demo script will launch the example using distributed Akka actor-based channels; the lchannels documentation also includes a version where the server and clients run as local threads, using a non-distributed message transport.

Example: Three-Buyer Protocol

This is a widely-used example in MPST literature, inspired by a W3C Web Services Choreography use case (C-UC-001 Travel Agent). We use the version presented in the following paper: M. Coppo, M. Dezani-Ciancaglini, N. Yoshida, L. Padovani. "Global Progress for Dynamically Interleaved Multiparty Sessions". Mathematical Structures in Computer Science, 2016 (DOI).

Quoting from the paper:

The overall scenario, involving a Seller (s), Alice (a), Bob (b) and Carol (c), proceeds as follows.

  1. Alice sends a book title to Seller, then Seller sends back a quote to Alice and Bob. Then Alice tells Bob how much she can contribute.
  2. If the price is within Bob’s budget, Bob notifies both Seller and Alice he accepts, then sends his address, and Seller sends back the delivery date.
  3. If the price exceeds the budget, Bob asks Carol to collaborate together by establishing a new session. Then Bob sends how much Carol must pay, then delegates the remaining interactions with Alice and Seller to Carol.
  4. If the rest of the price is within Carol’s budget, Carol accepts the quote and notifies Alice, Bob and Seller, and continues the rest of the protocol with Seller and Alice transparently, as if she were Bob. Otherwise she notifies Alice, Bob and Seller to quit the protocol.

Similarly to the multiparty game, this example includes a three-party session --- here, involving the Seller and the two buyers Alice and Bob. Depending on Alice's choice, a third buyer (Carol) could be transparently involved by Bob, using session delegation.

The Scribble specification of this example is available in /home/osboxes/scribble/modules/linmp-scala/src/test/scrib/ThreeBuyer.scr (and also here): 

global protocol PlayAlice(role alice, role seller) {
    PlayAlice(TwoBuyer@alice) from seller to alice;
}

global protocol PlayBob(role bob, role seller) {
    PlayBob(TwoBuyer@bob) from seller to bob;
}

global protocol TwoBuyer(role alice, role bob, role seller) {
    Title(String) from alice to seller;
    QuoteA(Int) from seller to alice;
    QuoteB(Int) from seller to bob;
    ShareA(Int) from alice to bob;
    do TwoBuyerChoice(alice, bob, seller);
}

aux global protocol TwoBuyerChoice(role alice, role bob, role seller) {
    choice at bob {
        OkA() from bob to alice;
        OkS() from bob to seller;
        Address(String) from bob to seller;
        Deliver(ZonedDateTime) from seller to bob;
    } or {
        QuitA() from bob to alice;
        QuitS() from bob to seller;
    }
}


global protocol Delegation(role carol, role bob) {
    Contrib(Int) from bob to carol;  // Should be the Int on line 19
    Delegate(TwoBuyerChoice@bob) from bob to carol;
    choice at carol {
        OkC() from carol to bob;
    } or {
        QuitC() from carol to bob;
    }
}

We model this example by letting the Seller behave similarly to the server in the multiparty game. The Seller will wait for Alice's and Bob's connections, and then it will create a three-party session (based on the TwoBuyer protocol, on line 9) involving the Seller itself, Alice and Bob. For this purpose, the Seller first establishes binary sessions with Alice and Bob (based on the PlayAlice and PlayBob protocols, on lines 1 and 5); after they are connected, the Seller sends them the PlayAlice and PlayBob messages (lines 2 and 6), using delegation to let them join the three-party session.

The global protocol Delegation only involves Carol and Bob, and is used by the former to let Carol know how much she should contribute, and then pass her what is left of Bob's duties in the TwoBuyer session (specifically, Bob delegates the TwoBuyerChoice part of the session).

Generating and Using the Session Classes

The Scribble specification above contains multiple global protocols, and each one can be used to generate multiparty protocol classes. Assume that we want to implement a Scala program that talks to the Seller, and then plays role Alice: to do so, we can generate the session classes for the global protocol PlayAlice, and write our program using those pertaining to role alice. 

cd ~/scribble
./scribblec-linmp.sh modules/linmp-scala/src/test/scrib/ThreeBuyer.scr PlayAlice

Similarly, to implement role bob, we can specify the global protocls PlayBob, and use the Scribble-generated classes for role bob to write our code. Note, however, that to fully implement Bob and his interaction with Carol, we will also need bob's session classes generated from the Delegation global protocol.

Instead, if we want to implement the Seller, we will need all the Scribble-generated session classes obtained from PlayAlice and PlayBob, using those pertaining to role seller. The reason is that Seller will need to interact with both Alice and Bob, and must therefore implement the "other side" of both their protocols.

Finally, if we want to implement Carol, we need to specify the global protocol Delegation, and then use carol's session classes.

Implementation Details

This implementation adopts several solutions already seen in the game example.

Running the ThreeBuyer Example

To run the game example, you can launch the artifact demo script or follow the lchannels documentation. Note that the demo script will launch the example using distributed Akka actor-based channels; the lchannels documentation also includes a version where the server and clients run as local threads, using a non-distributed message transport.

Notes on Scribble with Scala API Extension

Implementation

Known Limitations

Building Scribble-Scala from Source

Prerequisites

Command Line Instructions

If all goes well, you will finally see a report like this: 

    [INFO] ------------------------------------------------------------------------
    [INFO] Reactor Summary:
    [INFO]
    [INFO] Scribble .......................................... SUCCESS [7.924s]
    [INFO] Scribble::Modules::Core ........................... SUCCESS [3:29.963s]
    [INFO] Scribble::Modules::Parser ......................... SUCCESS [7.706s]
    [INFO] Scribble::Modules::CLI ............................ SUCCESS [55.630s]
    [INFO] linmp-scala ....................................... SUCCESS [1.763s]
    [INFO] Scribble::Distribution ............................ SUCCESS [2.364s]
    [INFO] Scribble::Modules::Demos .......................... SUCCESS [0.145s]
    [INFO] ------------------------------------------------------------------------
    [INFO] BUILD SUCCESS
    [INFO] ------------------------------------------------------------------------
    [INFO] Total time: 4:45.961s
    [INFO] Finished at: Thu Jun 22 22:32:21 BST 2017
    [INFO] Final Memory: 30M/203M
    [INFO] ------------------------------------------------------------------------

Scribble-Scala is now ready to use via the scribblec-linmp.sh script in the project root directory, e.g., following the instructions here.