X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README.md;h=de8c3ef5c18699cf6d1b499b32c16c38ac920c5c;hb=26010e1410faa0dcefc8d384872bc0210cc0be92;hp=c8f755041d385d23832d6837c3eb94ac06019809;hpb=1c9f756acfac5eb9bc4fba73967e73e2aafa8323;p=model-checker.git diff --git a/README.md b/README.md index c8f7550..de8c3ef 100644 --- a/README.md +++ b/README.md @@ -146,15 +146,15 @@ Second, because CDSChecker must be able to manage your program for you, your program should declare its main entry point as `user_main(int, char**)` rather than `main(int, char**)`. -Third, test programs should use the standard C11/C++11 library headers -(``/``, ``, ``, ``). -As of now, we only support C11 thread syntax (`thrd_t`, etc. from -``). +Third, test programs must use the standard C11/C++11 library headers (see below +for supported APIs) and must compile against the versions provided in +CDSChecker's `include/` directory. Notably, we only support C11 thread syntax +(`thrd_t`, etc. from ``). Test programs may also use our included happens-before race detector by including and utilizing the appropriate functions -(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for loading/storing data from/to -non-atomic shared memory. +(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data +to/from non-atomic shared memory. CDSChecker can also check boolean assertions in your test programs. Just include `` and use the `MODEL_ASSERT()` macro in your test program. @@ -167,6 +167,22 @@ available to the dynamic linker, using the `LD_LIBRARY_PATH` environment variable, for instance. +### Supported C11/C++11 APIs ### + +To model-check multithreaded code properly, CDSChecker needs to instrument any +concurrency-related API calls made in your code. Currently, we support parts of +the following thread-support libraries. The C versions can be used in either C +or C++. + +* ``, ``, `` +* `` +* `` +* `` + +Because we want to extend support to legacy (i.e., non-C++11) compilers, we do +not support some new C++11 features that can't be implemented in C++03 (e.g., +C++ ``). + Reading an execution trace --------------------------