Tool Overview

Our paper presents an analysis for verifying lock-free data structures that use safe memory reclamation (SMR) algorithms. We follow a compositional approach which factors out the verification of the SMR implementation MeyerW19. That is, we work with a specification of the SMR algorithm rather than its implementation. The SMR specification is given in form of an SMR automaton (also called observer). This automaton is a parameter in our theory/tool (not hard-coded). To verify the data structure wrt. the SMR specification, we perform a type check. A successful typing implies that the data structure is memory safe. As a consequence, our theory allows to perform the actual verification task under garbage collection (GC) semantics—that is, we can ignore the memory management for the verification task. A major design decision in our type system is the fact that we do not track shape information. Instead, we rely on simple, light-weight annotations in the program. As we show, these annotations can be discharged under GC as well. Altogether, this means that the entire verification can soundly be conducted with an off-the-shelf GC verifier.

We implemented the proposed analysis in our tool seal. As such, it performs the following tasks:

• a type check to decide whether or not the data structure properly manages its memory (a successful type check implies memory safety),
• a check to prove correct the invariant annotations in the input program (which may be needed for a successful type check), and
• a linearizability check of the data structure.

The novelty of our approach lies in the ability to perform the last two tasks under garbage collection, using an off-the-shelf verifier. For our tool we use Vafeiadis' CAVE Vafeiadis09, Vafeiadis10a, Vafeiadis10b as a back-end solver. To help the type check go through, our tool comes with an experimental rewrite engine to automatically add invariant annotations and apply Lipton's Lipton75 mover types.

In the this page we discuss how to reproduce our experiments. Therefore, we walk through the installation, compilation, and benchmarking. In the end, we briefly link the concepts and techniques from the paper to our implementation.

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 here:    GitHub release with tag POPL20

System Requirements

To compile this project you need CMake (>3.5), a C++17 compatible compiler, Java JRE (>1.6), OCaml, and Z3 (v4.8.5). Compilation was tested with Apple LLVM v.9.1.0, Apple LLVM v.10.0.1, and Clang v.8.0. To run the benchmarking script, you need Pyton 3 (>3.5).

Compilation

To build the project, do the following:

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

This creates a folder /path/to/installation/seal at the specified location. This folder contains all binaries, scripts, and examples needed to reproduce the evaluation from the paper.

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 omit the -DCMAKE_CXX_COMPILER option to use your system's default compiler.

Troubleshooting

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: clang and libc++ on Linux

When using clang to build seal, 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, use the clang++-libc++ compiler wrapper, i.e., pass -DCMAKE_INSTALL_PREFIX=clang++-libc++ to cmake; it properly sets up clang++ to use libc++.

Benchmarking

We describe how to repeat the benchmarks from the paper for verifying lock-free data structures relative to an SMR specification.

SMR Specifications

seal comes packaged with an SMR automata for Epoch-Based Reclamation (EBR) Fraser04, McKenneyS98 and Hazard Pointers (HP) Michael02b The HP specification assumes two hazard pointers per thread. The SMR automata can be found here:

• EBR: examples/ebr.smr (human readable .pdf)
• HP: examples/hp.smr (human readable .pdf)

Benchmark Programs

We evaluated our tool on Treiber's Stack Treiber86, Michael02b, Michael&Scott's Queue MichaelS96, Michael02b, the DGLM queue DohertyGLM04, Vechev&Yahav's DCAS Set VechevY08, Vechev&Yahav's CAS Set VechevY08, the ORVYY Set OHearnRVYY10, and Michael's Set Michael02a using Hazard Pointers and Epoch-Based Reclamation.

For our experiments, we transformed the programs in order for the type check to go through. To that end, we added annotations and applied Lipton's mover types. For the code consider the following list.

Running Benchmarks

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

        cd path/to/installation
        python3 benchmark.py
			

Make sure to use python3. Our test script uses the timeout feature of the subprocess library which is available only in version 3.5 and newer.

The benchmark.py script runs every task (type check, annotation check, linearizability check) for every example program with a default timeout of 12 hours. You can modify the timeout in seconds by passing an optional argument to benchmark.py:

        python3 benchmark.py <timeout_in_seconds>
			

The benchmark script will output a table with the following columns:

1. Program: the name of the example program,
2. Types: time in seconds to perform a type check (with automatically generated types),
3. Annotations: time in seconds to perform an annotation check with our back-end solver CAVE, and
4. Linearizability: time in seconds to perform a linearizability check with our back-end solver CAVE.

Expected Benchmarks Results

We repeat our evaluation. We used an Intel i5-8600K@3.6GHz machine with 16GB of RAM running MAC OS 10.12. The timeout was set to 12h. We mark successful tasks with , failed tasks with , and timed out tasks with .

^* False-positive due to imprecision in the back-end verifier.

The seal Tool

Instead of using the benchmark script, you can directly interact with our tool seal.

Basic Usage

You invoke seal like so:

        ./seal  [-t] [-l] [-a] [-s] [-e]  <path_to_program> <path_to_smr>
			

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.

Experimental Rewrite Engine

Our tool comes with an experimental rewrite engine for hazard pointers that fully automatically applies moverness arguments and inserts active annotations upon a failed type check. This rewrite engine is turned on by default (turned off by the -e eager flag).

For an example, one can execute seal on Micheal&Scott's non-preprocessed queue (Michael&Scott's Queue):

        cd path/to/seal
        ./seal -t examples/HP/MichaelScottQueue.cola examples/hp.smr
			

Doing so, seal will start with the type check and soon report on a failure due using a potentially invalid pointer. It will then attempt to fix the issue based on integrated heuristics and repeat the type check. The output will give insights on the exact failure during the type check and the fix that is applied. Note that fixing an issue may take some time as seal may invoke the back-end solver to test if an annotation can be added.

At the end, seal outputs the rewritten program and the number of rewrites performed. For Michael&Scott's queue, 12 rewrites are necessary.

Notes on the Implementation

The following table links the techniques presented in the paper to the implementation.

References