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

Auto merge of #2984 - RalfJung:soundness, r=RalfJung

Browse Source 
clarify that we do not prove soundness

Cc https://github.com/rust-lang/miri/issues/2982
This commit is contained in:
bors 2023-07-17 14:49:17 +00:00
commit bbabfdc4d3
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -74,12 +74,19 @@ behavior** in your program, and cannot run all programs:
unobservable by compiled programs running on real hardware when `SeqCst` fences are used, and it unobservable by compiled programs running on real hardware when `SeqCst` fences are used, and it
cannot produce all behaviors possibly observable on real hardware. 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/ [rust]: https://www.rust-lang.org/
[mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md [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 [`unreachable_unchecked`]: https://doc.rust-lang.org/stable/std/hint/fn.unreachable_unchecked.html
[`copy_nonoverlapping`]: https://doc.rust-lang.org/stable/std/ptr/fn.copy_nonoverlapping.html [`copy_nonoverlapping`]: https://doc.rust-lang.org/stable/std/ptr/fn.copy_nonoverlapping.html
[Stacked Borrows]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md [Stacked Borrows]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md
[Tree Borrows]: https://perso.crans.org/vanille/treebor/ [Tree Borrows]: https://perso.crans.org/vanille/treebor/
[Soundness]: https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#soundness-of-code--of-a-library
## Using Miri ## Using Miri