mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

clarify that we do not prove soundness

Browse Source
This commit is contained in:
Ralf Jung 2023-07-16 13:47:16 +02:00
parent 0548274b4b
commit d537a7aaa2
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/tools/miri/README.md
View File

@ -74,6 +74,12 @@ behavior** in your program, and cannot run all programs:
unobservable by compiled programs running on real hardware when `SeqCst` fences are used, and it
cannot produce all behaviors possibly observable on real hardware.
Moreover, Miri fundamentally cannot tell you whether your code is *sound*. Soundness is the property
of never causing undefined behavior when invoked from arbitrary safe code, even in combination with
other sound code. In contrast, Miri can just tell you if *a particular way of interacting with your
code* (e.g., a test suite) causes any undefined behavior. It is up to you to ensure sufficient
coverage.
[rust]: https://www.rust-lang.org/
[mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md
[`unreachable_unchecked`]: https://doc.rust-lang.org/stable/std/hint/fn.unreachable_unchecked.html