fix typo

[web.git] / personal / _posts / 2025-12-22-miri.md

diff --git a/personal/_posts/2025-12-22-miri.md b/personal/_posts/2025-12-22-miri.md
index 00fb7ff411c7f4c05b0c42e378e2c29d1a9a4fc8..c6ec030d61fb91a9a90df294764d5a11e8793d2b 100644 (file)
--- a/personal/_posts/2025-12-22-miri.md
+++ b/personal/_posts/2025-12-22-miri.md
@@ -13,7 +13,7 @@ This means it can find bugs in your unsafe code where you failed to uphold requi
 Miri's claim to fame is that it is a practical tool that can find *all de-facto Undefined Behavior in deterministic Rust programs*.
 To my knowledge, no other freely available tool can claim this---for any language.<!-- MORE -->[^relwork]
 
 Miri's claim to fame is that it is a practical tool that can find *all de-facto Undefined Behavior in deterministic Rust programs*.
 To my knowledge, no other freely available tool can claim this---for any language.<!-- MORE -->[^relwork]
 

-[^relwork]: Please let me know if there is such a tool and I just missed it!
+[^relwork]: Please let me know if there is such a tool and I just missed it! The paper discusses why sanitizers and valgrind, while being immensely useful tools, still miss some UB. I just know of one commercial tool that can make similar claims to Miri, the "TrustInSoft Analyzer". It requires a license, so I can't say how good its coverage of the C standard is; in particular, it would be interesting to compare what GCC and clang think is UB with what the tool thinks. In Miri, we spend a lot of time discussing with compiler folks to ensure we all have a shared understanding of what is and is not UB. In principle, this should not be needed in C since it has a standard; in practice, the standard can [diverge pretty far](https://dl.acm.org/doi/10.1145/2908080.2908081) from what programmers expect and from what compilers implement.

 
 We can only talk about *de-facto UB* because Rust has not yet stabilized its definition of Undefined Behavior.
 In lieu of that, we carefully check what the compiler does to ensure, to the best of our abilities, that all the UB which a Rust program can encounter *today* is caught by Miri.
 
 We can only talk about *de-facto UB* because Rust has not yet stabilized its definition of Undefined Behavior.
 In lieu of that, we carefully check what the compiler does to ensure, to the best of our abilities, that all the UB which a Rust program can encounter *today* is caught by Miri.


@@ -38,10 +38,10 @@ This is mostly about operating system APIs as well as CPU vendor intrinsics.
 The following list attempts to summarize which shims have been added to Miri since the previous update:
 
 - Greatly expand support for Windows API shims, covering in particular basic file access (by @beepster4096, @CraftSpider).
 The following list attempts to summarize which shims have been added to Miri since the previous update:
 
 - Greatly expand support for Windows API shims, covering in particular basic file access (by @beepster4096, @CraftSpider).

-- Support for various new file descriptor kinds on Unix and specifically Linux, such as `socketpair`, `pipe`, and `eventfd` (by @DebugSteven, @tiif, @RalfJung, @FrankReh).
+- Support for various new file descriptor kinds on Unix and specifically Linux, such as `socketpair` (only `SOCK_STREAM`), `pipe`, and `eventfd` (by @DebugSteven, @tiif, @RalfJung, @FrankReh).

 - Support for Linux `epoll` (by @tiif with some groundwork and extensions by @DebugSteven, @FrankReh, @RalfJung).
 - Broaden the general file API support (by @Pointerbender, @Jefffrey, @tiif, @newpavlov).
 - Support for Linux `epoll` (by @tiif with some groundwork and extensions by @DebugSteven, @FrankReh, @RalfJung).
 - Broaden the general file API support (by @Pointerbender, @Jefffrey, @tiif, @newpavlov).

-- Support for many Intel vendor intrinsics covering SSE2 all the way up to AVX2 (mostly by @eduardosm with some help by @TDecking and @Kixunil).
+- Support for many Intel vendor intrinsics covering SSE2 all the way up to AVX2 (mostly by @eduardosm with some help by @TDecking, @Kixunil). Thanks to @folkertdev, Miri even supports some AVX-512 intrinsics, making it a suitable [testbed](https://trifectatech.org/blog/emulating-avx-512-intrinsics-in-miri/) for code you may not be able to run on real hardware!

 - Support for basic functionality on FreeBSD (by @devnexen and @LorrensP-2158466).
 - Support for basic functionality on Illumos and Solaris (by @devnexen).
 - Support for basic functionality on Android (by @YohDeadfall).
 - Support for basic functionality on FreeBSD (by @devnexen and @LorrensP-2158466).
 - Support for basic functionality on Illumos and Solaris (by @devnexen).
 - Support for basic functionality on Android (by @YohDeadfall).


@@ -121,7 +121,7 @@ Miri is still not exactly fast, but some performance work helped significantly s
 The data race checker and weak memory support in Miri was originally based on a paper that followed the C++11 concurrency semantics.
 However, Rust is specified to use the C++20 semantics, which required some adjustments.
 @cbeuw did the bulk of that work, with help by @SabrinaJewson and @michaliskok.
 The data race checker and weak memory support in Miri was originally based on a paper that followed the C++11 concurrency semantics.
 However, Rust is specified to use the C++20 semantics, which required some adjustments.
 @cbeuw did the bulk of that work, with help by @SabrinaJewson and @michaliskok.

-(See the [paper](https://plf.inf.ethz.ch/research/popl26-miri.html) for more details on this.)
+(See [§4 in the paper](https://plf.inf.ethz.ch/research/popl26-miri.html) for more details on this.)

 As part of writing the paper, I also found and fixed two flaws in the core of the weak memory implementation.
 
 On top of this, @geetanshjuneja adjusted Miri's scheduler to be fully non-deterministic, making it possible to find issues that would not arise with round-robin scheduling.
 As part of writing the paper, I also found and fixed two flaws in the core of the weak memory implementation.
 
 On top of this, @geetanshjuneja adjusted Miri's scheduler to be fully non-deterministic, making it possible to find issues that would not arise with round-robin scheduling.


@@ -163,7 +163,7 @@ If your name should be on that list, then I am sorry for forgetting you.
 ## How you can help
 
 If you want to help improve Miri, that's awesome!
 ## How you can help
 
 If you want to help improve Miri, that's awesome!

-The [issue tracker](https://github.com/rust-lang/miri/issues) is a good place to start; the list of issues is short enough that you can just browse through it rather quickly to see if anything pikes your interest.
+The [issue tracker](https://github.com/rust-lang/miri/issues) is a good place to start; the list of issues is short enough that you can just browse through it rather quickly to see if anything piques your interest.

 The ones that are particularly suited for getting started are marked with a green label.
 Another good starting point is to try to implement the missing bit of functionality that keeps your test suite from working.
 That said, you should have gathered some Rust experience in a simpler project before tackling Miri; Miri is not a good codebase for your first steps in Rust.
 The ones that are particularly suited for getting started are marked with a green label.
 Another good starting point is to try to implement the missing bit of functionality that keeps your test suite from working.
 That said, you should have gathered some Rust experience in a simpler project before tackling Miri; Miri is not a good codebase for your first steps in Rust.