X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README.md;h=ba64e188ddbc956c0a941d83687ebc171c9bec1c;hb=refs%2Fheads%2Fmaster;hp=c85a727db920d6fd8758188c0c285960eb436536;hpb=278ff43e5570a6cd8a42aa03070c5b59d079a999;p=model-checker.git

diff --git a/README.md b/README.md
index c85a727..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`
 
@@ -324,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.
 
@@ -373,7 +376,7 @@ See Also
 
 The CDSChecker project page:
 
->   <http://demsky.eecs.uci.edu/c11modelchecker.php>
+>   <http://demsky.eecs.uci.edu/c11modelchecker.html>
 
 The CDSChecker source and accompanying benchmarks on Gitweb:
 
@@ -392,6 +395,14 @@ CDSChecker catches bugs in your programs.
 Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
 
 
+Copyright
+---------
+
+Copyright &copy; 2013 Regents of the University of California. All rights reserved.
+
+CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
+
+
 References
 ----------