README: add bit on MODEL_ASSERT() macro

[model-checker.git] / README

diff --git a/README b/README
index cdeea6eda6a50e4b8bed3f93a69666f823897128..3064ce64e3c8cfe1d64c984ce480f5191b0a6e6a 100644 (file)
--- a/README
+++ b/README
@@ -134,7 +134,12 @@ 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.
+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