Subset Projection in Asynchronous Multiparty Session Types

This prototype implements the sound and complete subset projection operator for asynchronous Multiparty Session Types. Notably, it uses a global message causality analysis to ensure correctness of projections. In addition, the functionality of the incomplete generalized projection operator, also called classical projection operator, is implemented.

Corresponding Publication

This work is part of the paper "Complete Multiparty Session Type Projection with Automata", published at CAV 2023. To use the same version of the tool that was used for producing the results reported in the paper, please refer to the cav_23 tag.

Contact

• Felix Stutz (fstutz@mpi-sws.org)

Structure and Content

This repository contains (among others) the following folders:

• main.py is the entry point to our tool and provides a command line interface with several options (see Section "Command Line Interface")
• datatypes with basic data types for global and local types as well as finite state machine representations of those; these contain the main functionality of both approaches
• evaluation_data stores the raw data for the evaluation
• evaluation_functionality provides the scripts and functionality to run the evaluation and process the resulting data; all parameters for the evaluation can be set in evaluation_config.py
• evaluation_results is an (initially empty) folder where the results of the evaluation is stored
• global_types comprise of the global types used in our evaluation, represented
• parsing implements the parsing functionality to parse global types given as specified by the grammar GlobalType.g4

Command Line Interface

Running python3 main.py --help gives detailed information about how to use the command line interface:

usage: main.py [-h] [--option O] [--global_type FILE] [--no_output] 
               [--num_runs N] [--size S] [--save_to FILE] [--overwrite]

optional arguments:
  -h, --help          show this help message and exit
  --option O          specifies which experiment should be run: 
                      'subset_project' takes a global type and attempts to produce local FSMs 
                            using subset projection; 
                      'classical_project' takes a global type and attempts to produce local FSMs 
                            using classical projection; 
                      'projectability_subset' (default) computes a table of 
                            individual projection times using subset projection; 
                      'projectability_classical' computes a table of 
                            individual projection times using classical projection;
                      'state_explosion' computes a graph that demonstrates how the number of states 
                            evolve with increasing global type size; 
  --global_type FILE  to provide the global type to project and, thus, only applies to ''subset_*'
  --no_output         do not show results
  --num_runs N        specifies the number of runs for all but state_explosion (for which it is 1); 
                            range: 1-1000; default of 10 applied if out of range or not given; 
                            does not apply to 'state_explosion' (no times reported)
  --size S            specifies the size up to which the parameterized experiments should run
  --save_to FILE      store output in file or files with this prefix if multiple 
                            (relative to where the script is called from)
  --overwrite         overwrites file if provided

The option --option specifies which experiment will be run:

1. subset_project: a global type (given via --global_type) is projected using subset projection and the local specifications are output if they exist
2. classical_project: a global type (given via --global_type) is projected using classical projection and the local specifications are output if they exist
3. projectability_subset: this produces runs the subset projection on a number of examples and produces a table as results
4. projectability_classical: this produces runs the classical projection on a number of examples and produces a table as results
5. state_explosion: this option generates the subset projections to show-case the exponential blow-up in state space when generating an implementation

Note that, in general, the tool outputs its result on stdout, which can be suppressed using --no_output. To allow overwriting existing results files, use the option --overwrite.

Reproducing the Evaluation Results

We provide a docker image to facilitate easy reproducability of the results reported in the paper.

How to Setup and Run the Docker Image

First load the docker image docker-tool-cav from the tar-files:

docker load < docker-tool-cav.tar

Create a directory on your machine that should be used to hold the outputs of the experiments. This directory will be mapped to the results directory in the docker container. In the following, we refer to the absolute path to this directory as /absolute/path/to/local/result/directory.

Run the docker image in interactive mode, providing the absolute path to the local results directory. (This may require sudo.)

docker run -v /absolute/path/to/local/result/directory:/tool-cav/evaluation_results 
           -it docker-tool-cav bash

This opens a shell that allows you to run the experiments and inspect the code. In order to modify the code or configuration, we suggest to use a similar mapping of a local directory via the -v flag, but for the directory tool-cav in the docker container.

To run the experiments, first change to the directory of the tool:

cd tool-cav/

Finally, run the evaluation script:

./evaluation_functionality/script_evaluation.sh 

The script will run three experiments. The script will indicate which experiment is currently running:

1) Computing results for subset projection.
2) Computing results for classical projection.
3) Computing results for state space explosion analysis.

If all experiments were run successfully, the script will print:

Computing requested results was successful.

Resource Requirements and Expected Run Time

Using the provided docker image, 4GB RAM should be sufficient to run the evaluation. We expect that the experiments take at most 15 minutes to complete.

For the results reported in the paper, we ran the experiments without using a docker container on a laptop with a 11th Gen Intel® Core™ i7-1165G7 2.80GHz and 32GB RAM. The computation was not parallelized and the maximal RAM usage was less than 500MB. The run time was less than 6 minutes.

How to Inspect the Results

The results of the experiments can be found in evaluation_results. This directory is mapped to the local results directory outside the docker image as indicated earlier. (The intermediate results of the evaluation can be found in evaluation_data for inspection.)

The files table_projection_subset.txt and table_projection_classical.txt contain the results of the first two experiments, which project various global types using the respective projection operator. Combined, these files provide the data for Table 1 in the paper.

For both projection operators, we provide the expected result of the projection (in EvalSubsetProjection.py and EvalClassicalProjection.py) and check against this, as indicated by the last line in each table.

If the projection operator is not defined for a given global type, then this is indicated by reporting the value -1 in the "Size Proj's" column.

Note that reported sizes of the global types may differ between the tables for the two projection operators. This is because the size is computed slightly differently for each projection operator. For the classical projection, the size is computed purely syntactically, accounting for identical subterms multiple times. For the subset projection, however, we consider the size of the resulting global finite state machine (i.e., the sum of the number of states and the number of transitions). This measure does not repeatedly count identical subterms.

The file plot_state_space_explosion.pdf provides the output of the third experiment. It consists of a plot as shown in Figure 4 of the paper. The sizes reported in the plot are determined using the finite state machines obtained by projecting a family of global types G_n. While Figure 4 in the paper reports results for all n < 20, the default configuration only considers values n < 17. This is to speed up the run time of Experiment 3, while still showing the state space explosion. The maximal value of n for this experiment can be configured in evaluation_config.py.