X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=README.md;h=73173c737c5ed9a6dded95c7fabfc2b9023d7b4b;hp=e020ad42a6592762a06ea4b611b240de506e4b91;hb=3c9548186ff354eeb93e6d850d3de61a884ed089;hpb=7d48344a260daccd4a4255bd7e07ab232c7ba653 diff --git a/README.md b/README.md index e020ad4..73173c7 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -CDSChecker Readme -================= +CDSChecker: A Model Checker for C11 and C++11 Atomics +===================================================== Copyright © 2013 Regents of the University of California. All rights reserved. @@ -121,8 +121,15 @@ the benchmarks as follows: > make benchmarks > cd benchmarks -> ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness -> ./bench.sh # run all benchmarks and provide timing results +> +> # 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 Running your own code @@ -139,15 +146,14 @@ 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 should use the standard C11/C++11 library headers -(``/``, ``, ``, ``). -As of now, we only support C11 thread syntax (`thrd_t`, etc. from -``). +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. @@ -160,6 +166,22 @@ 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 -------------------------- @@ -249,9 +271,59 @@ 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. -Other Notes ------------ +* 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. @@ -271,6 +343,31 @@ Other Notes 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 --------