Multiparty Session Nets

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

2014-05-16 The Session Nets Java API (and this page) have been updated. The previous version can be found here.

Updates to this page and the linked resources (e.g. the tool implementation) are continuing

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 src directory do the following. (Manually do mkdir bin first if required.)

javac -sourcepath src src/sessnet/test/concur14/Examples.java -d bin
java -cp bin sessnet.test.concur14.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 the Place, Output, Input and InternalTransition objects (from the sessnet.net package) for the initial A role structure.

// Nodes for the initial A role structure Place p1 = new Place("A"); Output oa = new Output("a");

After creating the various place and transition objects, we use a SessionGraphBuilder (sgb) to assemble the role structure by declaring the nodes and edges via its input/output role tree builder (sgb.irt and sgb.ort) helper subcomponents. The role structure is assembled by:

SessionGraphBuilder sgb = new SessionGraphBuilder(); // Construct the first A RS sgb.nextCorePlace(p1); // Set the core place (adds place to both the IRT and ORT) sgb.ort.addEdge(p1, oa); // The ORT has one edge (the node is added implicitly) sgb.finishRoleStructure(); // Finalise the RS

The finishRoleStructure method finalises the role structure being assembled (checking that it has been correctly constructed) and resets its state for assembling the next role structure.

The first B RS is constructed as follows.

// Nodes for the 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"); // Assemble the first B role structure sgb.nextCorePlace(p3); // Set the core place sgb.irt.addEdge(ia, p2); // The IRT has one edge sgb.irt.addEdge(p2, t); // The ORT is a fork with two leaves sgb.irt.addEdge(t, p3); sgb.irt.addEdge(ic, p3); sgb.ort.addEdge(p3, ob); sgb.finishRoleStructure(); // Finalise the RS

The other two role structures are constructed similarly.

// Second A role structure Input ib = new Input("b"); Place p4 = new Place("A"); Output oc = new Output("c"); Output od = new Output("d"); sgb.nextCorePlace(p4); sgb.irt.addEdge(ib, p4); sgb.ort.addEdge(p4, oc); sgb.ort.addEdge(p4, od); sgb.finishRoleStructure(); // Final B role structure Input id = new Input("d"); Place p5 = new Place("B"); sgb.nextCorePlace(p5); sgb.irt.addEdge(id, p5); sgb.finishRoleStructure();

Finally, we add the communication places between the outputs and inputs to the graph, and finalise the whole graph with the role structures and communication places assembled 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 and check its construction

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. Using the makeWellFormedSessionGraph instead will additionally check that the session graph 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"); // Adding an additional RS place sgb.nextCorePlace(p3); sgb.irt.addEdge(ia, p2); sgb.irt.addEdge(p2, t); sgb.irt.addEdge(t, p3); sgb.irt.addEdge(ic, pp); // Connect ?c to t via the extra place pp sgb.irt.addEdge(pp, t); sgb.ort.addEdge(p3, ob); sgb.finishRoleStructure();

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.

If makeWellFormedSessionGraph method is called on the builder, the following exception will be raised (modulo the integer identifier for the offending transition):

Well-formedness error: Entry/exit node of cycle must be a place: tau<77>

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 makeWellFormedSessionGraph builder method returns a sessnet.net.WellFormedSessionGraph object.

To test an endpoint type for conformance, we create the sessnet.endpoint.EndpointType object that represents the syntactic type.

Using sessnet.endpoint.Parser, 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. Note: the parser currently accepts only the formally defined endpoint type grammar in Section 3 of the above paper (with $\mu$ replaced by rec); it does not accept the sugared notation used in e.g. Figure 5.

Parser parser = new Parser(); String TA_bad = "!{B<a>.?{B<b>.!{B<c>.?{B<d>.end}}}}"; EndPointType et = parser.parse("A", TA_bad);

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 WellFormedSessionGraph object for Figure 5 SessionNet net = sg.makeInitialNet(); System.out.println("Checking: " + et); // et is the EndpointType from above System.out.println("Conformance: " + net.isConformant(et));

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-05-16.