Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

This web page accompanies our VMCAI 2016 submissions Pointer Race Freedom. Here you can

Prototype

Our prototype is written in C++. All its components are implemented from scratch.

We integrated the following techniques following the approach from An Integrated Specification and Verification Technique for Highly Concurrent Data Structures:

In addition to an analysis for explicit memory management and garbage collection, we integrated our new ownership-respecting memory semantics. It allows for a faster analysis as we can rely on certain ownership guarantees — making thread-modular reasoning for single threads practical.

The source code can be downloaded here.

Experimental Results

For experiments we used an Intel Xeon E5-2650 v3 running at 2.3 GHz and tested our tool on the following data structure implementations:

The results are listed in the table below. The experiments were conducted on an Intel Xeon E5-2650 v3 running at 2.3 GHz. The table includes the following:

For a comparison, we also include the results with the ownership-based optimization turned off (suffix -). Note: this optimization does not apply to the memory-managed semantics.

Our experiments confirm the usefulness of pointer race freedom. When equipped with pruning (OWN), the ownership-respecting semantics provides a speed-up of two orders of magnitude for Treiber's stack and the single lock data structures compared to the memory-managed semantics (MM-). The size of the explored state space is close to the one for the garbage-collected semantics (GC) and up to two orders of magnitude smaller than the one for explicit memory management.

For Michael&Scott's queue we had to provide hints in order to eliminate certain patterns of false positives. This is due to an imprecision that results from joins over a large number of states (we are using a joined representation of states based on Cartesian abstraction). Those hints are sufficient for the analysis relying on the ownership-respecting semantics to establish correctness. The memory-managed semantics produces more false positives, the elimination of which would require more hinting.

In addition to the above test we also stress tested our tool by purposely inserting pointer races, for example, by discarding the version counters. In all cases, the tool was able to detect those races. The results of those test can be found in the table below.

For the stress tests note the following: