Copyright (c) 2013 Regents of the University of California. All rights reserved.
-CDSChecker is distributed under the GPL v2.
+CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
This README is divided into sections as follows:
Default: 1
-b, --bound=MAX Upper length bound.
Default: 0
--v, --verbose Print verbose execution information.
+-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
-o help for a list of options
-- Program arguments follow.
+Analysis plugins:
+SC
+
Note that we also provide a series of benchmarks (distributed separately),
which can be placed under the benchmarks/ directory. After building CDSChecker,
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
-from non-atomic shared memory.
+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 will report a bug in any possible execution in which the argument to
+MODEL_ASSERT() evaluates to false (that is, 0).
Test programs should be compiled against our shared library (libmodel.so) using
the headers in the include/ directory. Then the shared library must be made