Artifacts for Reasoning About Recursive Tree Traversals

NOTE:

• Source code of Retreet is included in the docker image (as linked below) but not in this package. You can go to our github repo if you want to start from scratch.
• Content of this current package is also hosted in a github repo, you could do git clone from there to get this package as well

Getting Started

1. To get started, you will need to install docker on your system, and have xz ready for decompressing the image file (These are probably already in your system software repository, be sure to check that). Also you will need to have the artifact docker image file retreet.tar.xz, which is hosted here on Google drive. Please download it and put it in current directory.

   • Besides installing docker, you need to give your local user the permission to run docker command, or you will have to prefix sudo in every docker-related commands below
   • Alternatively you could manually build the image, see subsection Manually Building Image below for details

2. Use the import script to check file integrity of the image file and import it to your local docker system:

   ./import_image.sh

   The importing process should not take more than a few minutes.

3. The loaded image is named as yanjun1006/retreet, run it as

   docker run -it --name evaluation yanjun1006/retreet

   And then you are in the artifact image environment. Feel free to substitute evaluation with any other proper container name. You could peek around and do some evaluations, after you are done, just exit or Ctrl-D to quit. Next time when you want to start from where you left, just do

   docker start -ia evaluation

   • Optional: If you have abundant computing resources, i.e. running the image on a large server, since by default docker uses as much resource as its host may provide, you may want to limit resource uses of the running container. You can do this by supplying some extra options when executing docker run. For example to limit the container to use 40 cores and 128 GB memory:

     docker run -it --name evaluation --memory 128g --cpus 40 yanjun1006/retreet

     See Unsupported Claims section below for more details about the original experiment environment

4. Once you are in, we could do some basic testings to ensure everything works. For example we could use our test script to run Retreet to check the parallelizability (data-race-freeness) of size_counting traversals

   $ cd /home/user/Retreet
   $ python3 run_benchmarks.py -t parallel -c size_counting
   Checking parallelizability of fusible size_counting traversals.
   ANALYSIS
   Result: Parallelizable
   Total time: 00:00:00.01

   It should not take more than a few minutes to finish these. Once you see something like above, it's a good sign of docker image running well.

Manually Building Image

This section is the alternative manual setup descriptions, skip if you have downloaded the image.

1. Run the docker build script to build the docker image (make sure you are in this directory):

   docker build -t yanjun1006/retreet .

   It should take around 20-30 minutes to finish, depending on your network and computing performance.

2. Now the built image is in your local docker system, follow step 3, 4 in the Getting Started section above

File structure in artifact image

Under $/home/user/:

• MONA/ source repository for MONA
• Retreet/ source repository for Retreet
  • run_benchmarks.py test script
  • case_study/ directory of all case studies as mentioned in paper
    • size_counting/ Size counting
    • css/ CSS minification
    • cycletree/ Cycletree
    • shiftsum/ List sum and shift
  • output/ directory of generated MSO constraints that will be consumed by MONA

mona executable (Used for solving constraints generated by Retreet) is in /usr/local/bin

If you wish to run Retreet on any benchmark manually:

• Generate MSO constraints:
  • cd into Retreet/
    • cd /home/user/Retreet
  • Generate MSO constraints that check fusibility
    • exec.sh fuse <path to unfused traversals file> <path to fused traversal file> <path to file of relationship between unfused and fused traversals>
  • Generate MSO constraints that check parallelizability (data-race-freeness)
    • exec.sh fuse <path to unfused traversals file> <path to fused traversal file> <path to file of relationship between unfused and fused traversals>
• Run MONA on generated MSO constraints (usually located in $/home/user/Retreet/output)
  • mona <MSO constraint>

Evaluations

Test script

The main test facility would be the test script at $/home/user/Retreet/run_benchmarks.py, you could see its full help documentation by running $/home/user/Retreet/run_benchmarks.py --help:

Usage: run_benchmarks.py [options]

Options:
  -h, --help            show this help message and exit
  --runall              Run all experiments listed in Evaluation, default:
                        False
  -t TYPE, --type=TYPE  Type of trasformation to verify, specify 'fuse' for
                        fusion, specify 'parallel' for parallelization, if
                        omitted, all would be run
  -c CASE, --case=CASE  Case to verify, , could be repeated to specify
                        multiple, specify 'size_counting', 'css', 'cycletree'
                        or 'list' for fusibility verification, specify
                        'size_counting' or 'cycletree' for parallelizability
                        verification, if omitted, all would be run
  --retreet_entrypoint=RETREET
                        Entrypoint to Retreet run script, default:
                        /home/user/Retreet/exec.sh
  --mona_entrypoint=MONA
                        Entrypoint to MONA, default: /usr/local/bin/mona
  -B CASE_STUDY_BASE, --case_study_base=CASE_STUDY_BASE
                        Case study base directory path, default:
                        /home/user/Retreet/case_study/
  -O OUTPUT_BASE, --output_base=OUTPUT_BASE
                        Generated MONA files base directory path, default:
                        /home/user/Retreet/output/

Available transformations are fuse, parallel

Available case studies are size_counting, css, cycletree, list

Most of the flags are more configurable behavior and you could just use the default version.

For example, if you want to verify fusibility (fuse) of CSS minification (css) traversals:

$cd /home/user/Retreet
$python3 run_benchmarks.py -t fuse -c css

If you want to verify parallelizability (parallel) of size counting (size_counting) traversals:

$cd /home/user/Retreet
$python3 run_benchmarks.py -t parallel -c size_counting

NOTE:

• Make sure you are in /home/user/Retreet when running run_benchmarks.py
• Due to unknown bug in Docker image, there exist cases that nothing prints out when run Retreet on a benchmark for the first time. The issue should be gone after running the same comand again.

Steps to reproduce results in paper

1. Run Retreet on every benchmark

   $cd /home/user/Retreet
   $python3 run_benchmarks.py --runall

2. Inspect results in stdout

   Result: Fusible/Result: Parallelizable if the traverals are fusible/data-race-free.

   Checking fusibility of fusible size_counting traversals.
   ANALYSIS
   Result: Fusible
   Total time: 00:00:00.18
   

   An satisfying example will be given if the traverals are infusible or not data-race-free.

   Checking fusibility of infusible size_counting traversals.
   ANALYSIS
   Result: NOT Fusible
   Free variables are: x, y, Cmainx, C0x, C1x, C2x, C4x, C5x, C6x, C8x, C9x, C10x, Cmainy, C0y, C1y, C2y, C4y, C5y, C6y, C8y, C9y, C10y, Dmainx, D0x, D1x, D3x, D4x, D5x, D6x, Dmainy, D0y, D1y, D3y, D4y, D5y, D6y
   
   A counter-example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (11XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX,(),())
   Universe <dummy>:
   ()
   
   A satisfying example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (001100000000110000000011000001100000,(),(010000010000000001000100000010000101,(),(100000001010000000000000010010000000,(),())))
   Universe <dummy>:
   ()
   
   Total time: 00:00:00.18
   

   Running time is shown by Total time: .

Supported Claims

The results in paper can be reproduced by $ python3 run_benchmarks.py --runall. (See subsection Steps to reproduce results in paper above)

1. Fusibility and parallelizability of mutually recursive size-counting traversals

   • Retreet verifies the validity of fusing fusible size counting traversals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t fuse -c size_counting
   Checking fusibility of fusible size_counting traversals.
   ANALYSIS
   Result: Fusible
   Total time: 00:00:00.18
   

   • Retreet checks the validity of fusing infusible size counting traversals (The ouput below is generated along with the command above)

   Checking fusibility of infusible size_counting traversals.
   ANALYSIS
   Result: NOT Fusible
   Free variables are: x, y, Cmainx, C0x, C1x, C2x, C4x, C5x, C6x, C8x, C9x, C10x, Cmainy, C0y, C1y, C2y, C4y, C5y, C6y, C8y, C9y, C10y, Dmainx, D0x, D1x, D3x, D4x, D5x, D6x, Dmainy, D0y, D1y, D3y, D4y, D5y, D6y
   
   A counter-example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (11XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX,(),())
   Universe <dummy>:
   ()
   
   A satisfying example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (001100000000110000000011000001100000,(),(010000010000000001000100000010000101,(),(100000001010000000000000010010000000,(),())))
   Universe <dummy>:
   ()
   
   Total time: 00:00:00.18
   

   • Retreet verifies the validity of parallelizing size counting traverals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t parallel -c size_counting
   Checking parallelizability of fusible size_counting traversals.
   ANALYSIS
   Result: Parallelizable
   Total time: 00:00:00.01
   

2. Fusibility of CSS minification traversals

   • Retreet verifies the validity of fusing CSS minification traversals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t fuse -c css
   Checking fusibility of fusible CSS minification traversals.
   ANALYSIS
   Result: Fusible
   Total time: 00:00:08.50
   

3. Fusibility and parallelizability of cycletree routing traversals

   • Retreet verifies the validity of fusing cycletree routing traversals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t fuse -c cycletree
   Checking fusibility of fusible cycletree traversals.
   Problem broken down into 5 MONA queries.
   ANALYSIS
   Result: Fusible
   Total time: 00:00:12.97
   
   ANALYSIS
   Result: Fusible
   Total time: 00:04:10.71
   
   ANALYSIS
   Result: Fusible
   Total time: 00:02:43.96
   
   ANALYSIS
   Result: Fusible
   Total time: 00:02:09.89
   
   ANALYSIS
   Result: Fusible
   Total time: 00:00:33.62
   

   • Retreet verifies the validity of parallelizing cycletree routing traverals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t parallel -c cycletree
   Checking parallelizability of fusible cycletree traversals.
   ANALYSIS
   Result: NOT Parallelizable
   Free variables are: x, y, C3x, C4x, C5x, C7x, C8x, C9x, C11x, C12x, C13x, C15x, C16x, C17x, C0x, D19y, D20y, D21y, D1y
   
   A counter-example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (1100000000000XXXXXX,(),())
   Universe <dummy>:
   ()
   
   A satisfying example is:
   Booleans:
   XXXXXXXXXXXXXXXXXXX
   Universe <univ>:
   (111000000000001XX11,(),())
   Universe <dummy>:
   ()
   
   Total time: 00:00:01.17
   

4. Fusibility of List Sum and Shift

   • Retreet verifies the validity of fusing list Shift and Sum traversals

   $cd /home/user/Retreet
   $python3 run_benchmarks.py -t fuse -c list
   Checking fusibility of fusible list_sum and list_shift traversals.
   ANALYSIS
   Result: Fusible
   Total time: 00:00:00.02
   

Unsupported Claims

• The experiments reported in the paper were originally conducted on a server with a 40-core, 2.2GHz CPU and 128GB memory, which may have far more computing resources then most artifact evaluation environments, the absolute performance (e.g. running time) may be very different. Under the same environment as the one used in paper, python3 run_benchmarks.py --runall should finish in around 10 minutes. For your reference, we list the running time we report in the paper here:
  • Size-counting traversals
    • 0.14s (fusible)
    • 0.14s (infusible)
    • 0.02s (parallelizable)
  • CSS minification traversals
    • 6.88s (fusible)
  • Cycletree routing traversals
    • 490.55s (fusible)
    • 0.95s (not parallelizable)
  • List sum and shift traversals
    • 0.11s (fusible)
• Running Retreet on cycletree consumes extremely large amount of memory, it is very likely that running this experiment will run into Out of memory error, if the artifact evaluation environment does not have sufficient memory (e.g. memory less than 128GB). For your reference, this artifact was also tested on a machine with a dual-core, 2.9GHz CPU and 8GB memory and also a machine with a dual-core, 1.6GHz CPU and 16GB memory. It ran into Out of memory error on verification of cycletree traversals, but worked fine on other benchmarks.
• As the bisimulation checking step was done by hand (as we mentioned in the paper page 8 line 860-861), we manually listed the fused traversals checked by us in the artifact. Hence, this artifact is only about verification.
• For reference, we have included our original results below, see section Reference stdout below.

Reference stdout

$cd /home/user/Retreet
$python3 run_benchmarks.py --runall
Checking fusibility of fusible size_counting traversals.
ANALYSIS
Result: Fusible
Total time: 00:00:00.18

Checking fusibility of infusible size_counting traversals.
ANALYSIS
Result: NOT Fusible
Free variables are: x, y, Cmainx, C0x, C1x, C2x, C4x, C5x, C6x, C8x, C9x, C10x, Cmainy, C0y, C1y, C2y, C4y, C5y, C6y, C8y, C9y, C10y, Dmainx, D0x, D1x, D3x, D4x, D5x, D6x, Dmainy, D0y, D1y, D3y, D4y, D5y, D6y

A counter-example is:
Booleans:
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Universe <univ>:
(11XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX,(),())
Universe <dummy>:
()

A satisfying example is:
Booleans:
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Universe <univ>:
(001100000000110000000011000001100000,(),(010000010000000001000100000010000101,(),(100000001010000000000000010010000000,(),())))
Universe <dummy>:
()

Total time: 00:00:00.18

Checking fusibility of fusible CSS minification traversals.
ANALYSIS
Result: Fusible
Total time: 00:00:08.50

Checking fusibility of fusible cycletree traversals.
Problem broken down into 5 MONA queries.
ANALYSIS
Result: Fusible
Total time: 00:00:12.97

ANALYSIS
Result: Fusible
Total time: 00:04:10.71

ANALYSIS
Result: Fusible
Total time: 00:02:43.96

ANALYSIS
Result: Fusible
Total time: 00:02:09.89

ANALYSIS
Result: Fusible
Total time: 00:00:33.62

Checking fusibility of fusible list_sum and list_shift traversals.
ANALYSIS
Result: Fusible
Total time: 00:00:00.02

Checking parallelizability of fusible size_counting traversals.
ANALYSIS
Result: Parallelizable
Total time: 00:00:00.01

Checking parallelizability of fusible cycletree traversals.
ANALYSIS
Result: NOT Parallelizable
Free variables are: x, y, C3x, C4x, C5x, C7x, C8x, C9x, C11x, C12x, C13x, C15x, C16x, C17x, C0x, D19y, D20y, D21y, D1y

A counter-example is:
Booleans:
XXXXXXXXXXXXXXXXXXX
Universe <univ>:
(1100000000000XXXXXX,(),())
Universe <dummy>:
()

A satisfying example is:
Booleans:
XXXXXXXXXXXXXXXXXXX
Universe <univ>:
(111000000000001XX11,(),())
Universe <dummy>:
()

Total time: 00:00:01.17