CDSSpec: Checking Concurrent Data Structures Under the C/C++11 Memory Model
While using the low-level relaxed atomics introduced by the C/C++11 memory model can improve the performance of concurrent data structures, it introduces non-intuitive behaviors that makes testing and reasoning concurrent data structures hard. One observation is that the classic and intuitive correctness criteria for concurrent data structures — linearizability — cannot be directly applied to C/C++11 concurrent data structures. Thus, in order to help developers find bugs and improve code quality, we design and implement the CDSSpec specification checker framework. The CDSSpec checker allows developers to specify lock-based and lock-free concurrent data structures under the C/C++11 memory models and check their implementations against the specifications.
The CDSSpec specification has the following advantages: (1) it is based on the intuition of mapping concurrent executions to executions on equivalent sequential data structures; and (2) like linearizability, the CDSSpec specification is composable, which is a very important property for building modular systems. More details can be found in this paper.
- Get the source of the CDSSpec checker (along with the specification compiler). We implemented the CDSSpec checker as a backend analysis of the CDSChecker model checker. If you haven’t done so already, you may download the CDSSpec checker using git:
git clone -b ppopp17-artifact git://plrg.eecs.uci.edu/model-checker.git model-checker
- Compile CDSChecker with the CDSSpec backend analysis :
- Get the benchmarks (not required; distributed separately), placing them as a subdirectory under the
git clone -b ppopp17-artifact git://plrg.eecs.uci.edu/model-checker-benchmarks.git benchmarks
- Compile the CDSSpec compiler:
- Compile the instrumented benchmarks (the “generate.sh” file will generate instrumented files to the “test-cdsspec” directory). Use the following command:
- Note that each instrumented benchmark will be generated in the “test-cdsspec/” directory. For example, the instrumented ms-queue benchmark will be placed in the test-cdsspec/ms-queue directory. With those compiled benchmarks, you are ready to run the instrumented benchmark. About how to run an instrumented benchmark, PLEASE see the CDSChecker page (you only need to run with the additional “-tSPEC” command). An example command is shown below:
./run.sh mcs-lock/main -m2 -y -tSPEC
A bug of CDSChecker when running under Ubuntu 16.04 was reported and fixed. If you are running our tool under Ubuntu 16.04, keep in mind that you will need the latest version of CDSChecker at http://plrg.eecs.uci.edu/git/model-checker.git/.
The CDSSpec checker, the CDSSpec compiler source and the accompanying benchmarks source on Gitweb:
The CDSChecker model checker page for more optional information.
The AutoMO tool page for more optional information about the known bugs in our benchmarks,.
We make no warranties that the output of CDSSpec is free of errors. You are responsible for assuring the correctness of your software. See the GPL2 license for further disclaimers.
Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.
Copyright © 2013 Regents of the University of California. All rights reserved.
CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
This material is based upon work supported by the National Science Foundation under Grant Nos CCF-0846195, CCF-1217854, CNS-1228995, and CCF-1319786.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.