Composition

Composition is achieved through binary actions that compose 2 processes together. Although there is some high level user control over the actions, the composition is automated and strictly follows the rules of linear logic.

The result is an intermediate composite process specified by its input and output resources and a correct-by-construction, executable π-calculus definition. These processes can then be further composed using subsequent actions.

Performing an action involved the production and maintenance of a temporary internal state called an actionstate. This provides additional metadata about how a composition was achieved.

Actions

Binary composition actions have the following structure:

 1module Action = struct
 2
 3  type t = {
 4    act : string;
 5    larg : string;
 6    lsel : string;
 7    rarg : string;
 8    rsel : string;
 9    res : string ;
10  }
11
12(*...*)
13end;;

The fields can be described briefly as follows:

By default there are 3 available composition actions:

1. TENSOR: Parallel composition.
2. WITH: Conditional composition.
3. JOIN: Sequential composition.

These are described in more detail below.

Each action is associated with an implemented reasoning process (or tactic) in HOL Light. There is an internal associative map between tactic names and their actual implementation.

These reasoning processes follow the rules of linear logic in a formally verified way, with the associated guarantees of correctness we have discussed. This may sometimes lead to results in terms of input and output types for the composite process that may be more complex than expected. Though such results may seem unintuitive at first, their correctness is mathematically guaranteed, with an enforced systematic accounting of all resources (linearity). Small examples of this appear in our description of the actions below.

Selector arguments allow users to specify a specific part of each composed process. These arguments have a different use in each action, but allow a high level of user control.

Parallel - TENSOR

The TENSOR action composes two processes in parallel. This results in a composite process with all the inputs of both processes and their two outputs composed in a single parallel output.

Its name corresponds to the ⊗ operator (pronounced times or tensor), which denotes parallel resources.

Selector arguments

Selector arguments are unused in the TENSOR action.

Example

As an example, the result R of the parallel composition of a process P with input X and output A ++ B and a process Q with inputs Y and Z and output C is the following process:

 1{name = "R";
 2  inputs = [(`X`, `cP_X_1`); (`Y`, `cQ_Y_1`); (`Z`, `cQ_Z_2`)];
 3  output = (`(A ++ B) ** C`, `c_Step0___Step0__z1`);
 4  prov =
 5    Provnode ("times", Provnode ("plus", Provleaf "P", Provleaf "P"),
 6              Provleaf "Q");
 7  proc =
 8    `R (cP_X_1,cQ_Y_1,cQ_Z_2,c_R___R__z1) =
 9      PiTimesProc (A ++ B) C c_R___R__z1 oP_lB_A_Plus_B_rB_ oQ_C_
10        (P (cP_X_1,oP_lB_A_Plus_B_rB_))
11        (Q (cQ_Y_1,cQ_Z_2,oQ_C_))`;
12  actions =
13      [{Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = "";
14        res = "R"}];
15  copier = false;
16  intermediate = true}

The action used can be noticed in the actions field above and is as follows:

1{Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = ""; res = "R"}

Conditional - WITH

The WITH action composes two processes conditionally.

More specifically, given an input X of a process P and a Y input of a process Q, their conditional composition yields a process with an optional input X ++ Y, i.e. one that can accept X or Y (but not both). If the composite process receives X then P will be executed. Otherwise if the composite process receives Y then Q will be executed.

Its name corresponds to the & operator (pronounced with), which denotes optional input resources.

Selector arguments

Selector arguments are used in the WITH action to specify which inputs should be used in the composite conditional input. The user needs to provide the resource type of the input to be used from each process.

Example

As an example, the result R of the conditional composition of a process P with input X and output A ++ B and a process Q with inputs Y and Z and output C with inputs X and Y selected is the following process:

 1{name = "R";
 2  inputs = [(`Z`, `cQ_Z_2`); (`X ++ Y`, `c_R___R__x3`)];
 3  output = (`((A ++ B) ** Z) ++ C`, `c_R___R__y3`);
 4  prov =
 5   Provnode ("plus",
 6    Provnode ("times",
 7     Provnode ("plus", Provleaf "&_R", Provleaf "&_R"),
 8     Provleaf "&_R"),
 9    Provleaf "&_R");
10  proc = (*...*);
11  actions =
12   [{Action.act = "WITH"; larg = "P"; lsel = "X"; rarg = "Q"; rsel = "Y";
13     res = "R"}];
14  copier = false;
15  intermediate = true}

The action used can be noticed in the actions field above and is as follows:

1{Action.act = "WITH"; larg = "P"; lsel = "X"; rarg = "Q"; rsel = "Y"; res = "R"}

It is worth noting the output type of the composite process, namely ((A ++ B) ** Z) ++ C. This is an optional output consisting of the outputs A ++ B and C of the two components, each of which may be produced depending on which process is executed at runtime.

Note, however, that the output A ++ B is paired with a new output Z. This corresponds to the second input Z of Q. This needs to still be an input in the composite process R because without it Q would not be able to execute. However, if P is executed then the input Z will not be used.

The rules of linear logic guarantee that unused resources are accounted for and do not just disappear. This leads to Z appearing as an output parallel to the output of P.

Merged inputs

A notable case is one where the two conditionally composed processes have common inputs. In that case, the common inputs merge into inputs of the composite process.

For example, both composed processes may have an input of type A each. This means both processes require a resource of type A in order to execute. No matter which of the 2 processes ends up executing in the conditional execution at runtime, the composite process will require an input of type A.

Therefore, the composite process will have a single A input. We call such an input a merged input. These are reported explicitly in the actionstate.

Sequential - JOIN

The JOIN action composes two processes sequentially.

More specifically, given a selected sub-term of the output of the first process and a matching input of the second process, their sequential composition yields a composite process where the resource corresponding to the selected sub-term is connected from the output of the first process to the output of the second.

Selector arguments

The first/left selector argument is used in the JOIN action to select the output sub-term of the first/left process.

This is specified as a path in the syntax tree of the process's output. It should follow the syntax of HOL Light's find_path function.

In short, the string lr means we should take the left path in the syntax tree, whereas the string r means we should take the right. An empty string indicates we should consider the type of the whole output.

For example, given an output A ** (B ++ C) we can select any sub-term as follows:

The second/right selector argument is used to select the input type of the second/right process that is expected to match our selected sub-term. This can help disambiguate between 2 inputs that are both able to receive the selected output type.

Example

As an example, the result R of the sequential composition of a process P with input X and output A ++ B and a process Q with inputs A and Y and output C is the following process:

 1{name = "R";
 2 inputs = [(`X`, `cP_X_1`); (`Y`, `cQ_Y_2`)];
 3 output = (`C ++ (Y ** B)`, `c_R___R__y3`);
 4 prov =
 5   Provnode ("plus", Provleaf "Q",
 6             Provnode ("times", Provleaf "Q:cQ_Y_2", Provleaf "P"));
 7 proc = (* ... *);
 8 actions =
 9   [{Action.act = "JOIN"; larg = "P"; lsel = "lr"; rarg = "Q"; rsel = "A"; res = "R"}];
10 copier = false;
11 intermediate = true}

The action used can be noticed in the actions field above and is as follows:

1{Action.act = "JOIN"; larg = "P"; lsel = "lr"; rarg = "Q"; rsel = "A"; res = "R"}

Notes

There are many different possible cases of interesting sequential compositions and edge cases. Depending on their types there may also be multiple ways that two specific processes can be composed together sequentially.

In our experience, it is not easy or practical for the user to control the sequential composition in such a fine grained way. Instead, the reasoner uses a set of heuristics to make its own decisions based on 2 key goals:

1. Connect the 2 processes maximally: The reasoner attempts to connect as many of the inputs resources of the receiving process as possible.
2. Minimize the execution steps in the final composition: The reasoner aims to make as few reasoning steps as possible, minimize the number of resources that are buffered (i.e. forwarded explicitly from one process to the next), and reduce repeating resources.

The first goal means that if the left process has output A ** B ** C and the right process has inputs B and C, then both of the two inputs will be connected to their respective parallel outputs irrespective of the user selection.

The second goal affects multiple decisions in the sequential composition.

One example is when the optional output of the left process is converted to an optional output with identical options, such as Y ++ Y. This might occur for example when a process that may fail to produce resource Y and throw an exception is composed with a contingency process that can recover from the exception and produce Y after all. The reasoner will attempt to collapse that output to a single Y output, whether that is the result of the original or of the contingency process. In fact, this will also reduce the reasoning steps and the size of the generated executable term, making it more efficient. It may also reduce the branching in subsequent compositions further down the line.

The tradeoff is that it is no longer possible to determine whether Y was produced from the original component or from the contingency process, which may be useful in some cases. The reasoner makes this decision under the assumption that if such differentiation is to be made between the produced Y resources, it should be reflected in the their respective types, instead of them having the same type Y.

Actionstate

Each composition action corresponds to a reasoning tactic implemented in HOL Light. These tactics require an extended proof state to function appropriately. This extension is captured using the Actionstate structure.

The final actionstate resulting from a composition proof is provided within the reasoner's response, so it may be useful to explain its structure briefly here.

The Actionstate structure is defined as follows:

 1module Actionstate = struct
 2  type t = {
 3      label : string;
 4      ctr : int;
 5      metas : term list;
 6      merged : (term * string * string) list;
 7      iprov : (term * provtree) list;
 8      prov : (string * provtree) list;
 9    }
10
11(* ... *)
12end;;

The fields can be described briefly as follows:

The unique name and counter are used to guarantee uniqueness of introduced channel names.

Merged inputs occur during conditional composition, when both processes have the same input type, so that the final composition does not duplicate inputs. Each entry consists of the input term as it appears in the composition paired with the names of the 2 input channels that got merged.