X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=README.md;h=3557e1db80fcbaebb485df2fd9874d23c1d7fc81;hb=HEAD;hp=8ae834c4def5af80b37ed5ff5aceba8ac72ea239;hpb=98ac1429b9b2801c8c3266d736d86c465a2e7232;p=c11tester.git diff --git a/README.md b/README.md index 8ae834c4..3557e1db 100644 --- a/README.md +++ b/README.md @@ -55,21 +55,11 @@ Useful Options > Specify the number number of executions to run. -`-u num` - - > Value to provide to atomics loads from uninitialized memory locations. The - > default is 0, but this may cause some programs to throw exceptions - > (segfault) before the model checker prints a trace. - Benchmarks ------------------- -Many simple tests are located in the `test/` directory. These are -manually instrumented and can just be run. - -You may also want to try the larger benchmarks (distributed -separately). These require LLVM to instrument. - +The benchmarks are distributed separately. These require LLVM to instrument. +You may also follow the steps in the Artifact Appendix of our paper (https://dl.acm.org/doi/abs/10.1145/3445814.3446711) to run the benchmarks. Running your own code --------------------- @@ -179,9 +169,8 @@ summaries are based off of a few different properties of an execution, which we will break down here: * A _buggy_ execution is an execution in which C11Tester has found a real - bug: a data race, a deadlock, failure of a user-provided assertion, or an - uninitialized load, for instance. C11Tester will only report bugs in feasible - executions. + bug: a data race, a deadlock, or a failure of a user-provided assertion. + C11Tester will only report bugs in feasible executions. Other Notes and Pitfalls