+++ /dev/null
-****************************************
-CDSChecker Readme
-****************************************
-
-Copyright (c) 2013 Regents of the University of California. All rights reserved.
-
-CDSChecker is distributed under the GPL v2.
-
-CDSChecker compiles as a dynamically-linked shared library by simply running
-'make'. It should compile on Linux and Mac OSX, and has been tested with LLVM
-(clang/clang++) and GCC.
-
-Test programs should use the standard C11/C++11 library headers
-(<atomic>/<stdatomic.h>, <mutex>, <condition_variable>, <thread.h>) and must
-name their main routine as user_main(int, char**) rather than main(int, char**).
-We only support C11 thread syntax (thrd_t, etc. from <thread.h>).
-
-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.
-
-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
-available to the dynamic linker, using the LD_LIBRARY_PATH environment
-variable, for instance.
-
-Sample run instructions:
-
-$ make
-$ export LD_LIBRARY_PATH=.
-$ ./test/userprog.o # Runs simple test program
-$ ./test/userprog.o -h # Prints help information
-Copyright (c) 2013 Regents of the University of California. All rights reserved.
-Distributed under the GPLv2
-Written by Brian Norris and Brian Demsky
-
-Usage: ./test/userprog.o [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]
-
-MODLE-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments
-provided after the `--' (the PROGRAM ARGS) are passed to the user program.
-
-Model-checker options:
--h, --help Display this help message and exit
--m, --liveness=NUM Maximum times a thread can read from the same write
- while other writes exist.
- Default: 0
--M, --maxfv=NUM Maximum number of future values that can be sent to
- the same read.
- Default: 0
--s, --maxfvdelay=NUM Maximum actions that the model checker will wait for
- a write from the future past the expected number
- of actions.
- Default: 6
--S, --fvslop=NUM Future value expiration sloppiness.
- Default: 4
--y, --yield Enable CHESS-like yield-based fairness support.
- Default: disabled
--Y, --yieldblock Prohibit an execution from running a yield.
- Default: disabled
--f, --fairness=WINDOW Specify a fairness window in which actions that are
- enabled sufficiently many times should receive
- priority for execution (not recommended).
- Default: 0
--e, --enabled=COUNT Enabled count.
- Default: 1
--b, --bound=MAX Upper length bound.
- Default: 0
--v, --verbose Print verbose execution information.
--u, --uninitialized=VALUE Return VALUE any load which may read from an
- uninitialized atomic.
- Default: 0
--c, --analysis Use SC Trace Analysis.
- -- Program arguments follow.
-
-
-Note that we also provide a series of benchmarks (distributed separately),
-which can be placed under the benchmarks/ directory. After building CDSChecker,
-you can build and run the benchmarks as follows:
-
- cd benchmarks
- make
- ./run.sh barrier/barrier -y -m 2 # runs barrier test with fairness/memory liveness
- ./bench.sh # run all benchmarks twice, with timing results
projects / c11tester.git / blobdiff