Abstract. We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages its memory. If the type check succeeds, it is safe to ignore the SMR algorithm and consider the program under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMR algorithm. There are two design decisions. The type system does not track any shape information, which makes it extremely lightweight. Instead, we rely on invariant annotations that postulate a protection by the SMR. To this end, we introduce angels, ghost variables with an angelic semantics. Moreover, the SMR algorithm is not hard-coded but a parameter of the type system definition. To achieve this, we rely on a recent specification language for SMR algorithms. Our second contribution is to automate the type inference and the invariant check. For the type inference, we show a quadratic-time algorithm. For the invariant check, we give a source-to-source translation that links our programs to off-the-shelf verification tools. It compiles away the angelic semantics. This allows us to infer appropriate annotations automatically in a guess-and-check manner. To demonstrate the effectiveness of our type-based verification approach, we check linearizability for various list and set implementations from the literature with both hazard pointers and epoch-based memory reclamation. For many of the examples, this is the first time they are verified automatically. For the ones where there is a competitor, we obtain a speed-up of up to two orders of magnitude.
CCS Concepts: • Theory of computation → Program verification; Type theory; Shared memory algorithms; Concurrent algorithms; Program analysis; Invariants; • Software and its engineering → Memory management; Model checking; Automated static analysis.
Additional Key Words and Phrases: lock-free data structures, safe memory reclamation, garbage collection, linearizability, verification, type systems, type inference
ACM Reference Format:
Roland Meyer and Sebastian Wolff. 2020. Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation. Proc. ACM Program. Lang. 4, POPL, Article 68 (January 2020), 36 pages. https://doi.org/10.1145/3371136
~/Desktop/pw.txt). The artifact is located at
~/popl20artifact/. The folder
~/popl20artifact/seal/contains an installation of our tool seal, the back-end verifier, and all examples.
cd ~/popl20artifact/seal/ && python3 benchmark.pyto run all benchmarks.
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:
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.
This section describes how to setup your system to repeat the benchmarks from the paper.
The source code can be downloaded from GitHub here:
GitHub release with tag
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).
To build the project, do the following:
cd path/to/Seal-POPL20 mkdir build cd build cmake .. -DCMAKE_INSTALLATION_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_INSTALLATION_PREFIX to specify a location where to install the tool.
Omitting this flag will install the tool somewhere like
You can omit the
-DCMAKE_CXX_COMPILER option to use your system's default compiler.
AntLR, however, your system might miss some dependencies for it to build successfully. On Linux (tested with Ubuntu 18.04), make sure you have
clangto build seal, you might run into problems compiling and linking
AntLR. To solve this (tested with Ubuntu 18.04), install
libc++abi-dev. Then, use the
clang++-libc++compiler wrapper, i.e., pass
cmake; it properly sets up
We describe how to repeat the benchmarks from the paper for verifying lock-free data structures relative to an SMR specification.
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:
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.
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
Our test script uses the timeout feature of the
subprocess library which is available only in version 3.5 and newer.
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
python3 benchmark.py <timeout_in_seconds>
The benchmark script will output a table with the following columns:
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 .
|Opt. Treiber's Stack||HP||0.5s||11s||1s|
|Vechev&Yahav's DCAS Set||EBR||0.8s||38s||200s|
|Vechev&Yahav's CAS Set||EBR||0.8s||7h||42m|
* False-positive due to imprecision in the back-end verifier.
Instead of using the benchmark script, you can directly interact with our tool seal.
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).
|Flag / Argument||Optional||Default||Description|
||no||—||Input program file to analyze. For examples, See Benchmark Programs|
||no||—||Input SMR automaton file for SMR specification. For examples, See SMR Specification|
||Performs type check.|
||Perform annotation check.|
||Perform linearizability check.|
||Simple type check. Turns of experimental rewriting&retrying (atomicity abstraction) upon type errors.|
||Lets the experimental rewriting&retrying check every annotation for validity before adding (deactivates heuristics).|
Besides the above,
--version prints the tool's version,
--help print the full usage description.
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.
The following table links the techniques presented in the paper to the implementation.
||Abstract syntax tree for programs. Supports a more powerful language than the one used in the paper.|
||Translates a given program into a simpler one following the command language given in the paper.|
|SMR automata (aka observers)||
||SMR automata/observer implementation. Like in the paper, the implementation assumes that non-specified transitions are intended to be self-loops.|
||Type implementation, storing the SMR automata locations that it represents as well as flags whether the type contains 𝔸, 𝕃, or 𝕊. The 𝔼 guarantees are implicit. Intuitively, our implementation computes the most precise 𝔼 on-the-fly.|
|Post Image on Observers||
Our implementation uses a symbolic observer.
It implements the cross-product on SMR automata, their completion wrt. to non-specified/implicit transitions, and uses more powerful formulas as transition guards that ordinary SMR automata from
|Type Transformer Relation||
||As described in the paper, relies on the post image for observers. Additionally, properly computes how 𝔸, 𝕃, and 𝕊 are maintained/lost/added.|
||Implements the type rules from the paper. In addition, performs on-the-fly loop-peeling for better convergence.|
Implements the source-to-source translation from the paper.
Here, however, we the destination program is one that can be fed to the
|Program Transformation (Annotations, Mover Types)||
||Based on failed type checks, uses heuristics to add annotations or apply mover types. If necessary, annotations are checked for correctness before being added. (For example, active annotations on shared variables are typically not checked.) Mover types are applied if no helpful annotation can be found. Then, a sequence is checked for right-moverness and if applicable moved into an atomic block.|