X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=README.md;h=73173c737c5ed9a6dded95c7fabfc2b9023d7b4b;hp=ea3b2423753bf3698ca3d280187ce63c3bea8261;hb=3c9548186ff354eeb93e6d850d3de61a884ed089;hpb=3ff940ed5c20a17155bf998bd5aac8a735032c67 diff --git a/README.md b/README.md index ea3b242..73173c7 100644 --- a/README.md +++ b/README.md @@ -1,31 +1,25 @@ -CDSChecker Readme -================= +CDSChecker: A Model Checker for C11 and C++11 Atomics +===================================================== 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 README is divided into sections as follows: - - * Overview - * Basic build and run - * Running your own code - * Reading an execution trace - * References Overview -------- -CDSChecker is a model checker for C11/C++11 exhaustively explores the behaviors -of code under the C11/C++11 memory model. It uses partial order reduction to -eliminate redundant executions to significantly shrink the state space. -The model checking algorithm is described in more detail in this paper -(currently under review): +CDSChecker is a model checker for C11/C++11 which exhaustively explores the +behaviors of code under the C/C++ memory model. It uses partial order reduction +as well as a few other novel techniques to eliminate time spent on redundant +execution behaviors and to significantly shrink the state space. The model +checking algorithm is described in more detail in this paper (published in +OOPSLA '13): - +> It is designed to support unit tests on concurrent data structure written using -C11/C++11 atomics. +C/C++ atomics. CDSChecker is constructed as a dynamically-linked shared library which implements the C and C++ atomic types and portions of the other thread-support @@ -38,100 +32,128 @@ CDSChecker should compile on Linux and Mac OSX with no dependencies and has been tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX flavors. We have not attempted to port to Windows. -Other references can be found at the main project page: - +Getting Started +--------------- -Basic build and run -------------------- +If you haven't done so already, you may download CDSChecker using +[git](http://git-scm.com/) (for those without git, snapshots can be found at the +Gitweb URLs below): -Sample run instructions: + git clone git://demsky.eecs.uci.edu/model-checker.git -
-$ make
-$ export LD_LIBRARY_PATH=.
-$ ./test/userprog.o                   # Runs simple test program
-$ ./test/userprog.o -h                # Prints help information
-Copyright (c) 2013 Regents of the University of California. All rights reserved.
-Distributed under the GPLv2
-Written by Brian Norris and Brian Demsky
-
-Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
-
-MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
-provided after the `--' (the PROGRAM ARGS) are passed to the user program.
-
-Model-checker options:
--h, --help                  Display this help message and exit
--m, --liveness=NUM          Maximum times a thread can read from the same write
-                              while other writes exist.
-                              Default: 0
--M, --maxfv=NUM             Maximum number of future values that can be sent to
-                              the same read.
-                              Default: 0
--s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for
-                              a write from the future past the expected number
-                              of actions.
-                              Default: 6
--S, --fvslop=NUM            Future value expiration sloppiness.
-                              Default: 4
--y, --yield                 Enable CHESS-like yield-based fairness support.
-                              Default: disabled
--Y, --yieldblock            Prohibit an execution from running a yield.
-                              Default: disabled
--f, --fairness=WINDOW       Specify a fairness window in which actions that are
-                              enabled sufficiently many times should receive
-                              priority for execution (not recommended).
-                              Default: 0
--e, --enabled=COUNT         Enabled count.
-                              Default: 1
--b, --bound=MAX             Upper length bound.
-                              Default: 0
--v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:
-                              0 is quiet; 1 is noisy; 2 is noisier.
-                              Default: 0
--u, --uninitialized=VALUE   Return VALUE any load which may read from an
-                              uninitialized atomic.
-                              Default: 0
--t, --analysis=NAME         Use Analysis Plugin.
--o, --options=NAME          Option for previous analysis plugin.
-                            -o help for a list of options
- --                         Program arguments follow.
-
-Analysis plugins:
-SC
-
+Get the benchmarks (not required; distributed separately): + + cd model-checker + git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks + +Compile the model checker: + + make + +Compile the benchmarks: + + make benchmarks + +Run a simple example (the `run.sh` script does some very minimal processing for +you): + + ./run.sh test/userprog.o + +To see the help message on how to run CDSChecker, execute: + + ./run.sh -h + + +Useful Options +-------------- + +`-m num` + + > Controls the liveness of the memory system. Note that multithreaded programs + > often rely on memory liveness for termination, so this parameter is + > necessary for such programs. + > + > Liveness is controlled by `num`: the number of times a load is allowed to + > see the same store when a newer store exists---one that is ordered later in + > the modification order. + +`-y` + + > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()` + > instrumentation in test program). + +`-f num` + + > Turns on alternative fairness support (less desirable than `-y`). + +`-v` + + > Verbose: show all executions and not just buggy ones. + +`-s num` + + > Constrain how long we will run to wait for a future value past when it is + > expected +`-u num` -Note that we also provide a series of benchmarks (distributed separately), -which can be placed under the `benchmarks/` directory. After building CDSChecker, -you can build and run the benchmarks as follows: + > Value to provide to atomics loads from uninitialized memory locations. The + > default is 0, but this may cause some programs to throw exceptions + > (segfault) before the model checker prints a trace. + +Suggested options: + +> -m 2 -y + +or + +> -m 2 -f 10 + + +Benchmarks +------------------- + +Many simple tests are located in the `tests/` directory. You may also want to +try the larger benchmarks (distributed separately), which can be placed under +the `benchmarks/` directory. After building CDSChecker, you can build and run +the benchmarks as follows: + +> make benchmarks +> cd benchmarks +> +> # run barrier test with fairness/memory liveness +> ./run.sh barrier/barrier -y -m 2 +> +> # Linux reader/write lock test with fairness/memory liveness +> ./run.sh linuxrwlocks/linuxrwlocks -y -m 2 +> +> # run all benchmarks and provide timing results +> ./bench.sh - cd benchmarks - make - ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness - ./bench.sh # run all benchmarks and provide timing results Running your own code --------------------- -We provide several test and sample programs under the `test/` directory, which -should compile and run with no trouble. Of course, you likely want to test your -own code. To do so, you need to perform a few steps. +You likely want to test your own code, not just our simple tests. To do so, you +need to perform a few steps. First, because CDSChecker executes your program dozens (if not hundreds or thousands) of times, you will have the most success if your code is written as a unit test and not as a full-blown program. -Next, test programs should use the standard C11/C++11 library headers -(``/``, ``, ``, ``) and must -name their main routine as `user_main(int, char**)` rather than `main(int, char**)`. -We only support C11 thread syntax (`thrd_t`, etc. from ``). +Second, because CDSChecker must be able to manage your program for you, your +program should declare its main entry point as `user_main(int, char**)` rather +than `main(int, char**)`. + +Third, test programs must use the standard C11/C++11 library headers (see below +for supported APIs). Notably, we only support C11 thread syntax (`thrd_t`, etc. +from ``). Test programs may also use our included happens-before race detector by including and utilizing the appropriate functions -(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to -non-atomic shared memory. +(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data +to/from non-atomic shared memory. CDSChecker can also check boolean assertions in your test programs. Just include `` and use the `MODEL_ASSERT()` macro in your test program. @@ -143,6 +165,23 @@ the headers in the `include/` directory. Then the shared library must be made available to the dynamic linker, using the `LD_LIBRARY_PATH` environment variable, for instance. + +### Supported C11/C++11 APIs ### + +To model-check multithreaded code properly, CDSChecker needs to instrument any +concurrency-related API calls made in your code. Currently, we support parts of +the following thread-support libraries. The C versions can be used in either C +or C++. + +* ``, ``, `` +* `` +* `` +* `` + +Because we want to extend support to legacy (i.e., non-C++11) compilers, we do +not support some new C++11 features that can't be implemented in C++03 (e.g., +C++ ``). + Reading an execution trace -------------------------- @@ -232,6 +271,127 @@ vector consists of the following values: CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10 +End of Execution Summary +------------------------ + +CDSChecker prints summary statistics at the end of each execution. These +summaries are based off of a few different properties of an execution, which we +will break down here: + +* An _infeasible_ execution is an execution which is not consistent with the + memory model. Such an execution can be considered overhead for the + model-checker, since it should never appear in practice. + +* A _buggy_ execution is an execution in which CDSChecker has found a real + bug: a data race, a deadlock, failure of a user-provided assertion, or an + uninitialized load, for instance. CDSChecker will only report bugs in feasible + executions. + +* A _redundant_ execution is a feasible execution that is exploring the same + state space explored by a previous feasible execution. Such exploration is + another instance of overhead, so CDSChecker terminates these executions as + soon as they are detected. CDSChecker is mostly able to avoid such executions + but may encounter them if a fairness option is enabled. + +Now, we can examine the end-of-execution summary of one test program: + + $ ./run.sh test/rmwprog.o + + test/rmwprog.o + ******* Model-checking complete: ******* + Number of complete, bug-free executions: 6 + Number of redundant executions: 0 + Number of buggy executions: 0 + Number of infeasible executions: 29 + Total executions: 35 + +* _Number of complete, bug-free executions:_ these are feasible, non-buggy, and + non-redundant executions. They each represent different, legal behaviors you + can expect to see in practice. + +* _Number of redundant executions:_ these are feasible but redundant executions + that were terminated as soon as CDSChecker noticed the redundancy. + +* _Number of buggy executions:_ these are feasible, buggy executions. These are + the trouble spots where your program is triggering a bug or assertion. + Ideally, this number should be 0. + +* _Number of infeasible executions:_ these are infeasible executions, + representing some of the overhead of model-checking. + +* _Total executions:_ the total number of executions explored by CDSChecker. + Should be the sum of the above categories, since they are mutually exclusive. + + +Other Notes and Pitfalls +------------------------ + +* Deadlock detection: CDSChecker can detect deadlocks. For instance, try the + following test program. + + > ./run.sh test/deadlock.o + + Deadlock detection currently detects when a thread is about to step into a + deadlock, without actually including the final step in the trace. But you can + examine the program to see the next step. + +* CDSChecker has to speculatively explore many execution behaviors due to the + relaxed memory model, and many of these turn out to be infeasible (that is, + they cannot be legally produced by the memory model). CDSChecker discards + these executions as soon as it identifies them (see the "Number of infeasible + executions" statistic); however, the speculation can occasionally cause + CDSChecker to hit unexpected parts of the unit test program (causing a + division by 0, for instance). In such programs, you might consider running + CDSChecker with the `-u num` option. + +* Related to the previous point, CDSChecker may report more than one bug for a + particular candidate execution. This is because some bugs may not be + reportable until CDSChecker has explored more of the program, and in the + time between initial discovery and final assessment of the bug, CDSChecker may + discover another bug. + +* Data races may be reported as multiple bugs, one for each byte-address of the + data race in question. See, for example, this run: + + $ ./run.sh test/releaseseq.o + ... + Bug report: 4 bugs detected + [BUG] Data race detected @ address 0x601078: + Access 1: write in thread 2 @ clock 4 + Access 2: read in thread 3 @ clock 9 + [BUG] Data race detected @ address 0x601079: + Access 1: write in thread 2 @ clock 4 + Access 2: read in thread 3 @ clock 9 + [BUG] Data race detected @ address 0x60107a: + Access 1: write in thread 2 @ clock 4 + Access 2: read in thread 3 @ clock 9 + [BUG] Data race detected @ address 0x60107b: + Access 1: write in thread 2 @ clock 4 + Access 2: read in thread 3 @ clock 9 + + +See Also +-------- + +The CDSChecker project page: + +> + +The CDSChecker source and accompanying benchmarks on Gitweb: + +> +> +> + + +Contact +------- + +Please feel free to contact us for more information. Bug reports are welcome, +and we are happy to hear from our users. We are also very interested to know if +CDSChecker catches bugs in your programs. + +Contact Brian Norris at or Brian Demsky at . + References ----------