README.md: remove <pre></pre> tags

[model-checker.git] / README.md

diff --git a/README.md b/README.md
index 37eb96265e56d130ea288471c666e23b68b73268..c85a727db920d6fd8758188c0c285960eb436536 100644 (file)
--- 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.
 
 
 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
 --------
 
 
 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):

 
 

-  [http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf](http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf)
+>   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>

 
 It is designed to support unit tests on concurrent data structure written using
 
 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
 
 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,129 @@ 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.
 
 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:

 
 

-  [http://demsky.eecs.uci.edu/c11modelchecker.php](http://demsky.eecs.uci.edu/c11modelchecker.php)
+Getting Started
+---------------
+
+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):
+
+      git clone git://demsky.eecs.uci.edu/model-checker.git
+
+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

 
 

-Basic build and run
+`-u num`
+
+  > 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

 -------------------
 
 -------------------
 

-Sample run instructions:
-
-<pre>
-$ 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
-</pre>
-
-
-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:
-
-        cd benchmarks
-        make
-        ./run.sh barrier/barrier -y -m 2     # runs barrier test with fairness/memory liveness
-        ./bench.sh                           # run all benchmarks twice, with timing results
+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
+

 
 Running your own code
 ---------------------
 
 
 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.
 
 
 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
-(`<atomic>`/`<stdatomic.h>`, `<mutex>`, `<condition_variable>`, `<thread.h>`) 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 `<thread.h>`).
+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) and must compile against the versions provided in
+CDSChecker's `include/` directory. Notably, we only support C11 thread syntax
+(`thrd_t`, etc. from `<thread.h>`).

 
 Test programs may also use our included happens-before race detector by
 including <librace.h> and utilizing the appropriate functions
 
 Test programs may also use our included happens-before race detector by
 including <librace.h> 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 `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
 
 CDSChecker can also check boolean assertions in your test programs. Just
 include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.


@@ -143,10 +166,27 @@ 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.
 
 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++.
+
+* `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
+* `<condition_variable>`
+* `<mutex>`
+* `<threads.h>`
+
+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++ `<thread>`).
+

 Reading an execution trace
 --------------------------
 
 Reading an execution trace
 --------------------------
 

-When CDSChecker detects a bug in your program (or when run with the --verbose
+When CDSChecker detects a bug in your program (or when run with the `--verbose`

 flag), it prints the output of the program run (STDOUT) along with some summary
 trace information for the execution in question. The trace is given as a
 sequence of lines, where each line represents an operation in the execution
 flag), it prints the output of the program run (STDOUT) along with some summary
 trace information for the execution in question. The trace is given as a
 sequence of lines, where each line represents an operation in the execution


@@ -166,8 +206,8 @@ The following list describes each of the columns in the execution trace output:
 
  * Action type: The type of operation performed
 
 
  * Action type: The type of operation performed
 

- * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where XXX is
-   relaxed, release, acquire, rel_acq, or seq_cst)
+ * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
+   `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)

 
  * Location: The memory location on which this operation is operating. This is
    well-defined for atomic write/read/RMW, but other operations are subject to
 
  * Location: The memory location on which this operation is operating. This is
    well-defined for atomic write/read/RMW, but other operations are subject to


@@ -176,11 +216,11 @@ The following list describes each of the columns in the execution trace output:
  * Value: For reads/writes/RMW, the value returned by the operation. Note that
    for RMW, this is the value that is *read*, not the value that was *written*.
    For other operations, 'value' may have some CDSChecker-internal meaning, or
  * Value: For reads/writes/RMW, the value returned by the operation. Note that
    for RMW, this is the value that is *read*, not the value that was *written*.
    For other operations, 'value' may have some CDSChecker-internal meaning, or

-   it may simply be a don't-care (such as 0xdeadbeef).
+   it may simply be a don't-care (such as `0xdeadbeef`).

 
  * Rf: For reads, the sequence number of the operation from which it reads.
    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
 
  * Rf: For reads, the sequence number of the operation from which it reads.
    [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),

-   as printed during --verbose execution, reads may not be resolved and so may
+   as printed during `--verbose` execution, reads may not be resolved and so may

    have Rf=? or Rf=Px, where x is a promised future value.]
 
  * CV: The clock vector, encapsulating the happens-before relation (see our
    have Rf=? or Rf=Px, where x is a promised future value.]
 
  * CV: The clock vector, encapsulating the happens-before relation (see our


@@ -199,39 +239,158 @@ The following list describes each of the columns in the execution trace output:
 
 See the following example trace:
 
 
 See the following example trace:
 

-<pre>
-------------------------------------------------------------------------------------
-#    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
-------------------------------------------------------------------------------------
-</pre>
+    ------------------------------------------------------------------------------------
+    #    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:
 
 This is the 10th operation in the execution order. It is an atomic read-relaxed
 
 Now consider, for example, operation 10:
 
 This is the 10th operation in the execution order. It is an atomic read-relaxed

-operation performed by thread 3 at memory address 0x601068. It reads the value
+operation performed by thread 3 at memory address `0x601068`. It reads the value

 "0", which was written by the 2nd operation in the execution order. Its clock
 vector consists of the following values:
 
         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 
 "0", which was written by the 2nd operation in the execution order. Its clock
 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:
+
+>   <http://demsky.eecs.uci.edu/c11modelchecker.php>
+
+The CDSChecker source and accompanying benchmarks on Gitweb:
+
+>   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
+>
+>   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
+
+
+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 <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
+

 
 References
 ----------
 
 References
 ----------