---
-title: "A paper about Miri, and other Miri news"
+title: "What's \"new\" in Miri (and also, there's a Miri paper!)"
categories: rust
+reddit: /rust/comments/1pt3kfx/whats_new_in_miri_and_also_theres_a_miri_paper/
---
It is time for another "what is happening in Miri" post.
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.
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 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).
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.
projects / web.git / blobdiff