personal/_posts/2025-12-22-miri.md

   1 ---
   2 title: "A paper about Miri, and other Miri news"
   3 categories: rust
   4 ---
   5
   6 It is time for another "what is happening in Miri" post.
   7 In fact this is *way* overdue, with the [previous update]({% post_url 2022-07-02-miri %}) being from more than 3 years ago (what even is time?!?), but it is also increasingly hard to find the time to blog, so... here we are.
   8 Better late than never. :)
   9
  10 For the uninitiated, [Miri](https://github.com/rust-lang/miri/) is an [Undefined Behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) testing tool for Rust.
  11 This means it can find bugs in your unsafe code where you failed to uphold requirements like "all accesses must be aligned" or "mutable references must never alias" or "there must not be any data races".
  12 Miri's claim to fame is that it is a practical tool that can find *all de-facto Undefined Behavior in deterministic Rust programs*.
  13 To my knowledge, no other freely available tool can claim this---for any language.<!-- MORE -->[^relwork]
  14
  15 [^relwork]: Please let me know if there is such a tool and I just missed it!
  16
  17 We can only talk about *de-facto UB* because Rust has not yet stabilized its definition of Undefined Behavior.
  18 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.
  19 This means a program that passes Miri should be compiled correctly on *today's* compiler, but the same program might suffer from UB in the future.
  20 Furthermore, if a Rust program is *non-deterministic*, that means it can execute in more than one way, and Miri will only execute it once.
  21 You can ask Miri to randomly explore multiple possible executions with `-Zmiri-many-seeds`, but there might always be more executions that Miri did not find yet.
  22 This is a fundamental limitation of all testing tools; you generally have to reach for model checking or deductive verification to overcome this.
  23
  24 To learn more about Miri, you can read the [**paper**](https://plf.inf.ethz.ch/research/popl26-miri.html).
  25 Yes, there's a paper! That's the first bit of news.
  26 *"Miri: Practical Undefined Behavior Detection for Rust"* has been accepted to POPL 2026, one of the most prestigious and competitive conferences for fundamental research in Programming Languages.
  27
  28 ## Miri progress
  29
  30 The paper aside, what progress has Miri made in the last three years?
  31 We have landed over 1500 PRs in that time, so it is impossible to go into all the details, but I will do my best to highlight the general trends and point out anything major.
  32
  33 ### Shims
  34
  35 The bread-and-butter of new features added to Miri is to add shims for functions that are implemented outside of Rust and hence cannot be directly executed by Miri.
  36 This is mostly about operating system APIs as well as CPU vendor intrinsics.
  37 The following list attempts to summarize which shims have been added to Miri since the previous update:
  38
  39 - Greatly expand support for Windows API shims, covering in particular basic file access (by @beepster4096, @CraftSpider).
  40 - Support for various new file descriptor kinds on Unix and specifically Linux, such as `socketpair`, `pipe`, and `eventfd` (by @DebugSteven, @tiif, @RalfJung, @FrankReh).
  41 - Support for Linux `epoll` (by @tiif with some groundwork and extensions by @DebugSteven, @FrankReh, @RalfJung).
  42 - Broaden the general file API support (by @Pointerbender, @Jefffrey, @tiif, @newpavlov).
  43 - Support for many Intel vendor intrinsics covering SSE2 all the way up to AVX2 (mostly by @eduardosm with some help by @TDecking and @Kixunil).
  44 - Support for basic functionality on FreeBSD (by @devnexen and @LorrensP-2158466).
  45 - Support for basic functionality on Illumos and Solaris (by @devnexen).
  46 - Support for basic functionality on Android (by @YohDeadfall).
  47 - Improve shims for pthread synchronization operations (by @Mandragorian, @LorrensP-2158466, @RalfJung).
  48 - Extend our support for macOS-specific APIs (by @joboet).
  49 - Support for weak definitions (by @bjorn3).
  50 - Support for miscellaneous small system APIs (by @folkertdev, @Mandragorian, @tgross35, @rayslava, @LorrensP-2158466, @YohDeadfall, @vishruth-thimmaiah, @saethlin, @RalfJung).
  51 - Support for global constructors that execute before `main` (by @ibraheemdev).
  52
  53 ### Diagnostics
  54
  55 Our diagnostics have improved dramatically since the last blog post, mostly thanks to @saethlin.
  56 For instance, a data race error now points at both of the accesses that caused the race:
  57 ```
  58 error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `unnamed-1` and (2) non-atomic write on thread `unnamed-2` at alloc87
  59   --> tests/fail/data_race/read_write_race.rs:24:13
  60    |
  61 24 | ...   *c.0 = 64; //~ ERROR: Data race detected between (1) non-atomic read on thread `unnamed-1` and (2) non-atomic write on thread ...
  62    |       ^^^^^^^^^ (2) just happened here
  63    |
  64 help: and (1) occurred earlier here
  65   --> tests/fail/data_race/read_write_race.rs:19:24
  66    |
  67 19 |             let _val = *c.0;
  68    |                        ^^^^
  69 ```
  70 A use-after-free error shows where the allocation this pointer points to got created and where it got freed:
  71 ```
  72 error: Undefined Behavior: memory access failed: alloc194 has been freed, so this pointer is dangling
  73  --> tests/fail/dangling_pointers/dangling_pointer_deref.rs:9:22
  74   |
  75 9 |     let x = unsafe { *p }; //~ ERROR: has been freed
  76   |                      ^^ Undefined Behavior occurred here
  77   |
  78 help: alloc194 was allocated here:
  79  --> tests/fail/dangling_pointers/dangling_pointer_deref.rs:6:17
  80   |
  81 6 |         let b = Box::new(42);
  82   |                 ^^^^^^^^^^^^
  83 help: alloc194 was deallocated here:
  84  --> tests/fail/dangling_pointers/dangling_pointer_deref.rs:8:5
  85   |
  86 8 |     };
  87   |     ^
  88 ```
  89 A Stacked Borrows error shows where the relevant pointer got created, and where it got invalidated:
  90 ```
  91 error: Undefined Behavior: attempting a write access using <254> at alloc115[0x0], but that tag does not exist in the borrow stack for this location
  92  --> tests/fail/stacked_borrows/illegal_write2.rs:8:14
  93   |
  94 8 |     unsafe { *target2 = 13 }; //~ ERROR: /write access .* tag does not exist in the borrow stack/
  95   |              ^^^^^^^^^^^^^ this error occurs as part of an access at alloc115[0x0..0x4]
  96   |
  97 help: <254> was created by a SharedReadWrite retag at offsets [0x0..0x4]
  98  --> tests/fail/stacked_borrows/illegal_write2.rs:5:19
  99   |
 100 5 |     let target2 = target as *mut _;
 101   |                   ^^^^^^
 102 help: <254> was later invalidated at offsets [0x0..0x4] by a Unique retag
 103  --> tests/fail/stacked_borrows/illegal_write2.rs:6:10
 104   |
 105 6 |     drop(&mut *target); // reborrow
 106   |          ^^^^^^^^^^^^
 107 ```
 108
 109 @Vanille-N implemented similar tracking for Tree Borrows, so its errors are on par with those emitted by Stacked Borrows.
 110 @Zoxc also contributed logic to improve data race errors that involve the aliasing model.
 111
 112 ### Optimizations
 113
 114 Miri is still not exactly fast, but some performance work helped significantly speed up Miri's aliasing checks:
 115 - @saethlin added a garbage collector for pointer tags to Miri, allowing Stacked Borrows to skip a lot of work related to tracking pointers that do not exist anymore.
 116 - @JojoDeveloping added various optimizations to the Tree Borrows checker.
 117
 118 ### Improved concurrency support
 119
 120 The data race checker and weak memory support in Miri was originally based on a paper that followed the C++11 concurrency semantics.
 121 However, Rust is specified to use the C++20 semantics, which required some adjustments.
 122 @cbeuw did the bulk of that work, with help by @SabrinaJewson and @michaliskok.
 123 (See the [paper](https://plf.inf.ethz.ch/research/popl26-miri.html) for more details on this.)
 124 As part of writing the paper, I also found and fixed two flaws in the core of the weak memory implementation.
 125
 126 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.
 127 Furthermore, @pvdrz added support for entirely "virtual" timekeeping to the scheduler, allowing Miri to support a monotone clock in a fully deterministic way.
 128 I also made Miri correctly enforce the restrictions for atomic accesses in read-only memory (which is mostly forbidden, with a few exceptions).
 129
 130 Finally, @Patrick-6 has laid the groundwork for integrating GenMC into Miri.
 131 GenMC is a weak memory model checker written by @michaliskok, which means that it can enumerate *all* behaviors of a concurrent program (as long as the program has no unbounded loops).
 132 By combining it with Miri, we can do full UB checking for all these executions.
 133 (When I mentioned model checking in the introduction, that was indeed foreshadowing. :)
 134 At the moment, using Miri+GenMC is still highly experimental, slow, and requires a custom build of Miri, but the first steps are taken and I am quite excited about the future potential of this combination!
 135
 136 ### Invoking native code from Miri
 137
 138 Did you know that Miri can execute native code invoked from Rust via FFI?
 139 This support is very experimental and incomplete, and obviously the native code then runs without any UB checking, but there have been significant improvements since the previous update:
 140
 141 - @Strophox has implemented support for sharing Rust-allocated memory with the native code.
 142 - @nia-e has added some truly cursed magic to let Miri trace quite precisely which memory the native code accesses, and use that to improve Miri's UB checking. I hear she has plans for making this even more powerful in the future. :)
 143
 144 ### Miscellaneous
 145
 146 Finally, we had some contributions that are large enough to be worth mentioning, but did not fit any of the categories above:
 147
 148 - The memory leak detector can now take into account main-thread thread-local storage (by @max-heller).
 149 - Our representation of file descriptions is a lot more flexible and extensible (by @Luv-Ray, @oli-obk, @RalfJung).
 150 - Miri now makes the precision of some floating-point operations non-deterministic to catch code incorrectly relying on precise or deterministic answers (by @LorrensP-2158466).
 151 - Miri non-deterministically causes `read` and `write` operations to only process a part of the buffer to catch programs that incorrectly rely on such operations reliably completing immediately (by @RalfJung).
 152 - Tree Borrows now by default tracks `UnsafeCell` as precisely as Stacked Borrows, catching UB when other bytes behind the same reference are incorrectly mutated (by @yoctocell, @JojoDeveloping).
 153 - Tree Borrows now supports wildcard provenance, so Miri can check programs that use integer-to-pointer casts and still catch some of the bugs involving those pointers (by @royAmmerschuber).
 154 - Miri can detect UB related to in-place ("move") function arguments (by @RalfJung).
 155 - Miri supports precise profiling, tracking where all the execution time is spent (by @Stypox).
 156 - Miri no longer needs xargo, cutting down the setup effort (by @RalfJung).
 157
 158 On top of this, there has been a lot of bug-fixing as well as continuous refactoring and cleanup to keep the code maintainable.
 159 Thank you to everyone who contributed.
 160 If your name should be on that list, then I am sorry for forgetting you.
 161
 162 ## How you can help
 163
 164 If you want to help improve Miri, that's awesome!
 165 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.
 166 The ones that are particularly suited for getting started are marked with a green label.
 167 Another good starting point is to try to implement the missing bit of functionality that keeps your test suite from working.
 168 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.
 169 However, if you already know Rust, Miri can be a fun and rewarding next challenge!
 170 If you need any mentoring, just [get in touch](https://rust-lang.zulipchat.com/#narrow/stream/269128-miri). :)
 171
 172 We are currently looking for someone who wants to maintain Miri's support for wasm targets.
 173 The wasm API is quite different from other OS APIs, so maintaining those shims without the help of someone who actually knows and understands the wasm ecosystem turned out to not be sustainable.
 174 Furthermore, we are also looking for someone with Android experience to serve as Android target maintainer for Miri.
 175 This mostly means fixing Android-specific issues that come up due to changes in the standard library -- which should be rare, but when it happens it is really useful to have someone to ping.
 176 Android is also fairly close to passing our entire test suite, so you could make it your challenge to fix the remaining bits and pieces.
 177
 178 That's all for now!
 179 I am immensely proud of what Miri has become, and deeply grateful to everyone who helped us get here.
 180 Thanks to Miri and other tools based on Miri's understanding of UB, avoiding Undefined Behavior in unsafe code becomes practically possible even at scale, while at the same time giving us a chance to specify UB in a way that satisfies the needs of real-world unsafe code out there.
 181 This has worked out way better than I could have ever imagined,
 182 and it would not have been possible without the entire amazing Rust community being on-board -- I am looking forward to seeing what's next. :D