Tool Overview

The purpose of krill is to compute the footprint for the difference of two graphs. It takes as input semi-symbolic flow graphs, meaning that the nodes in the graph are fixed but the contents of those nodes and their edges are described by logic constraints.

krill comes with a benchmark suite that was extracted from the plankton tool, an experimental verifyer for lock-free set data structures. More specifically, we used plankton's benchmarks and recorded all the flow graphs for which it computes footprint during proof construction.

A discussion on how to reproduce our experiments follows. Therefore, we walk through the installation, compilation, and benchmarking.

Compilation and Installation

This section describes how to setup your system to repeat the benchmarks from the paper.

Download

The source code can be downloaded from GitHub:    GitHub release with tag TACAS23

Alternatively, you may wish to clone/download a potentially different version from GitHub:    GitHub repository

System Requirements

To compile this project you need CMake (>3.21), GCC and G++ (>10.0) or CLAN (>12.0), Java JRE (>1.6), and Z3 (v4.8.7). Compilation with CLAN (>12.0) is also possible. To run the benchmark suite, you also need Pyton 3 (>3.5), latex, and pgfplots.

Z3 Version

For reproducing the results, we recommend using Z3 version 4.8.7. Versions >4.8.7 generally fail to run z3::solver::consequences(). We do not expect this to influence the evaluation with krill, but it does affect plankton and the flow graph extraction. More specifically, if z3::solver::consequences() fails, plankton issues a warning and uses a backup procedure relying on z3::solver::check(). The backup procedure tremendously decreases performance, hence increases the runtime.

If you compile Z3 yourself, we highly recommend to use the same compiler (GCC/G++ vs CLANG) as for compiling this project.

Compilation

To build the project, do the following:

        cd path/to/krill
        mkdir build
        cd build
        CXX=/path/to/CXX-compiler cmake .. -DCMAKE_INSTALL_PREFIX=/path/to/installation
        CXX=/path/to/CXX-compiler make
        make install
			

This creates a folder /path/to/installation/krill at the specified location. This folder contains all binaries, scripts, and examples needed to reproduce the evaluation from the paper. Note that this includes binaries for both krill and plankton.

We recommend to use the -DCMAKE_INSTALL_PREFIX to specify a location where to install the tool. Omitting this flag will install the tool somewhere like /usr/local/. You can customize the folder that is appended to /path/to/installation by setting -DINSTALL_FOLDER appropriately in the cmake invocation.

You can omit setting the CXX environment variable to use your system's default compiler.

Troubleshooting

There are some known issues you might run into.

Issue: missing external dependencies

The project includes the code for AntLR, however, your system might miss some dependencies for it to build successfully. On Linux (tested with Ubuntu >18.04), make sure you have uuid, uuid-dev, and pkg-config installed.

Issue: timeout while cloning from GitHub

In some versions, the build process of AntLR fetches the library utfcpp from GitHub. In some (mainly academic) network setups this may fail and time out. The problem can be solved by forcing git to use https like so:

        git config --global url."https://".insteadOf git://
			

Issue: clang and libc++

When building with clang, you might run into problems compiling and linking AntLR. To solve this (tested with Ubuntu >18.04), install libc++-dev and libc++abi-dev. Then, create a compiler wrapper stdclang like so

        sudo touch /usr/bin/stdclang
        sudo chmod a+x /usr/bin/stdclang
			

Edit the created file /usr/bin/stdclang to contain this:

        #!/bin/bash
        clang++ -stdlib=libc++ $@
			

With this, use stdclang as the CXX compiler in the above build commands; it properly sets up clang++ to use libc++.

Docker

The repository comes with a Dockerfile that creates a Docker container with the necessary dependencies and an installation. To use it, you can something like this:

        cd path/to/krill
        docker build . -t krill
        docker run -it krill
			

Benchmarking

We describe how to repeat the benchmarks from the paper for computing footprints for the difference of two flow graphs. The flow graphs were extracted from plankton's proof generation for lock-free set data structures.

Benchmark Flow Graphs

We extracted flow graphs capturing the updates as encountered while verifying the following implementations:

• Fine-grained set HerlihyS08   Code   Flow Graph
• Lazy set HellerHLMSS05   Code   Flow Graph
• FEMRS tree (no maintenance) FeldmanEMRS18   Code   Flow Graph
• Vechev&Yahav's DCAS set VechevY08   Code   Flow Graph
• Vechev&Yahav's CAS set VechevY08   Code   Flow Graph
• ORVYY's set OHearnRVYY10   Code   Flow Graph
• Michael's set Michael02a   Code   Flow Graph
• Harris' set Harris01   Code   Flow Graph
• Michael's set (with wait-free search) Michael02a   Code   Flow Graph
• Harris' set (with wait-free search) Harris01   Code   Flow Graph

Running Benchmarks

To run the benchmarks go to the installation folder and execute the benchmark script like so:

        cd path/to/installation
        ./eval.sh
			

The eval.sh script runs each benchmark for 100 times. To modify the repetition count, just pass the desired count as an argument to the script, e.g., ./eval 77. You can customize the file the evaluation is written to doing this: ./eval.sh 77 path/to/file.

The eval.sh script produces a PDF eval.pdf containing the result of the evaluation, i.e., reproducing tables/charts like the ones from the paper.

Expected Benchmarks Results

We repeat our evaluation. We used an Apple M1 Pro with 16GB of RAM. We mark successful tasks with , failed tasks with , and timed out tasks with . The #FG refers to the number of flow graphs that a footprint is computed for. The speedup refers to the speedup of the new method compared to the naive method.

Generating Flow Graphs

The installation comes with the flow graphs that we extracted. If you want to re-extract them, you can do:

        ./mk_graphs.sh
			

This will run plankton on all the set data structures mentioned above and export the encountered flow graphs. Note that this will overwrite the existing files containing the flow graphs we extracted! Also note that this task is quite time consuming.

The krill Tool

Instead of using the benchmark script, you can directly interact with krill.

Basic Usage

You invoke krill like so:

        ./krill <path/to/flow_graph>
			

The flags and their arguments are listed in the following table (excerpt).

Besides the above, --version prints the tool's version, -h and --help print the full usage description.

Input Flow Graphs

The input format for flow graphs is shown on an example below. Input files may have arbitrarily many graphs. Flow graphs may have arbitrarily many nodes and constraints. Nodes may have arbitrarily many fields. For an exact specification of the input files, refer to the ANTLR parser definition  here.

        #name "Foobarium"

        struct Node { data_t val; Node * next; } 
        def @outflow[next](Node * node, data_t key) { node -> val < key } 
        
        @graph { 
            #name "example graph"
            @node[a1 : Node*] {
                @pre-unreachable; // optional
                @pre-emptyInflow; // optional
                @field val : data_t = d1 / d2;
                @field next : Node* = a2 / a2;
            }
            @constraint d1 >= MIN;
            @constraint d1 <= MAX;
            @constraint d2 >= MIN;
            @constraint d2 <= MAX;
            @constraint a1 != nullptr;
            @constraint a2 == nullptr;
        }
			

The plankton Tool

Instead of using the mk_graphs.sh script, you can directly interact with plankton, which is built/compiled as part of the krill project.

For more details, see the project page for plankton.

Basic Usage

You invoke plankton like so:

        ./plankton  [-f <path/to/graph>] [-p]  <path/to/program>
			

The flags and their arguments are listed in the following table (excerpt).

Besides the above, --version prints the tool's version, -h and --help print the full usage description.

Note that --loopNoPostJoin flag is required in order for the FEMRS tree to be verified successfully. The remaining benchmarks do not require the increased precision. The mk_graphs.sh script passes this flag automatically.

References