Scribble-Java tutorial

This is a tutorial for using the Scribble-Java toolchain (for Scribble version 0.4).

Contents:

  1. About this tutorial

  2. Quick Start: the Adder application protocol
    1. Protocol overview
    2. Scribble global protocol
    3. An Adder client
    4. An Adder server

  3. Scribble modules and global protocols
    1. Scribble modules
    2. Message signatures
    3. Global protocol declarations
    4. The message interaction statement
    5. The choice statement
    6. The do statement

  4. Further global protocol features
    1. Message signature name declarations
    2. The connection interaction statement

  5. Scribble protocol validation
    1. Valid global protocols and well-formed modules
    2. Characteristics of Endpoint FSMs
    3. Safety and liveness of Scribble global protocols

  6. Endpoint API generation
    1. Endpoint API overview
    2. Names as singleton types
    3. State Channel API
    4. Output state API
    5. Receive state API
    6. Accept state API
    7. Disconnect state API
    8. Linear usage of state channel instances

  7. Endpoint implementation using Scribble-generated APIs
    1. Connection establishment for non-explicit global protocols
    2. Usage contract of Endpoint APIs and endpoint implementation safety

  8. Building/installing Scribble-Java

  9. Running the Scribble-Java command line tool

About this tutorial

Scribble-Java is a toolchain for programming distributed applications in Java based on the theory of multiparty session types.

The main input and output of the toolchain are:

Useful links and resources

Tutorial version history

Upcoming in future tutorial versions

Upcoming in future Scribble versions

< top; next >

Quick Start: the Adder application protocol

This quick start will run through the specification of a simple application protocol in Scribble, to Java implementations of client and server endpoints using the Scribble-generated APIs.

< prev; top; next >

Protocol overview

We illustrate a client-server protocol for a network service that adds two numbers.

An outline of the protocol:

< prev; top; next >

Scribble global protocol

Below we give a Scribble specification of the Adder application protocol.

This code is available from the Scribble GitHub repository:

Adder.scr

Lst. 2.1: Scribble specification of the Adder application protocol.
   
  1. module tutorial.adder.Adder;
  2.  
  3. type <java> "java.lang.Integer" from "rt.jar" as Int;
  4.  
  5. global protocol Adder(role C, role S) {
  6.     choice at C {
  7.         Add(Int, Int) from C to S;
  8.         Res(Int) from S to C;
  9.         do Adder(C, S);
  10.     } or {
  11.         Bye() from C to S;
  12.     }
  13. }

We use the above example to give a brief overiew of Scribble syntax. The links give further details of each element.

< prev; top; next >

Running the Scribble-Java command line tool

The command given below assumes:

In a Linux, Cygwin/Windows, or Mac OS terminal, the command is: 

    ./scribblec.sh scribble-demos/scrib/tutorial/src/tutorial/adder/Adder.scr -api Adder C -d scribble-demos/scrib/tutorial/src/

The above command performs the following tasks.

See here for more information on using the command line tool.

< prev; top; next >

An Adder client

We use the Endpoint API generated in the previous step to summarise the key elements behind Scribble Endpoint APIs.

We then give an example implementation using the above Endpoint API.

< prev; top; next >

Endpoint FSM

Below is the endpoint finite state machine (FSM) for the C role in Adder.

Fig. 2.3.1: The FSM for C in Adder.

< prev; top; next >

Endpoint API overview

So that they may be used as types in Java, Scribble generates the various role and operator names in the source protocol as singleton types. For the Adder protocol, Scribble generates the following singleton types as API constants:

Roles C, S
Operators   Add, Res, Bye

The API generation renders each state in the Endpoint FSM as a Java class for a state-specific communication channel (which we call a state channel for short).

See here for an example Javadoc generated (by the standard javadoc tool) from the Scribble-generated API for C in Adder.

The following summarises the key state channel classes and their I/O methods.

Adder_C_1 (state 1 in the FSM).

Type Method
Adder_C_2   send(S role, Add op, Integer arg0, Integer arg1)
EndSocket send(S role, Bye op)

Adder_C_2 (state 2 in the FSM).

Type Method
Adder_C_1   receive(S role, Res op, Buf<? super Integer> arg0)

EndSocket (state 3 in the FSM) has no I/O methods.

We explain the Endpoint API for S later. It features the API generation for non-unary receive (i.e., branch) states, which is not demonstrated by the API for C.

< prev; top; next >

Endpoint implementation

Usage contract of Scribble-generated Endpoint APIs

Starting from an instance of the initial state channel, an endpoint implemention should proceed by calling one method on the current channel to obtain the next, up to the end of the protocol (if any).

Below we give an example implementation of a C endpoint in an application of Adder. We use the Scribble-generated API following the above usage contract. This client uses the Adder service to calculate the n-th Fibonacci number.

The full code is available from the Scribble GitHub repository:

AdderC.java

Lst. 2.3.1: Java implementation of a C endpoint in Adder using the Scribble-generated API.
   
  1. package tutorial.adder;
  2.  
  3. /* Imports omitted */
  4.  
  5. public class AdderC {
  6.  
  7.     public static void main(String[] args) throws Exception {
  8.         Adder adder = new Adder();
  9.         try (MPSTEndpoint<Adder, C> client =
  10.                     new MPSTEndpoint<>(adder, C, new ObjectStreamFormatter())) {    
  11.             client.connect(S, SocketChannelEndpoint::new, "localhost", 8888);
  12.             int n = 10;
  13.             System.out.println(n + "th Fibonacci number: "
  14.                     + fibo(new Adder_C_1(client), n));
  15.         }
  16.     }
  17.     
  18.     private static int fibo(Adder_C_1 c1, int n) throws Exception {
  19.         Buf<Integer> x = new Buf<>(0);
  20.         Buf<Integer> y = new Buf<>(1);
  21.         Buf<Integer> i = new Buf<>(1);
  22.         while (i.val < n) {
  23.             Adder_C_2 c2 = c1.send(S, Add, x.val, y.val);
  24.             x.val = y.val;
  25.             c1 = c2.receive(S, Res, y);
  26.             c1 = add1(c1, i);
  27.         }
  28.         c1.send(S, Bye);  // EndSocket
  29.         return x.val;
  30.     }
  31.  
  32.     private static Adder_C_1 add1(Adder_C_1 c1, Buf<Integer> i) throws Exception {
  33.         return c1.send(S, Add, i.val, 1).receive(S, Res, i);
  34.     }
  35. }

We summarise the key elements in the above code.

The main method contains a typical preamble for an implemention of a client endpoint using an Endpoint API.

The fibo method contains the main body of the protocol implementation using the Endpoint API explained earlier. It takes the initial state channel, Adder_C_1, and follows the protocol through to the terminal state channel, EndSocket, returned by c1.send(S, Bye).

< prev; top; next >

An Adder server

Endpoint implementation

We give an example implementation of an S server for Adder. We highlight the features that are different or not shown in the example client implementation.

The full code is available from the Scribble GitHub repository:

AdderS.java

Lst. 2.3.2: Java implementation of a S endpoint in Adder using the Scribble-generated API.
   
  1. package tutorial.adder;
  2.  
  3. /* Imports omitted */
  4.  
  5. public class AdderS {
  6.  
  7.     public static void main(String[] args) throws Exception {
  8.         try (ScribServerSocket ss = new SocketChannelServer(8888)) {
  9.             while (true) {
  10.                 Adder adder = new Adder();
  11.                 try (MPSTEndpoint<Adder, S> server
  12.                             = new MPSTEndpoint<>(adder, S, new ObjectStreamFormatter())) {
  13.                     server.accept(ss, C);
  14.                     new AdderS().run(new Adder_S_1(server));
  15.                 } catch (ScribbleRuntimeException | IOException | ClassNotFoundException e) {
  16.                     e.printStackTrace();
  17.                 }
  18.             }
  19.         }
  20.     }
  21.  
  22.     private void run(Adder_S_1 s1) throws Exception {
  23.         Buf<Integer> x = new Buf<>();
  24.         Buf<Integer> y = new Buf<>();
  25.         while (true) {
  26.             Adder_S_1_Cases cases = s1.branch(C);
  27.             switch (cases.op) {
  28.                 case Add: s1 = cases.receive(Add, x, y)
  29.                                     .send(C, Res, x.val+y.val); break;
  30.                 case Bye: cases.receive(Bye);                   return;
  31.             }
  32.         }
  33.     }
  34. }

< prev; top; next >

Scribble modules and global protocols

This section describes the syntax of Scribble modules and global protocols in more detail. It describes the syntactic constraints imposed by Scribble on global protocol definitions.

< prev; top; next >

Scribble modules

A Scribble module is a file with the following elements, in order.

The notion of well-formed module is discussed here.

< prev; top; next >

Message signatures

A message signature specifies the key elements of a message. 

    op ( pay1, ..., payn )

< prev; top; next >

Global protocol declarations

A Scribble global protocol describes the interactions between the participants of a communication session from the global (i.e., neutral) perspective. A Scribble protocol abstracts session participants as named roles. Sessions are sometimes referred to as conversations.

Scribble protocols are strictly explicit about session interactions -- the only application-level messages to be communicated in a Scribble session are those that are explicitly specified in the protocol. 

    global protocol MyProto(role r1, ..., role rn) {
        ...
    }

< prev; top; next >

The message interaction statement

A message interaction is a role-to-role pairing of a send action and a receive action of a message.

The message may be specified as a message signature, i.e., an operator and a payload: 

		op(pay) from r1 to r2;

or as a message signature name: 

		Msg from r1 to r2;

In both cases, r1 is the sender role and r2 is the receiver role.

The communication model of Scribble is that message delivery is output-asynchronous, reliable, and ordered in each direction between each pair of roles. Output-asynchronous means the send action is non-blocking for the sender, but the receive action is blocking for the receiver (i.e., until the message arrives). This model caters for applications using, e.g., TCP channels, or (unbounded) FIFOs in shared memory.

Send actions are considered output actions, and receive actions are considered input actions.

< prev; top; next >

The choice statement

The choice statement designates a branch point in the protocol. The protocol proceeds according to one of the or-separated cases. 

    choice at r { ... } or ... or { ... }

A choice statement is subject to the following syntactic constraints.

< prev; top; next >

The do statement

The do statement instructs the specified roles to perform the interactions of the specified protocol inline with the current session. 

do MyProto(r1, ..., rn);

In other words, each role in the role argument list plays the corresponding role in the role declaration list of the target protocol declaration.

< prev; top; next >

Recursive protocols

A do statement may be used to define (mutually) recursive protocols.

In addition to the previously stated constraints on do statements, Scribble global protocol definitions must be tail recursive per role. This means:

< prev; top; next >

Further global protocol features

Message signature name declarations

Message signature name declarations may occur alongside payload type declarations. 

    sig <java> "javapackage.JavaClass" from "myjar.jar" as MyMessage;

In message interactions that specify message signature names, the message signature name itself is used to identify the message (cf. the operator in a message signature).

< prev; top; next >

The connection interaction statement

A global protocol declaration may have the modifier explicit. 

    explicit global protocol MyProto(...) { ... }

The communication model of a non-explicit global protocol starts with all roles pairwise connected by binary channels.

By contrast, the communication model of an explicit global protocol starts with all roles unconnected. A pair of roles are connected by: 

    connect r1 to r2;

A connection interaction is a role-to-role pairing of a connection request action and a connection accept action. Role r1 is the client role, and r2 is the server role.

A connection interaction is a synchronous interaction between the client and server, i.e., the first role to perform either connection action is blocked until the other role performs the counterpart action. The connection interaction establishes a bidirectional binary (i.e., two-party) channel with the characteristics of the Scribble communication model, i.e. message delivery is reliable and ordered in each direction.

A pair of roles are disconnected by: 

    disconnect r1 and r2;

Each of the two disconnect actions in the above pairing is a local action, i.e. it does not directly pertain to any interaction between the two roles. A disconnect action closes the input queue at the local endpoint of the binary channel between these two roles.

In the context of Scribble, request actions are considered output actions, and accept actions are considered input actions.

An explicit global protocol is subject to the following syntactic constraints.

This means there is at most one connection between any two roles.

< prev; top; next >

Scribble protocol validation

This section describes the notion of whether a global protocol is valid in Scribble.

< prev; top; next >

Valid global protocols and well-formed modules

Scribble validates that a global protocol satisfies a set of desirable properties. These include safety properties, such as no reception errors (a role never receives an unexpected message), and liveness properties, such as eventual reception (a sent message can always eventually be received).

A Scribble global protocol is validated by two steps.

Specifically, the second step is conducted on a 1-bounded model of the protocol. That is, the model given by the exhaustive execution of the system of Endpoint FSMs where each communication channel is limited to a maximum capacity of one message in each direction.

The Scribble validation of global protocols is sound. This means a valid protocol satisfies the safety and liveness properties in the general setting, i.e., the system of Endpoint FSMs with unbounded channels. Soundness is due to the characteristics of the protocol (i.e., the restrictions on endpoint behaviours) imposed by syntactic well-formedness.

Well-formed modules

A module is well-formed if every global protocol in the module is valid.

< prev; top; next >

Characteristics of Endpoint FSMs

The Endpoint FSM for any role of a syntactically well-formed Scribble global protocol has the following characteristics.

< prev; top; next >

Safety and liveness of Scribble global protocols

We first introduce some terminology.

A valid Scribble global protocol satisfies the following safety properties.

A valid Scribble global protocol satisfies the following liveness properties.

Fairness of output choice implementations

Scribble supports an option to consider unfair endpoint implementations of the choice between actions at output states. Here, "unfair" means that the implementation of the choice may never perform a particular action, even if the choice may be repeated infinitely often (i.e., in a recursive protocol).

For this option, Scribble adopts a "worst case" view where endpoint implementations exercise a minimal number of output choice options during session execution. This is affected by a model transformation that commits a role to perform again the same action whenever an output state is revisited.

See here for the instructions on enabling or disabling this option in the command line tool.

< prev; top; next >

Endpoint API generation

This section describes the generation of protocol-specific Java Endpoint APIs by Scribble in more detail.

< prev; top; next >

Endpoint API overview

An Endpoint API for a role in a global protocol has two parts.

For a global protocol, e.g. Adder, in the Scribble module tutorial.adder.Adder, Scribble generates the Session Class as follows.

An Endpoint API uses classes from the base Scribble API, which will be referred to in the following sections.

< prev; top; next >

Names as singleton types

A global protocol may feature several kinds of names: roles, message operators and message signature names.

Scribble generates a Java singleton type for each of these names. The following illustrates the code generated for the C role in Adder. 

    package tutorial.adder.Adder.Adder.roles;

    public final class C extends org.scribble.sesstype.name.Role {
        private static final long serialVersionUID = -6429099329627603991L;
        public static final C C = new C();
        private C() {
            super("C");
        }
    }

The generation for message operators and message signature names is similar.

For convenience, the Session Class is also generated with field constants referring to the singleton type instances. E.g., the Adder Session Class has the following fields: 

    public static final C C = tutorial.adder.Adder.Adder.roles.C.C;
    public static final S S = tutorial.adder.Adder.Adder.roles.S.S;
    public static final Add Add = tutorial.adder.Adder.Adder.ops.Add.Add;
    public static final Bye Bye = tutorial.adder.Adder.Adder.ops.Bye.Bye;
    public static final Res Res = tutorial.adder.Adder.Adder.ops.Res.Res;

< prev; top; next >

State Channel API

The generation of a State Channel API for a role in a global protocol is based on the Endpoint FSM of that role.

Assume a valid global protocol G in a well-formed module mypack.MyMod. Let s be a state in the Endpoint FSM of G for role r.

If s is a terminal state in the Endpoint FSM, the Scribble generates:

N.B. Henceforth, references to a class G_r_s where s is a terminal state should be considered as EndSocket.

Otherwise (i.e., if s is not a terminal state):

< prev; top; next >

Output state API

Let:

For each send action ai to receiver role r_i for message m:

The send methods are generated to return without blocking.

For each connect action ai to receiver role r_i, Scribble generates an instance method in class G_r_s: 

    public G_r_si connect(ri role, Callable<? extends BinaryChannelEndpoint> cons, String host, int port)
            throws ScribbleRuntimeException, IOException

The connect method is generated to block until the connection is established or an exception is thrown.

< prev; top; next >

Receive state APIs

Let:

If s is a unary receive state, i.e., n = 1, and a1 specifies message m, then:

The receive methods are generated to block until a message is received.


Otherwise, i.e., n > 1, Scribble generates:

The branch method is generated to block until a message is received.

For each (receive) action ai from sender r' for message mi:

org.scribble.net.Buf<T> is a utility class in the Scribble API.

The receive methods in both of the above cases are generated to write the each of the received payload values or message object to the val field of the corresponding Buf argument before returning.

< prev; top; next >

Accept state API

Let:

Scribble generates an instance method in class G_r_s: 

    public G_r_s1 accept(ri role, ScribServerSocket ss) throws ScribbleRuntimeException, IOException

The accept method is generated to block until the connection is established or an exception is thrown.

< prev; top; next >

Disconnect state API

If s is a disconnect state in the Endpoint FSM of G for role r:

< prev; top; next >

Linear usage of state channel instances

Scribble enforces a linear usage discipline on state channel instances, by generating run-time checks into the Endpoint API. This means an endpoint implementation should invoke one I/O method on every instance of a state channel, apart from EndSocket. The following situations throw a ScribbleRuntimeException.

< prev; top; next >

Endpoint implementation using Scribble-generated APIs

This section describes additional details of endpoint implementation using Scribble-generated APIs and the associated safety properties.

< prev; top; next >

Connection establishment for non-explicit global protocols

Endpoint implementation using an Endpoint API generated from a non-explicit global protocol relies on a connection establishment phase between creating the MPSTEndpoint and the initial state channel.

Client-side connection requests

The following is from the example implementation of a C client in Adder. 

    Adder adder = new Adder();
    try (MPSTEndpoint<Adder, C> client =
                new MPSTEndpoint<>(adder, C, new ObjectStreamFormatter())) {
        client.connect(S, SocketChannelEndpoint::new, "localhost", 8888);
        /* Body of endpoint implementation, starting from new Adder_C_1(client)*/
    }

Client-side connection requests are peformed by the connect method of MPSTEndpoint. 

    client.connect(S, SocketChannelEndpoint::new, "localhost", 8888);

The above method has the same signature as the State Channel API connect method generated for explicit connect actions.

Server-side connection accepts

The following is from the example implementation of a S server in Adder. 

    try (ScribServerSocket ss = new SocketChannelServer(8888)) {
        while (true) {
            Adder adder = new Adder();
            try (MPSTEndpoint<Adder, S> server
                    = new MPSTEndpoint<>(adder, S, new ObjectStreamFormatter())) {
                server.accept(ss, C);
                new AdderS().run(new Adder_S_1(server));
            } catch (ScribbleRuntimeException | IOException | ClassNotFoundException e) {
                e.printStackTrace();
            }
        }
    }

Server-side connections are accepted via an instance of org.scrible.net.scribsock.ScribServerSocket. 

    try (ScribServerSocket ss = new SocketChannelServer(8888)) { ... }

A connection is accepted by the accept method of MPSTEndpoint. 

    server.accept(ss, C);

Safety warning for non-explicit connection actions

The actions performed in a non-explicit connection phase are not verified in any way. This means it is up to the programmer to avoid errors such as the following.

< prev; top; next >

Usage contract of Endpoint APIs and endpoint implementation safety

The following is the API usage contract for endpoint implementations using Scribble-generated Endpoint APIs.

Starting from an instance of the initial state channel, an endpoint implemention should proceed by calling one method on the current channel to obtain the next, up to the end of the protocol (if any).

An Endpoint API is generated to throw a ScribbleRuntimeException at run-time if the above rule, i.e. linear usage of state channels, is violated. The I/O action of the offending method invocation will not be performed.

Note that the only way that an endpoint implementation using an Endpoint API may attempt to violate the protocol is by violating state channel linearity. This confers the following form of safety for Scribble endpoint implementations.

< prev; top; next >

Building/installing Scribble-Java

The source code of the master version of Scribble-Java is available from GitHub.

We give basic instructions for two ways of building the Scribble-Java tool from source. Both ways will create the file 

    dist/target/scribble-dist-0.4-SNAPSHOT.zip

under the root directory of the scribble-java project.

Building Scribble-Java using command line Maven

These instructions have been tested on Ubuntu 16.04.2 using:

From the root directory of the scribble-java project:


Building Scribble-Java using Eclipse

These instructions have been tested for:

N.B. Eclipse must be configured to use a JDK 8 (Preferences → Java → Installed JREs).

Steps:

Installing the Scribble-Java command line tool

The scribble-dist-0.4-SNAPSHOT.zip built by the above instructions contains:

The script is immediately executable after extracting the zip contents.

Alternatively, the script is executable from the scribble-java root directory, without lib, by:

< prev; top; next >

Running the Scribble-Java command line tool

Assuming the scribblec.sh script is installed at the current directory, various command line options are shown by: 

    ./scribblec.sh --help

The following summarises a few options mentioned in this tutorial:

-ip import_path     Sets the import path for module imports.
-fair Disables the model transformation and checking for "unfair" endpoint implementations.

A command for validating the example Adder protocol and generating the API for the C role was given here.

Further examples of using the scribblec.sh script can be found in this README.

< prev; top; >