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
Copy file name to clipboardExpand all lines: README.md
+2-1Lines changed: 2 additions & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -220,7 +220,7 @@ degree documented below):
220
220
- `solaris` / `illumos`: maintained by @devnexen. Supports the entire test suite.
221
221
- `freebsd`: maintained by @YohDeadfall and @LorrensP-2158466. Supports the entire test suite.
222
222
- `android`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
223
-
- `wasi`: **maintainer wanted**. Support very incomplete, not even standard output works, but an empty `main` function works.
223
+
- `wasi`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
224
224
- For targets on other operating systems, Miri might fail before even reaching the `main` function.
225
225
226
226
However, even for targets that we do support, the degree of support for accessing platform APIs
@@ -606,6 +606,7 @@ Definite bugs found:
606
606
* [A bug in the new `RwLock::downgrade` implementation](https://rust-lang.zulipchat.com/#narrow/channel/269128-miri/topic/Miri.20error.20library.20test) (caught by Miri before it landed in the Rust repo)
607
607
* [Mockall reading uninitialized memory when mocking `std::io::Read::read`, even if all expectations are satisfied](https://github.com/asomers/mockall/issues/647) (caught by Miri running Tokio's test suite)
608
608
* [`ReentrantLock` not correctly dealing with reuse of addresses for TLS storage of different threads](https://github.com/rust-lang/rust/pull/141248)
609
+
* [Rare Deadlock in the thread (un)parking example code](https://github.com/rust-lang/rust/issues/145816)
609
610
610
611
Violations of [Stacked Borrows] found that are likely bugs (but Stacked Borrows is currently just an experiment):
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