X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=README.md;h=d5838cd98be0a1f84058fc092bdeec4ab8c9ebf1;hp=a2458f43b755098a4644e1a8eda67ece24d1feb4;hb=c7a6544c3f19d8c4d71b82871c832a866f8dbb79;hpb=f7a2a9682e6edbf7db5b07d1022436fb0f7c5594 diff --git a/README.md b/README.md index a2458f4..d5838cd 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. @@ -41,7 +41,11 @@ If you haven't done so already, you may download CDSChecker using git clone git://demsky.eecs.uci.edu/model-checker.git -Get the benchmarks (not required; distributed separately): +Source code can also be downloaded via the snapshot links on Gitweb (found in +the __See Also__ section). + +Get the benchmarks (not required; distributed separately), placing them as a +subdirectory under the `model-checker` directory: cd model-checker git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks @@ -84,7 +88,9 @@ Useful Options `-f num` - > Turns on alternative fairness support (less desirable than `-y`). + > Turns on alternative fairness support (less desirable than `-y`). A + > necessary alternative for some programs that do not support yield-based + > fairness properly. `-v` @@ -120,8 +126,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 @@ -138,15 +151,15 @@ 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) and must compile against the versions provided in +CDSChecker's `include/` directory. 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. @@ -159,6 +172,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 -------------------------- @@ -215,29 +244,27 @@ The following list describes each of the columns in the execution trace output: See the following example trace: -
-------------------------------------------------------------------------------------
-#    t    Action type     MO       Location         Value               Rf  CV
-------------------------------------------------------------------------------------
-1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
-2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
-3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
-4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
-5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
-6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
-7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
-8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
-9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
-10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
-11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
-12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
-13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
-14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
-15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
-16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
-HASH 4073708854
-------------------------------------------------------------------------------------
-
+ ------------------------------------------------------------------------------------ + # t Action type MO Location Value Rf CV + ------------------------------------------------------------------------------------ + 1 1 thread start seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 1) + 2 1 init atomic relaxed 0x601068 0 ( 0, 2) + 3 1 init atomic relaxed 0x60106c 0 ( 0, 3) + 4 1 thread create seq_cst 0x7f68fe51c710 0x7f68fe51c6e0 ( 0, 4) + 5 2 thread start seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 5) + 6 2 atomic read relaxed 0x60106c 0 3 ( 0, 4, 6) + 7 1 thread create seq_cst 0x7f68fe51c720 0x7f68fe51c6e0 ( 0, 7) + 8 3 thread start seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 8) + 9 2 atomic write relaxed 0x601068 0 ( 0, 4, 9) + 10 3 atomic read relaxed 0x601068 0 2 ( 0, 7, 0, 10) + 11 2 thread finish seq_cst 0x7f68ff11ebc0 0xdeadbeef ( 0, 4, 11) + 12 3 atomic write relaxed 0x60106c 0x2a ( 0, 7, 0, 12) + 13 1 thread join seq_cst 0x7f68ff11ebc0 0x2 ( 0, 13, 11) + 14 3 thread finish seq_cst 0x7f68ff11efc0 0xdeadbeef ( 0, 7, 0, 14) + 15 1 thread join seq_cst 0x7f68ff11efc0 0x3 ( 0, 15, 11, 14) + 16 1 thread finish seq_cst 0x7f68ff11e7c0 0xdeadbeef ( 0, 16, 11, 14) + HASH 4073708854 + ------------------------------------------------------------------------------------ Now consider, for example, operation 10: @@ -248,9 +275,65 @@ 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 +------------------------ + +* Many programs require some form of fairness in order to terminate in a finite + amount of time. CDSChecker supports the `-y num` and `-f num` flags for these + cases. The `-y` option (yield-based fairness) is preferable, but it requires + careful usage of yields (i.e., `thrd_yield()`) in the test program. For + programs without proper `thrd_yield()`, you may consider using `-f` instead. * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the following test program. @@ -270,6 +353,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 --------