POPL'20 Project Page

Institute of Theoretical Computer Science

Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation

Roland Meyer and Sebastian Wolff, TU Braunschweig, Germany

Presented at POPL'20.

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

Quick Start
  1. Download the Virtual Machine Snapshot (created with Virtual Box, credentials in ~/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.
    See Compilation and Installation
  2. Fire up the Virtual Machine.
  3. Open a Shell and simply execute cd ~/popl20artifact/seal/ && python3 benchmark.py to run all benchmarks.
    See Benchmarking
  4. Presto!

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:

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_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 /usr/local/. You can omit the -DCMAKE_CXX_COMPILER option 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: 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_INSTALLATION_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:

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 .

Program SMR Types Annotations Linearizability
Treiber's Stack EBR 0.6s 10s 1s
HP 0.7s 12s 1s
Opt. Treiber's Stack HP 0.5s 11s 1s
Michael&Scott's Queue EBR 0.7s 16s 5s
HP 0.6s 12s 4s
DGLM Queue EBR 0.7s 1s* 6s
HP 0.6s 1s* 5s
Vechev&Yahav's DCAS Set EBR 0.8s 38s 200s
HP 1.2s 13s 98s
Vechev&Yahav's CAS Set EBR 0.8s 7h 42m
HP 1.2s 3.5h 42m
ORVYY Set EBR 0.8s 7h 47m
HP 1.2s 3.2h 47m
Michael's Set EBR 0.2s 22s* t/o
HP 1.2s 90s* t/o

* 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).

Flag / Argument Optional Default Description
<path_to_program> no Input program file to analyze. For examples, See Benchmark Programs
<path_to_smr> no Input SMR automaton file for SMR specification. For examples, See SMR Specification
--checktypes
-t
yes true Performs type check.
--checkannotations
-a
yes true Perform annotation check.
--checklinearizability
-l
yes true Perform linearizability check.
--simple
-s
yes false Simple type check. Turns of experimental rewriting&retrying (atomicity abstraction) upon type errors.
--eager
-e
yes false Lets the experimental rewriting&retrying check every annotation for validity before adding (deactivates heuristics).

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.

Paper Implementation Description
Programs src/cola/ast.hpp Abstract syntax tree for programs. Supports a more powerful language than the one used in the paper.
Program Simplification src/types/preprocess.hpp
src/types/preprocess.cpp
Translates a given program into a simpler one following the command language given in the paper.
SMR automata (aka observers) src/cola/observer.hpp SMR automata/observer implementation. Like in the paper, the implementation assumes that non-specified transitions are intended to be self-loops.
Types src/types/types.hpp
src/types/types.cpp
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 src/types/sobserver.hpp
src/types/sobserver.cpp
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 src/cola/observer.hpp. For computing the post image, we use Z3 to check the satisfiability of guards.
Type Transformer Relation src/types/types.hpp
src/types/types.cpp
As described in the paper, relies on the post image for observers. Additionally, properly computes how 𝔸, 𝕃, and 𝕊 are maintained/lost/added.
Type Check src/types/checker.hpp
src/types/checker_check.cpp
Implements the type rules from the paper. In addition, performs on-the-fly loop-peeling for better convergence.
Invariant Check src/types/cave.hpp
src/types/cave.cpp
Implements the source-to-source translation from the paper. Here, however, we the destination program is one that can be fed to the CAVE tool (differs slightly from src/cola/ast.hpp).
Linearizability Check src/types/cave.hpp
src/types/cave.cpp
Uses CAVE to check for linearizability. This step requires to translate a program into one that can be fed to CAVE.
Program Transformation (Annotations, Mover Types) src/types/rmraces.hpp
src/types/rmraces.cpp
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.

References

DohertyGLM04 Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. 2004. Formal Verification of a Practical Lock-Free Queue Algorithm. In FORTE (LNCS), Vol. 3235. Springer, 97–114. https://doi.org/10.1007/978-3-540-30232-2_7
Fraser04 Keir Fraser. 2004. Practical Lock-Freedom. Ph.D. Dissertation. University of Cambridge, UK. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.599193
Lipton75 Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. CACM 18, 12 (1975), 717–721. https://doi.org/10.1145/361227.361234
McKenneyS98 Paul E. McKenney and John D. Slingwine. 1998. Read-copy Update: Using Execution History to Solve Concurrency Problems. In Parallel and Distributed Computing and Systems. http://www.rdrop.com/users/paulmck/RCU/rclockjrnl_tpds_mathtype.pdf
MeyerW19 Roland Meyer and Sebastian Wolff. 2019. Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3, POPL (2019), 58:1–58:31. https://doi.org/10.1145/3290371
Michael02a Maged M. Michael. 2002. High performance dynamic lock-free hash tables and list-based sets. In SPAA. 73–82. https://doi.org/10.1145/564870.564881
Michael02b Maged M. Michael. 2002. Safe memory reclamation for dynamic lock-free objects using atomic reads and writes. In PODC. ACM, 21–30. https://doi.org/10.1145/571825.571829
MichaelS96 Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC. ACM, 267–275. https://doi.org/10.1145/248052.248106
OHearnRVYY10 Peter W. O’Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010. Verifying linearizability with hindsight. In PODC. ACM, 85–94. https://doi.org/10.1145/1835698.1835722
Treiber86 R. Kent Treiber. 1986. Systems programming: coping with parallelism. Technical Report RJ 5118. IBM. https://domino.research.ibm.com/library/cyberdig.nsf/0/58319a2ed2b1078985257003004617ef?OpenDocument
Vafeiadis09 Viktor Vafeiadis. 2009. Shape-Value Abstraction for Verifying Linearizability. In VMCAI (LNCS), Vol. 5403. Springer, 335–348. https://doi.org/10.1007/978- 3- 540- 93900- 9_27
Vafeiadis10a Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In CAV (LNCS), Vol. 6174. Springer, 450–464. https://doi.org/10.1007/978-3-642-14295-6_40
Vafeiadis10b Viktor Vafeiadis. 2010. RGSep Action Inference. In VMCAI (LNCS), Vol. 5944. Springer, 345–361. https://doi.org/10.1007/978-3-642-11319-2_25
VechevY08 Martin T. Vechev and Eran Yahav. 2008. Deriving linearizable fine-grained concurrent objects. In PLDI. ACM, 125–135. https://doi.org/10.1145/1375581.1375598