miri bog post: minor tweaks

[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 efdca9caff007efce428b699cd3c59a2ef4fbea4..272f9c3e0944e4222e74c908128a5f15f67fa30a 100644 (file)
--- a/personal/_posts/2025-12-22-miri.md
+++ b/personal/_posts/2025-12-22-miri.md
@@ -1,6 +1,7 @@
 ---
 ---

-title: "A paper about Miri, and other Miri news"
+title: "What's \"new\" in Miri (and also, there's a Miri paper!)"

 categories: rust
 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.
 ---
 
 It is time for another "what is happening in Miri" post.


@@ -37,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).


@@ -120,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.