You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
BASIC="empty_main integer heap_alloc libc-mem vec string btreemap"# ensures we have the basics: pre-main code, system allocator
154
154
UNIX="hello panic/panic panic/unwind concurrency/simple atomic libc-mem libc-misc libc-random env num_cpus"# the things that are very similar across all Unixes, and hence easily supported there
155
155
TEST_TARGET=aarch64-linux-android run_tests_minimal $BASIC$UNIXtime hashmap random thread sync concurrency epoll eventfd
Copy file name to clipboardExpand all lines: doc/genmc.md
+34-4Lines changed: 34 additions & 4 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -9,9 +9,7 @@ Miri-GenMC integrates that model checker into Miri.
9
9
10
10
## Usage
11
11
12
-
**IMPORTANT: The license of GenMC and thus the `genmc-sys` crate in the Miri repo is currently "GPL-3.0-or-later", so a binary produced with the `genmc` feature is subject to the requirements of the GPL. As long as that remains the case, the `genmc` feature of Miri is OFF-BY-DEFAULT and must be OFF for all Miri releases.**
13
-
14
-
For testing/developing Miri-GenMC (while keeping in mind the licensing issues):
12
+
For testing/developing Miri-GenMC:
15
13
- clone the Miri repo.
16
14
- build Miri-GenMC with `./miri build --features=genmc`.
17
15
- OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
@@ -21,7 +19,30 @@ Basic usage:
21
19
MIRIFLAGS="-Zmiri-genmc" cargo miri run
22
20
```
23
21
24
-
<!-- FIXME(genmc): explain options. -->
22
+
Note that `cargo miri test` in GenMC mode is currently not supported.
23
+
24
+
### Supported Parameters
25
+
26
+
-`-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
27
+
-`-Zmiri-genmc-estimate`: This enables estimation of the concurrent execution space and verification time, before running the full verification. This should help users detect when their program is too complex to fully verify in a reasonable time. This will explore enough executions to make a good estimation, but at least 10 and at most `estimation-max` executions.
28
+
-`-Zmiri-genmc-estimation-max={MAX_ITERATIONS}`: Set the maximum number of executions that will be explored during estimation (default: 1000).
29
+
-`-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
30
+
-`-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
31
+
-`-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
32
+
-`-Zmiri-genmc-log=LOG_LEVEL`: Change the log level for GenMC. Default: `warning`.
33
+
-`quiet`: Disable logging.
34
+
-`error`: Print errors.
35
+
-`warning`: Print errors and warnings.
36
+
-`tip`: Print errors, warnings and tips.
37
+
- If Miri is built with debug assertions, there are additional log levels available (downgraded to `tip` without debug assertions):
38
+
-`debug1`: Print revisits considered by GenMC.
39
+
-`debug2`: Print the execution graph after every memory access.
40
+
-`debug3`: Print reads-from values considered by GenMC.
41
+
-`-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
42
+
43
+
#### Regular Miri parameters useful for GenMC mode
44
+
45
+
-`-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).
25
46
26
47
<!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
27
48
@@ -57,6 +78,15 @@ The process for obtaining them is as follows:
57
78
If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
58
79
formatting the Rust files inside that folder.
59
80
81
+
### Formatting the C++ code
82
+
83
+
For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
84
+
With `clang-format` installed, run this command to format the c++ files (replace the `-i` with `--dry-run` to just see the changes.):
0 commit comments