CDSSpec – Programming Languages Research Group

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.

Getting Started

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 :

     cd model-checker      make

Get the benchmarks (not required; distributed separately), placing them as a subdirectory under the model-checker directory:

     git clone -b ppopp17-artifact git://plrg.eecs.uci.edu/model-checker-benchmarks.git benchmarks

Compile the CDSSpec compiler:

     cd cdsspec-compiler       ./run-javacc.sh       ant compile       ./generate.sh

Compile the instrumented benchmarks (the “generate.sh” file will generate instrumented files to the “test-cdsspec” directory). Use the following command:

     cd ../test-cdsspec       make

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

Notice

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/?p=model-checker.git;a=summary.

Disclaimer

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.

Contact

Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.

Contact Peizhao Ou at peizhaoo@uci.edu or Brian Demsky at bdemsky@uci.edu for questions about CDSSpec.

Copyright

CDSChecker is distributed under the GPL v2. See the LICENSE file for details.

Acknowledgments

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.