From: Brian Norris <banorris@uci.edu>
Date: Wed, 14 Nov 2012 03:31:02 +0000 (-0800)
Subject: README
X-Git-Tag: pldi2013~2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=dd56df466206a5f34f1d9b1777d1f076f7c33e0f;hp=f5ec684987a17e41940dd3c80ad2b98460181054;p=model-checker.git

README
---

diff --git a/README b/README
new file mode 100644
index 0000000..de6bbc9
--- /dev/null
+++ b/README
@@ -0,0 +1,30 @@
+****************************************
+CDSChecker Readme
+****************************************
+
+This is an evaluation-only version of CDSChecker. Please do not distribute.
+
+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=.
+  # run test program