The artifacts represent evaluation results of real world networks having more than 40 nodes from Network Topology Zoo. The applied topologies are listed in following table, sorted in descending order by diameter (d) and nodal degree fluctuation (σ^2)).

    Topology
    |V|
    |E|

    σ^2
    d




    Chinanet
    42
    66
    1.5
    10.52
    4


    Litnet
    43
    43
    0.98
    5.04
    4


    Cernet
    41
    58
    1.32
    5.6 |
    5 |


    Ntt
    32
    65
    1.48
    7.07
    6


    Cesnet200706
    44
    51
    1.16
    6.27
    6


    Carnet
    44
    43
    0.98
    5.48
    6


    Dfn
    50
    78
    1.77
    5.31
    6


    Telcove
    71
    70
    1.59
    9.13
    7


    Forthnet
    62
    62
    1.41
    7.72
    7


    Bellsouth
    51
    66
    1.5 |
    7.55 |
    7 |


    Garr200902
    54
    68
    1.55
    5.13
    7


    Arnes
    41
    57
    1.3 |
    4.53 |
    7 |


    BeyondTheNetwork
    53
    65
    1.48
    3.98
    7


    Uunet
    49
    84
    1.91
    7.38
    8


    Tw
    71
    115
    2.61
    | 5.58
    | 8


    Uninett
    71
    97
    2.2
    3.12
    9


    Renater2010
    43
    56
    1.27
    3.08
    9


    Surfnet
    50
    68
    1.55
    3.36
    11


    Iris
    51
    64
    1.45
    2.16
    11


    Palmetto
    45
    64
    1.45
    2.57
    12


    BtLatinAmerica
    45
    50
    1.14
    1.87
    12


    Bellcanada
    48
    64
    1.45
    2.59
    13


    Sanet
    43
    45
    1.02
    1.66
    13


    LambdaNet
    42
    46
    1.05
    1.57
    13


    HiberniaGlobal
    55
    81
    1.84
    2.72
    16


    Ntelos
    47
    58
    1.32
    1.92
    17


    RedBestel
    84
    93
    2.11
    0.85
    28


    VtlWavenet2008
    88
    92
    2.09
    0.11
    31

The evaluation results consist of three major parts:

Raw Data: Configuration and results of all simulation experiments as CSV files.

Strategy Results: Visualization of the test results for each topology.

Best Strategies: Highlighting of the best strategies across all topologies.

Therein, the "Raw Data" comprise the configuration of or simulation experiments and the simulation results. Each line stands for a single simulation run.

"Strategy Results" and "Best Strategies" accompany the results presented in the paper. Result plots in the paper are excerpts from the plots in this repository. See below for further details.

Raw Data

Both, the configuration of a run and its results correspond to one line within a CSV file in subfolder ./raw. Each file comprises the results of a replication.

raw ├── results_0.csv ├── results_1.csv ├── ... └── results_9.csv

The raw data of a CSV file is structured as follows.

    Column
    Description




    topo
    Topology name.


    peers
    Number of nodes.


    edges
    Number of links.


    p_publishers
    Proportion of nodes acting as publisher (15% - 45%).


    p_subscriber
    Proportion of nodes acting as subscriber (15% - 45%).


    n_rules
    Number of allowed rules per switch.


    distances
    Flag for consideration of geographical distances (currently not used).


    strategy
    Applied virtual tree strategy.


    distribution
    Distribution method for client (uniform, distant, nearby)


    n_cluster
    Number of simulated clusters within the topology.


    p_change
    Churn rate of clients (0% - 100%).


    pub_change
    Flag for publisher migration (currently not used).


    tree_count
    Number of virtual trees installed in the network.


    selected_subscribers
    Avg. number of subscribers addressed by a publisher


    init_cost
    Avg. number of entries of a non-optimized distribution tree (per notification)


    trees
    Avg. proportion of tree entries per notification.


    stops
    Avg. proportion of stop entries per notification.


    hops
    Avg. proportion of hop entries per notification.


    final_cost
    Aggregated proportions (trees + stops + hops).


    datetime
    Timestamp of the simulation run.

Result Charts

The simulation results are visualized in plots.md or plots.html, ordered according above topology table.

Each topology accompanys following: - Topology figures with the computed Clusters therein. - Line charts outlining the behavior of the strategies over changing Number of Flow Rules. - Bar charts outlining the strategies' performance for different Migration Scenarios.

Details of the figures and diagrams are described next.

Clusters: Visualization of exemplary groups within the topology, computed by clusters and partitions strategy. The clusters strategy assigns 60% of a network's nodes to cluster groups; the partition strategy, in contrast, assigns all nodes to groups. Both strategies are described in Sec. III.

Number of Flow Rules: Results for varying number of rules (from 5 to 40) per switch, as described in Sec. IV. The charts are organized in a 3 x 3 matrix. A row of the matrix corresponds to different proportions of subscribers per publisher (15%, 30%, and 45%); a column corresponds to different distributions of clients (uniform, nearby and distant).

Migration Scenarios: Results for different migration scenarios with a fixed number of rules (40 rules per switch), as described in Sec. V. Each bar group stands for a strategy and reflects the results of different migration rates (0%, 30%, 50%, 70%, 100%).

Best Strategies

Scatter plots in subfolder ./fluctuation visualize the most efficient strategies for different migration scenarios by considering different proportions of subscribers per publisher (15%, 30%, and 45%). The plots show the results for a fixed number of subscribers (30% per publisher) and a churn rate of 100%. The strategies therein require the fewest labels in the header stack to encode a notification distribution tree, represented by the strategy's dot size

The demo data set consists the propagation path distances of AT & T North America Netowork Topology. The geographical node positions (latitude and longitude) along with the adjacency matrix has been found out from International Topology Zoo and the data set has been formed using the available data. This set has been used in Joint localization prolem of Controller and Hypervisor instances in vSDN enebled 5G Network.

This is the artefact for the paper "Automatic Synthesis of Transiently Correct Network Updates via Petri Games".

Requirements

The setup is build for running in an x86_64 architecture running Ubuntu 20.04 with python3 installed with the following pip3-package: networkx.

The original experiments were conducted on AMD EPYC 7551 processors with hyperthreading disabled and limited to 25 GB of memory.

Setup

To create the folder structure needed for running the experiments, please start by running mkdirs.sh.

The networkx library can be installed (in user space) by executing:

pip3 install --user networkx

All binaries are included and for repeatability we also include the source-code of the verifypn version used in these experiments. We use the following revision of the verifypn tool: https://bazaar.launchpad.net/~verifypn-cpn/verifypn/verifypn-games/revision/269

The source code of the revision 269 which is used for these experiments is located in the verifypn subfolder

Running experiments

All models come pre-build, the experiments can be executed sequentially by the following commands:

./solve_zoo.sh # experiments on the original, none-nested zoo-topologies ./solve_nested.sh # nested zoo topology experiments ./solve_synthetic.sh # experiments on synthetic networks

Memory, time and execution-environment can be set by setting the variables MEMORY, TIME and EXECUTOR variables in bash prior to execution.

For instance, to limit each single execution to 60 seconds, 500 MB of memory and run using sbatch the following can be used

export MEMORY=$((500*1024)) # memory in KB export TIME=60 # time in seconds export EXECUTOR=sbatch # to run on a slurm-enabled cluster ./solve_zoo.sh # experiments on the original, none-nested zoo-topologies ./solve_nested.sh # nested zoo topology experiments ./solve_synthethic.sh # experiments on synthetic networks

It will take more than 24 hours to complete the entire experimental setup with a one-hour timeout on a single core.

Data collection

After the execution, data can be collected using the ./extract_all.sh script which will generate .csv files for each subfigure of Figure 8 of the paper. The data reported in the .csv-files is in milliseconds for time and kilobytes for memory.

Notice that the data-folder is pre-populated with the results from the paper - these will be overwritten by a subsequent execution.

These .csv files can be turned into the graphs of the paper using the scripts provided in the plot-subfolder. From here, plots can be generated by running plot_all.sh for time-plots, or plot_all_mem.sh for memory-plots (not shown in paper). Notice that Figure 9 from the paper corresponds to (a): cactus-disjoint.pdf, (b) cactus-dependent_single.pdf, (c) cactus-dependen_10.pdf, (d) cactus-dependent_5.pdf, (e) shared-single.pdf and (f) cactus-nested.pdf. The remaining plots are from experiments not presented in the paper as they show similar trends to those incloded in the paper.

The raw results can be found in data/{synthethic,nested,zoo}_results and the corresponding strategy generated by verifypn can be found in data/{synthethic,nested,zoo}_strategy. The raw result output is postfixed with the engine generating the given result-file.

Notice that netsynth provides solutions directly in the output located in the data/{synthethic,nested,zoo}_results/*.netsynth files.

Lastly, consistency in the answers between netsynth and verifypn on the "nested" experiment can be checked by the consistent.sh script.

Modifying the experiments

Several parts of the experiments can be modified by changing the values of the generators. Notice that the artefact comes pre-loaded with a pre-generated set of models - so this step is optional.

The Generate_Synthetic.py facilitates the generation of all the synthetic models of the paper. This script will fill the data/synthethic_json folder.

The Generate_Nested.py constructs nested topologies from an existing set of .gml-files. Specifically it iterates through the contents of data/gml/ and randomly "subnets" networks into each other. The output is a new set of .gml files located in data/nested_gml/.

The Generate_Json.py reads the folders data/gml/ and data/nested_gml/ and creates (by random) a set of synthesis-problems based on the input topologies. By default the "source" and "target"-routes generated are appended up to n times to make harder instances. The value n ranges from 1-5.

Notice that Generate_Json.py can take more than a day to execute, given the rather brute-force nature of the optimization-problem solved for generating the random examples. The results of Generate_Json.py is placed in data/{zoo,nested}_json. Notice also that it is not guaranteed that a "sane" update synthesis problem is generated for all input .gml-files . To be a "sane" update synthesis problem, at least one waypoint must exist. Several attempts are made by the Generate_Json.py script to randomly generate such sane problems, however, this process can fail.

The last step is translation. The Translate.py script converts json-files into both .pnml-files for verifypn and .ltl-files for netsynth. The results are placed in the data/{synthethic,zoo,nested}_{ltl,pn}/ folders.