X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README.md;h=ba64e188ddbc956c0a941d83687ebc171c9bec1c;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hp=de8c3ef5c18699cf6d1b499b32c16c38ac920c5c;hpb=f8417a2a7b21e1b14fb8ce905640f96aafdf8177;p=model-checker.git
diff --git a/README.md b/README.md
index de8c3ef..ba64e18 100644
--- a/README.md
+++ b/README.md
@@ -1,14 +1,6 @@
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.
-
-
-Overview
---------
-
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
@@ -37,12 +29,15 @@ 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](http://git-scm.com/):
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
@@ -85,7 +80,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`
@@ -239,29 +236,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:
@@ -326,6 +321,12 @@ Now, we can examine the end-of-execution summary of one test program:
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.
@@ -375,7 +376,7 @@ See Also
The CDSChecker project page:
->
+>
The CDSChecker source and accompanying benchmarks on Gitweb:
@@ -394,6 +395,14 @@ CDSChecker catches bugs in your programs.
Contact Brian Norris at or Brian Demsky at .
+Copyright
+---------
+
+Copyright © 2013 Regents of the University of California. All rights reserved.
+
+CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
+
+
References
----------