README.md: reporting multiple data races for the same access?

[model-checker.git] / README.md

diff --git a/README.md b/README.md
index 5132935423d28648cee0715d04bd9015fc1bb180..fa54aca1b964ba5e030c8a089793bdddc8e01029 100644 (file)
--- 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.
 
@@ -16,7 +16,7 @@ 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>
 
 It is designed to support unit tests on concurrent data structure written using
 C/C++ atomics.
@@ -32,16 +32,13 @@ 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.
 
-You may also refer to the CDSChecker project page:
-
-  <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/):
+[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
 
@@ -124,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
@@ -253,8 +257,8 @@ vector consists of the following values:
         CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
 
 
-Other Notes
------------
+Other Notes and Pitfalls
+------------------------
 
 * Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
   following test program.
@@ -274,6 +278,45 @@ 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
+--------
+
+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
 -------