+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
+------------------------
+
+* 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.
+
+ > ./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.html>
+
+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>.
+
+
+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.
+