From d537a7aaa26b48e723dcea0e1d065690a5632b45 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 16 Jul 2023 13:47:16 +0200 Subject: [PATCH 1/2] clarify that we do not prove soundness --- src/tools/miri/README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index 601101905f1..d51384d0a14 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -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 From 75da07bf28e64aadbc6f452da4d0cb44e4223b5a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 16 Jul 2023 15:51:46 +0200 Subject: [PATCH 2/2] link to a definition of soundness --- src/tools/miri/README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index d51384d0a14..a965f44a4e6 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -74,7 +74,7 @@ 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 +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 @@ -86,6 +86,7 @@ coverage. [`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 [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