Multiparty Session Nets

Luca Fossati, Raymond Hu (homepage), Nobuko Yoshida (homepage)

2014-04-28 If you downloaded the Java APIs some time in the last few days and had a compilation error due to a missing file, please re-download and try again. Apologies for any inconvenience.

This page and the linked resources (e.g. the tool implementation) will continue to be updated

Abstract

This paper introduces global session nets, an integration of multiparty session types (MPST) and Petri nets, for role-based choreographic specifications to verify distributed multiparty systems. The graphical representation of session nets enables more liberal combinations of branch, merge, fork and join patterns than the standard syntactic MPST. We use session net token dynamics to verify a flexible conformance between the graphical global net and syntactic endpoint types, and apply the conformance to ensure type-safety and progress of endpoint processes with channel mobility. We have implemented Java APIs for validating global session graph well-formedness and endpoint type conformance.

Downloads:

Multiparty Session Nets paper: pdf (draft version)

Session Net Java APIs: tgz

These APIs allow the construction of global session graphs, well-formedness validation and endpoint type conformance checking. Java 7 or above is required. Please note: this is a preliminary working version that is still under development. See below for a tutorial. For any queries regarding the APIs, please contact Raymond Hu.

Examples To compile the packaged source and run all the examples of the above paper, from the parent directory of the extracted sessnet and test directories do the following. (Manually do mkdir bin first if required.)

javac sessnet/Examples.java -d bin
java -cp bin sessnet.Examples

txt

The list of examples (as per the main method of the Examples class compiled above) and what it means to "run" them is as follows. All references to figures, pages, etc. are with respect to the above paper.

Figure 1: constructs the graph (well-formed) and tests T₁ and T₄ from page 2 for conformance (both conformant).
Figure 2: constructs the role structure (correctly constructed).
Figure 3 (left): constructs the graph without the dotted components (well-formed).
Figure 3 (left) "bad entry": constructs the variant graph of Figure 3 (left) with the dotted components in the first B role structure (badly-formed due to a cycle with a transition entry node), as described in Section 2.2 on page 7.
Figure 3 (left) "bad exit": constructs the variant graph of Figure 3 (left) with the dotted components in the second A role structure (badly-formed due to a cycle with a transition exit node), as described in Section 2.2 on page 7.
Figure 3 (right): constructs the graph without the dotted components (badly-formed due to a cross-free diamond starting at a place and ending at a transition).
Figure 3 (right) "fixed": constructs the variant graph of Figure 3 (right) including the dotted components (well-formed).
Figure 4 (a): constructs the graph (badly-formed due to a diamond starting at a transition ending at a place).
Figure 4 (b): constructs the graph (badly-formed due to a cross-free diamond starting at a place ending at a transition).
Figure 4 (c): constructs the graph (badly-formed due to a branch along one side of a cross-free diamond that is not re-merged back to the diamond before the end of the diamond).
Figure 5: constructs the graph (well-formed) and tests T_A^bad and T_B^bad for conformance (both non-conformant).
Figure 5 "conformant": constructs the same graph as Figure 5 and tests endpoint types for each role for conformance (both conformant).
Figure 8: constructs the graph (badly-formed due to mismatched sets of roles along each branch path from the initial place).
Figure 8 "fixed": constructs a variant of the Figure 5 graph with an additional C role structure along the lower branch path (well-formed).
Figure 10: constructs the graph (well-formed).
Figure 12: constructs the graph (well-formed).

Using the Session Net Java APIs

(1) Global session graph construction

Global session graphs are most conveniently constructed using the

sessnet.net.builder.SessionGraphBuilder

utility class. We use the graph in Figure 3 (left) from the above paper as an example.

We first create a new SessionGraphBuilder. We then create the Place, Output, Input and InternalTransition objects (from the sessnet.net package) for each role structure.

SessionGraphBuilder b = new SessionGraphBuilder(); // First A role structure Place p1 = new Place("A"); Output oa = new Output("a"); // First B role structure Input ia = new Input("a"); Input ic = new Input("c"); Place p2 = new Place("B"); InternalTransition t = new InternalTransition(); Place p3 = new Place("B"); Output ob = new Output("b"); // Second A role structure Input ib = new Input("b"); Place p4 = new Place("A"); Output oc = new Output("c"); Output od = new Output("d"); // Final B role structure Input id = new Input("d"); Place p5 = new Place("B");

After creating the various place and transition objects, the SessionGraphBuilder (b) is used to construct each role structure by declaring the nodes and edges via its role structure builder (b.rsb) and input/output role tree builder (b.rsb.ib and b.rsb.ob) helper subcomponents.

The first A role structure is constructed by:

// Construct the first A RS b.rsb.addCorePlace(p1); // Set the core place (adds to both IRT and ORT) // There are no further nodes in the IRT b.rsb.ob.addLeaves(oa); // The ORT has one leaf.. b.rsb.ob.addEdge(p1, oa); // ..and one edge b.addRoleStructure(); // Finalise the RS

The addRoleStructure method finalises the role structure being assembled (and checks that it has been correctly constructed) and resets the state of the role structure and input/output role tree builders.

The first B RS is constructed as follows.

// Construct the first B role structure b.rsb.addCorePlace(p3); // Set the core place b.rsb.ib.addLeaves(ia, ic); // The IRT has two leaves.. b.rsb.ib.addOtherNodes(p2, t); // ..and two additional nodes b.rsb.ib.addEdge(ia, p2); // Connect the IRT nodes b.rsb.ib.addEdge(p2, t); b.rsb.ib.addEdge(t, p3); b.rsb.ib.addEdge(ic, p3); b.rsb.ob.addLeaves(ob); // The ORT has one leaf.. b.rsb.ob.addEdge(p3, ob); // ..and one edge b.addRoleStructure(); // Finalise the RS

The other two role structures are constructed similarly. Finally, we add the communication places between the outputs and inputs to the graph, and finalise the whole graph with the role structures constructed so far.

// Add the communication places (the edges are added implicitly) b.addCommunicationPlace(oa, ia); b.addCommunicationPlace(ob, ib); b.addCommunicationPlace(oc, ic); b.addCommunicationPlace(od, id); Session Graph g = b.makeSessionGraph(); // Finalise the whole graph

Finalising the graph checks resets the state of the builder object.

(2) Well-formedness validation

The makeSessionGraph method finalises the session graph and checks that it has been correctly constructed and is well-formed.

For example, consider the following modification of the graph from (1) above (corresponding to the Figure 3 (left) "bad entry" example):

This may be constructed by replacing the code for the first B role structure with the following. The remainder of the code for this new graph is the same as above.

// Modified B role structure Place pp = new Place("B"); // An additional RS place is needed b.rsb.addCorePlace(p3); b.rsb.ib.addLeaves(ia, ic); b.rsb.ib.addOtherNodes(p2, t, pp); // The IRT has the extra place b.rsb.ib.addEdge(ia, p2); b.rsb.ib.addEdge(p2, t); b.rsb.ib.addEdge(t, p3); b.rsb.ib.addEdge(ic, pp); // Connect ?c to t via pp b.rsb.ib.addEdge(pp, t); b.rsb.ob.addLeaves(ob); b.rsb.ob.addEdge(p3, ob); b.addRoleStructure();

This graph is badly-formed because there is cycle with a transition entry node: the cycle is t -> B -> !b -> ?b -> A -> !c -> ?c -> t (omitting the unlabelled places) with entry path A -> !a -> ?a -> t. As explained in the above paper, the well-formedness condition that has been violated is (C1) in Definition 2.3.

When the final makeSessionGraph method is called, the following exception will be raised (modulo the integer identifier for the offending transition):

Well-formedness error: Entry node of cycle must be a place: Tau<87>

The API raises similar exceptions when any of the other well-formedness conditions are violated, indicating the problematic node or nodes.

(3) Endpoint type conformance

Provided a graph has been correctly constructed and is well-formed, the makeSessionGraph builder method returns a sessnet.net.SessionGraph object.

To test an endpoint type for conformance, we first construct the sessnet.endpoint.EndpointType object that represents the syntactic type. Note: the API for constructing endpoint types in the following example is an intermediate interface intended as a parser target rather than a direct user interface.

Here we create an EndpointType for T_A^bad (!B<a>.?B<b>.!B<c>.?B<d>.end) for the role A from the Figure 5 example.

// Construct the endpoint type: !B<a>.?B<b>.!B<c>.?B<d>.end EndpointType e; Map<Message, EndpointType> cases; //For convenience, we construct the type "backwards" e = new EndType("A"); cases = new HashMap<>(); cases.put(new Message("B", "A", "d"), e); e = new InputType("A", cases); cases = new HashMap<>(); cases.put(new Message("A", "B", "c"), e); e = new OutputType("A", cases); cases = new HashMap<>(); cases.put(new Message("B", "A", "b"), e); e = new InputType("A", cases); cases = new HashMap<>(); cases.put(new Message("A", "B", "a"), e); e = new OutputType("A", cases);

To test conformance, we then create an initial net from the session graph and pass the above EndpointType as an argument to the isConformant method of the net object.

// sg is a reference to the SessionGraph object for Figure 5 SessionNet net = sg.makeInitialNet(); System.out.println("Checking: " + e); // e is the EndpointType from above System.out.println("Conformance: " + net.isConformant(e));

The above code generates the following output:

Checking: A!{B<a>.A?{B<b>.A!{B<c>.A?{B<d>.end}}}} Conformance: false

Note: the EndpointType API, in comparison to the formal endpoint type syntax defined in the above paper, additionally prints the subject (i.e. A) in the branch and select types before the ! and ? symbols.

2014-04-29.