src_base: "/home/r/src"
out_base: "projects"
projects:
- - name: "lilass"
+ - name: "bubblebox"
- name: "dyn-nsupdate"
- - name: "zonemaker"
- - name: "schsh"
- - name: "rust-101"
- src: "rust/my/rust-101"
- name: "git-mirror"
+ - name: "lilass"
+ - name: "rust-101"
+ src: "rust/rust-101"
+ - name: "schsh"
+ - name: "zonemaker"
defaults:
- scope:
{% if include.item.author %} • {{ include.item.author }}{% endif %}
{% if include.item.meta %} • {{ include.item.meta }}{% endif %}
{% if include.item.categories %} • {{ include.item.categories | category_links }}{% endif %}
- • <a href="https://git.ralfj.de/web.git/history/refs/heads/master:/ralf/{{include.item.path}}">Edits</a>
+ • <a href="https://git.ralfj.de/web.git/history/refs/heads/master:/personal/{{include.item.path}}">Edits</a>
• <a href="{{ include.item.url }}">Permalink</a>
It turns out that the underlying reason for this observation is also a nice illustration for the concept of *semantic types* that comes up in my [work on formalizing Rust]({% post_url 2015-10-12-formalizing-rust %}) (or rather, its type system).
Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.
-**Update (Jan 11th):** Clarified the role of privacy; argued why `evil` is the problem.
+**Update (2016-01-11):** Clarified the role of privacy; argued why `evil` is the problem.
<!-- MORE -->
I spelled out the details [in the RFC issue](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-372109981).
So, if we want to declare that shared pinning is a typestate in its own right---which overall seems desirable---do we want it to be restricted like this due to an implementation detail of arbitrary self types?
-**Update:** @Diggsey [points out](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-379230538) that we can still have a `PinRefCell` with a method like `fn get_pin(self: Pin<PinRefCell<T>>) -> Pin<T>`, as long as the `PinRefCell` never gives out mutable references. So it turns out that combining interior mutability and pinning should work fine. Later, @glaebhoerl suggested we can even [combine `RefCell` and `PinRefCell` into one type if we dynamically track the pinning state](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281/11?u=ralfjung). **/Update**
+**Update:** @Diggsey [points out](https://github.com/rust-lang/rfcs/pull/2349#issuecomment-379230538) that we can still have a `PinRefCell` with a method like `fn get_pin(self: Pin<PinRefCell<T>>) -> Pin<T>`, as long as the `PinRefCell` never gives out mutable references. So it turns out that combining interior mutability and pinning should work fine. Later, @glaebhoerl suggested we can even [combine `RefCell` and `PinRefCell` into one type if we dynamically track the pinning state](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281/11?u=ralfjung). **/Update**
## 4 Conclusion
Anyway, as usual, please [let me know what you think](https://internals.rust-lang.org/t/safe-intrusive-collections-with-pinning/7281)!
+**Update:** Years later, I finally realized that there still is a major problem with intrusive collections -- it is basically impossible to have a by-reference iterator!
+With the collection not actually owning the memory the elements are stored in, it is basically impossible to guarantee that during the iteration, elements do not get removed from the collection, which would invalidate the reference.
+However, for many use-cases (like an intrusive queue) it is sufficient to just support by-value operations such as "enqueue" and "dequeue" over such a collection, and those can be given an entirely safe interface.
+If iteration is required, then more advanced [techniques to control sharing](https://plv.mpi-sws.org/rustbelt/ghostcell/) seem to be needed. **/Update**
+
#### Footnotes
---
title: "Pointers Are Complicated, or: What's in a Byte?"
-categories: internship rust
+categories: internship rust programming
forum: https://internals.rust-lang.org/t/pointers-are-complicated-or-whats-in-a-byte/8045
---
---
title: '"What The Hardware Does" is not What Your Program Does: Uninitialized Memory'
-categories: rust research
+categories: rust research programming
forum: https://internals.rust-lang.org/t/what-the-hardware-does-is-not-what-your-program-does-uninitialized-memory/10561
---
}
fn main() {
- let x: u8 = unsafe { mem::uninitialized() };
+ let x: u8 = unsafe { mem::MaybeUninit::uninit().assume_init() };
assert!(always_returns_true(x));
}
{% endhighlight %}
+**Update (2022-11-17):** Switched to `MaybeUninit` to keep the example working in newer versions of Rust.
+
`always_returns_true` is a function that, clearly, will return `true` for any possible 8-bit unsigned integer.
After all, *every* possible value for `x` will be either less than 120, equal to 120, or bigger than 120.
A quick loop [confirms this](https://play.rust-lang.org/?version=stable&mode=release&edition=2018&gist=65b690fa3c1691e11d4d45955358cdbe).
-However, if you [run the example](https://play.rust-lang.org/?version=stable&mode=release&edition=2018&gist=812fe3c8655bfedcea37bb18bb70a945), you can see the assertion fail.[^godbolt]
+However, if you [run the example](https://play.rust-lang.org/?version=stable&mode=release&edition=2018&gist=c17d299cacd626c572def0c4262aed69), you can see the assertion fail.[^godbolt]
[^godbolt]: In case this changes with future Rust versions, [here is the same example on godbolt](https://godbolt.org/z/9G67hP); the `xor eax, eax` indicates that the function returns 0, aka `false`. And [here is a version for C++](https://godbolt.org/z/TWrvcq).
---
title: "Pointers Are Complicated II, or: We need better language specs"
-categories: rust research
+categories: rust research programming
forum: https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562
license: CC BY-SA 4.0
license-url: https://creativecommons.org/licenses/by-sa/4.0/
{% endhighlight %}
However, that transformation is actually incorrect.
If we imagine a caller using this function as `sum_up(INT_MAX, 1, 0)`, then this is a perfectly correct way to call `sum_up`: the loop is never entered, so the overflowing addition `INT_MAX+1` is never performed.
-However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen!
+However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen![^signed-int-overflow]
[^loop]: If you are a regular reader of my blog, you will recognize this as the same optimization that already played a crucial role in [a previous post of mine]({% post_url 2020-07-15-unused-data %}). Loop-invariant code motion is a great optimization to look at when considering corner cases of IR semantics.
+[^signed-int-overflow]: If you are coming here with a Rust mindset, imagine `i + j` was written as `i.unchecked_add(j)`.
+
One might be tempted to ignore this problem because the UB on integer overflow is a compiler-only concept; every target supported by the compiler will do the obvious thing and just produce an overflowing result.
However, there might be other compiler passes running after the optimization we are considering.
One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable` since UB code is "by definition" unreachable, and another pass might then just remove all our code since it is unreachable.
---
title: "Pointers Are Complicated III, or: Pointer-integer casts exposed"
-categories: rust research
+categories: rust research programming
license: CC BY-SA 4.0
license-url: https://creativecommons.org/licenses/by-sa/4.0/
reddit: /rust/comments/u1bbqn/pointers_are_complicated_iii_or_pointerinteger/
That means a cast is the only legal way to turn a pointer into an integer, and after the discussion above we got our casts covered.
A [first careful step](https://github.com/rust-lang/rust/pull/95547) has recently been taken on this journey; the `mem::transmute` documentation now cautions against using this function to turn pointers into integers.
+**Update (2022-09-14):** After a lot more discussion, the current model pursued by the Unsafe Code Guidelines WG is to say that pointer-to-integer transmutation is permitted, but just strips provenance without exposing it.
+That means the program with the casts replaced by transmutation is UB, because the `ptr` it ends up dereferencing has invalid provenance.
+However, the transmutation itself is not UB.
+Basically, pointer-to-integer transmutation is equivalent to [the `addr` method](https://doc.rust-lang.org/nightly/std/primitive.pointer.html#method.addr), with all its caveats -- in particular, transmuting a pointer to an integer and back is like calling `addr` and then calling [`ptr::invalid`](https://doc.rust-lang.org/nightly/std/ptr/fn.invalid.html).
+That is a *lossy* round-trip: it loses provenance information, making the resulting pointer invalid to dereference.
+It is lossy even if we use a regular integer-to-pointer cast (or `from_exposed_addr`) for the conversion back to a pointer, since the original provenance might never have been exposed.
+Compared to declaring the transmutation itself UB, this model has some nice properties that help compiler optimizations (such as removing unnecessary store-load round-trips). **/Update**
+
## A new hope for Rust
All in all, while the situation may be very complicated, I am actually more hopeful than ever that we can have both -- a precise memory model for Rust *and* all the optimizations we can hope for!
The three core pillars of this approach are:
- making pointer-integer casts "expose" the pointer's provenance,
- offering `ptr.addr()` to learn a pointer's address *without* exposing its provenance,
-- and disallowing pointer-integer transmutation.
+- and making pointer-integer transmutation round-trips lossy (such that the resulting pointer cannot be dereferenced).
Together, they imply that we can optimize "nice" code (that follows Strict Provenance, and does not "expose" or use integer-pointer casts) perfectly, without any risk of breaking code that does use pointer-integer round-trips.
In the easiest possible approach, the compiler can simply treat pointer-integer and integer-pointer casts as calls to some opaque external function.
This was a long post, but I hope you found it worth reading. :)
To summarize, my concrete calls for action in Rust are:
-- Code that uses pointer-integer transmutation should migrate to regular casts or `MaybeUninit` transmutation ASAP.
- I think we should declare pointer-integer transmutation Undefined Behavior and not accept such code as well-defined.
+- Code that uses pointer-integer transmutation round-trips should migrate to regular casts or `MaybeUninit` transmutation ASAP.
+ I think we should declare pointer-integer transmutation as "losing" provenance, so code that assumes a lossless transmutation round-trip has Undefined Behavior.
- Code that uses pointer-integer or integer-pointer *casts* might consider migrating to the Strict Provenance APIs.
You can do this even on stable with [this polyfill crate](https://crates.io/crates/sptr).
However, such code *is and remains* well-defined. It just might not be optimized as well as one could hope, it might not compile on CHERI, and Miri will probably miss some bugs.
This would entirely lose the benefit I discussed above of making pointer-integer round-trips a *local* concern -- if these round-trips produce new, never-before-seen kinds of provenance, then the entire rest of the memory model has to define how it deals with those provenances.
We already have no choice but treat pointer-integer casts as an operation with side-effects; let's just do the same with integer-pointer casts and remain sure that no matter what the aliasing rules are, they will work fine even in the presence of pointer-integer round-trips.
+That said, under this model integer-pointer casts still have no side-effect, in the sense that just removing them (if their result is unused) is fine.
+Hence, it *could* make sense to implicitly perform integer-pointer casts in some situations, like when an integer value (without provenance) is used in a pointer operation (due to an integer-to-pointer transmutation).
+This breaks some optimizations like load fusion (turning two loads into one assumes the same provenance was picked both times), but most optimizations (in particular dead code elimination) are unaffected.
+
#### What about LLVM?
I discussed above how my vision for Rust relates to the direction C is moving towards.
--- /dev/null
+---
+title: "The last two years in Miri"
+categories: rust
+reddit: /rust/comments/vq3mmu/the_last_two_years_in_miri/
+---
+
+It has been [almost two years]({% post_url 2020-09-28-miri %}) since my last Miri status update.
+A lot has happened in the mean time that I would like to tell you all about!
+If you are using Miri, you might also be seeing new errors in code that previously worked fine; read on for more details on that.
+
+For the uninitiated, [Miri](https://github.com/rust-lang/miri/) is an interpreter that runs your Rust code and checks if it triggers any [Undefined Behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html) (UB for short).
+You can think of it a as very thorough (and very slow) version of valgrind/ASan/TSan/UBSan:
+Miri will detect when your program uses uninitialized memory incorrectly, performs out-of-bounds memory accesses or pointer arithmetic, causes a data race, violates key language invariants, does not ensure proper pointer alignment, or causes incorrect aliasing.
+As such, it is most helpful when writing unsafe code, as it aids in ensuring that you follow all the rules required for unsafe code to be correct and safe.
+Miri also detects memory leaks, i.e., it informs you at the end of program execution if there is any memory that was not deallocated properly.
+
+<!-- MORE -->
+
+Moreover, Miri is able to run code for other targets: for example, you might be developing code on x86_64, a 64-bit little-endian architecture.
+When you do low-level bit manipulation, it is easy to introduce bugs that only show up on 32-bit systems or big-endian architectures.
+You can run Miri with `--target i686-unknown-linux-gnu` and `--target mips64-unknown-linux-gnuabi64` to test your code in those situations -- and this will work even if your host OS is macOS or Windows!
+
+That said, it's not all roses and rainbows.
+Since Miri just knows how to interpret Rust code, it will get stuck when you call into C code.
+Miri knows how to execute a certain small set of well-known C functions (e.g. to access environment variables or open files), but it is still easy to run into an "unsupported operation" error due to missing C library implementations.
+In many cases you should be able to still write tests that cover the remaining code that does not need to, for example, directly access the network;
+but I also hope that Miri will keep growing its support for key platform APIs.
+
+## Miri progress
+
+So, what progress has Miri made in the last two years?
+
+### Concurrency
+
+The story of concurrency in Miri continues to surprise me: I had not even planned for Miri to support concurrency, but people just keep showing up and implement one part of it after the other, so now we have pretty good support for finding concurrency bugs!
+
+In that spirit, @JCTyblaidd implemented a data race detector.
+So if your code does not use appropriate atomic operations to make sure all accesses are suitably synchronized, Miri will now detect that problem and report Undefined Behavior.
+[Here's a demo](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=2dc29d339658dd2e1e74b84fcffc3926).
+(Click that link and then select "Tools - Miri" to see this in action.)
+Our data race error reports could be improved a lot (in particular they only show one of the two conflicting accesses involved in a data race), but they are still useful and have already found several data races in the wild.
+
+@thomcc changed our `compare_exchange_weak` implementation so that it randomly just fails with 80% probability.
+(The exact rate is adjustable via `-Zmiri-compared-exchange-weak-failure-rate=<x>`.)
+[Here's a demo](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0af8443b760985ce01640135ffb83749).
+This is super useful to find issues where code uses `compare_exchange_weak` but cannot handle spurious failures, since those are very unlikely to occur in the wild.
+
+@henryboisdequin added support for the atomic `fetch_min` and `fetch_max` operations, completing our support of the `Atomic*` types.
+
+And finally, @cbeuw showed up and added "weak memory emulation".
+This means that when you do an atomic load, you might not observe the latest value written to that location; instead, a previous value can be returned.
+[Here's a demo](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=7809a750bda54f0cc458b81823c79db7).
+This happens on real hardware, so having this supported in Miri helps to find more potential bugs.
+The caveat is that Miri still cannot produce *all* the behaviors that the actual program might exhibit.
+Also, the C++20 revision of the C++ memory model disallowed some possible behaviors that were previously allowed, but Miri might produce those behaviors -- there is currently no known algorithm that would prevent that.
+This should be very rare though.
+
+I then just put the icing on the cake by fixing some long-standing issues in our scheduler, so that it no longer gets stuck in spin loops.
+Miri now has a chance to preempt the running thread at the end of each basic block; the preemption probability is 1% but you can adjust it (using `-Zmiri-preemption-rate=<x>`).
+
+All of this made our concurrency support sufficiently solid that it no longer shows any warning about being "experimental".
+For example, it has already found a [data race in the standard library](https://github.com/rust-lang/rust/issues/98498).
+I can barely express how happy and proud I am that I had to do basically none of this work. :)
+
+One warning though: several of the improvements mentioned above rely on doing random choices.
+So, it is now more likely than before that Miri will work fine one day, and then show an error after some seemingly inconsequential change to the program the next day.
+I will get back to these problems later.
+
+### Pointer provenance and Stacked Borrows
+
+One of the most subtle aspects of Miri is [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md).
+The aliasing model is already quite complicated, and actually debugging what happens when Miri finds an aliasing violation in your code can be pretty tricky.
+However, @saethlin made this a lot easier!
+The error messages now show a lot more detail and point to several relevant locations in the code: not only where the bad access happened, but also where the pointer tag used for that access was created, and where that tag was invalidated.
+I am very impressed by how good some of these errors are, just [check this out](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=e831ed0f262e039dda4d24c159a9f5b0).
+
+Another big thing that happened recently is the entire ["Strict Provenance" story](https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance).
+I am super excited by these developments, because they offer the chance to fix some long-standing open problems in Miri:
+the issues with "untagged" raw pointers in Stacked Borrows, and Miri not properly supporting integer-to-pointer casts.
+
+After a lot of work by @carbotaniuman and myself, the situation now is as follows:
+- Miri always properly tags raw pointers.
+ So there are no longer any counter-intuitive behaviors caused by Miri "mixing up" two raw pointers that point to the same address, but were computed in a different way.
+ (We had a `-Zmiri-tag-raw-pointers` flag for a while that also achieves this; that flag is now on-by-default.)
+- If you do not use any integer-to-pointer casts, then you can stop reading here!
+ You can pass `-Zmiri-strict-provenance` to Miri to ensure that this is indeed the case.
+- If you *are* using integer-to-pointer casts, then Miri will warn about that. You now have two options.
+ - The ideal solution is to avoid using integer-to-pointer casts, and to follow Strict Provenance instead.
+ The [pointer library docs](https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance) explain in more detail what exactly that means.
+ Note that the APIs described there are still unstable, but a [polyfill](https://crates.io/crates/sptr) is available for stable Rust.
+ Also see [Gankra's blog post](https://gankra.github.io/blah/tower-of-weakenings/) and [my own blog post]({% post_url 2022-04-11-provenance-exposed %}) for some more background on this subject.
+ - If the casts are in code you do not control, or if you cannot currently avoid integer-to-pointer casts, you can pass `-Zmiri-permissive-provenance` to Miri to silence the warning.
+ Know that this means that Miri might miss some bugs in your code:
+ integer-to-pointer casts make it impossible to precisely track which pointer came from where, so Miri will conservatively accept some code that actually should be rejected.
+
+This is overall much better than previously -- there is nothing funky going on with raw pointers any more, and we should never incorrectly report UB any more even when integer-to-pointer casts are used.
+:-)
+
+### Other areas
+
+Concurrency and pointer aliasing are the two big changes, but there is also a long tail of smaller changes that together make Miri a hack of a lot more useful than it used to be:
+
+- @teryror made Miri support doctests, so now `cargo miri test` will also check your doctests for UB!
+- @Smittyvb fixed our fast-math intrinsics to properly report UB when they are used on non-finite values.
+- @hyd-dev added "symbol resolution" support to Miri, so if one part of your Rust code defines a function with a given `link_name`, and another piece of Rust code imports that function via an `extern` block, Miri now knows how to find the right function implementation.
+- @atsmtat added a `-Zmiri-isolation-error=<action>` flag so when a function call is rejected due to isolation, evaluation can continue by reporting an error code to the interpreted program.
+- @landaire added `-Zmiri-panic-on-unsupported`, which makes Miri raise a panic rather than stopping evaluation when an unsupported system function is encountered.
+This can be useful to keep going with the next test in a test suite.
+However, it also raises panics where usually that would be impossible, which can lead to surprising behavior.
+- @DrMeepster added support for running programs that use the `#[start]` attribute, and @oli-obk made that work even for targets without `libstd`.
+(You need to set `MIRI_NO_STD=1` to make the latter work.)
+- @DrMeepster also implemented support for the `#[global_allocator]` attribute.
+- @camelid made Miri optionally detect UB due to uninitialized integers, which has since become the default.
+- @saethlin made our errors more readable by pruning irrelevant details from the backtraces.
+- I have implemented support for calling methods on types like `Pin<Box<dyn Trait>>`.
+- @oli-obk fixed our handling of types like `MaybeUninit<u64>`, where previously we did not properly support only *some* of the bytes being initialized.
+
+We also improved out platform API and intrinsic support:
+
+- Thanks to @m-ou-se Miri now supports the Linux futex APIs used by the Rust standard library.
+ This was crucial for std's `park()` and `unpark()`, but meanwhile is also used for many other synchronization primitives.
+- On the file system side, @Aaron1011 implemented `readlink`, which makes `std::fs::read_link` work on Linux and macOS.
+- @asquared31415 made the three-argument form of `open` work.
+- @tavianator implemented `readdir64` so we can still list directories on Linux (the Rust standard library was changed to use that function rather than `readdir64_r`).
+- @Aaron1011 has also improved the rendering of panic backtraces inside the interpreter.
+- @frewsxcv implemented the missing bits to make the aarch64-apple-darwin target work in Miri.
+- I implemented the intrinsics required by `std::simd`, so portable-simd code should work with Miri.
+ It will not be very fast, though...
+- @V0ldek made our Windows `GetSystemInfo` shim work in more situations.
+- @saethlin added support for `*_COARSE` clocks on Linux.
+- @InfRandomness has started on getting Miri to work on FreeBSD targets (but this support is still incomplete).
+
+### Bugfixes and cleanup
+
+And of course there were tons of bugfixes.
+I want to particularly call out @hyd-dev who fixed a *lot* of issues in our `cargo miri` frontend.
+@dtolnay did a lot of code cleanup, making Miri pass by clippy's critical eyes and ensuring all our tests are properly formatted.
+And last not least, @oli-obk completely re-wrote our test suite so that we can finally actually test the full output of Miri.
+
+I have probably forgotten to mention something interesting as well.
+[See here](https://github.com/rust-lang/miri/graphs/contributors?from=2020-09-29&to=2022-07-02&type=c) for the full list of amazing people who contributed to Miri since my last update.
+I cannot thank all of you enough! <3
+
+## Help, Miri suddenly says my code is broken
+
+Several of the changes mentioned above, in particular with regards to concurrency and Stacked Borrows, mean that Miri is now able to detect more problems than before.
+On the one hand, that's of course great, but on the other hand, it can mean that when you re-test Miri on some code that seemed fine, it might suddenly complain!
+And because of all the non-determinism, it might also be the case that Miri *sometimes* complains, and sometimes doesn't (or that it works fine locally but complains on CI).
+What can you do when that happens?
+
+If Miri shows a new Stacked Borrows error, then that is probably caused by raw pointers now being properly tagged.
+The new Stacked Borrows messages should make it easier than before to diagnose these problems, but in the end this still remains a case-by-case issue.
+For example, [this program](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=14ddec169895d111578ec96757df95d1) will print:
+```
+error: Undefined Behavior: attempting a read access using <3255> at alloc1770[0x4], but that tag does not exist in the borrow stack for this location
+ --> src/main.rs:4:25
+ |
+4 | let _val = unsafe { *ptr.add(1) }; // ...and use it to access the *second* element.
+ | ^^^^^^^^^^^
+ | |
+ | attempting a read access using <3255> at alloc1770[0x4], but that tag does not exist in the borrow stack for this location
+ | this error occurs as part of an access at alloc1770[0x4..0x8]
+ |
+ = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
+ = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
+help: <3255> was created by a retag at offsets [0x0..0x4]
+ --> src/main.rs:3:15
+ |
+3 | let ptr = &x[0] as *const i32; // We create a pointer to the *first* element...
+ | ^^^^^
+ = note: backtrace:
+ = note: inside `main` at src/main.rs:4:25
+```
+In this case, the clue is in the offsets: note that the tag was created for offsets `[0x0..0x4]` (as usual in Rust, this *excludes* `0x4`), and the access was at `alloc1770[0x4]`.
+The pointer was thus used outside the offset range for which its tag (`<3255>`) is valid.
+The fix is to use `x.as_ptr()` rather than `&x[0] as *const i32` to get a pointer that is valid for the entire array.
+
+If the error only shows up sometimes, then it probably has something to do with concurrency.
+Miri is not *truly* random, but uses a pseudo-random number generator to make all concurrency-related choices (such as when to schedule another thread).
+This means you can explore various different possible choices by passing different *seeds* for Miri to use for its pseudo-random number generator.
+The following little shell snippet will run Miri with many different seeds, which is great to be able to locally reproduce a failure that you saw on CI, but that you are having trouble reproducing:
+```
+for SEED in $({ echo obase=16; seq 0 255; } | bc); do
+ echo "Trying seed: $SEED"
+ MIRIFLAGS=-Zmiri-seed=$SEED cargo miri test || { echo "Failing seed: $SEED"; break; };
+done
+```
+It is important that you use exactly the same `MIRIFLAGS` as CI to ensure the failure can even happen!
+It is also a good idea to use a filter with `cargo miri test FILTER` to ensure only the test you care about is being run.
+
+Once you confirmed that this is indeed a non-deterministic test failure, you can narrow it down further by reducing Miri's non-determinism:
+- You can pass `-Zmiri-preemption-rate=0` to make the scheduler non-preemptive (only schedule to other threads when a thread explicitly yields).
+ This *can* lead to infinite loops if there are spin-loops that do not yield, but if it makes the problem go away, then the problem needs some very particular scheduling decisions to surface, which might help you track down its source.
+- You can also pass `-Zmiri-disable-weak-memory-emulation` which has the effect of making atomic loads always return the latest value stored in that location.
+ If that makes the problem go away, then the issue is likely caused by insufficient synchronization somewhere. It might be a missing fence, or a `Relaxed` access that should be `Release`/`Acquire`.
+- Finally, `-Zmiri-compare-exchange-weak-failure-rate=0` makes `compared_exchange_weak` behave exactly like `compare_exchange`.
+ If that makes the problem go away, then some code using `compared_exchange_weak` is not properly handling spurious failures.
+
+Passing all of these flags will make Miri's concurrency entirely deterministic.
+That can be useful to avoid non-deterministic test failures, but note that this will also mask many real-world bugs.
+Those test failures are often real, even if they can be hard to track down!
+
+If you are still having trouble, feel free to come visit us in our [Zulip stream](https://rust-lang.zulipchat.com/#narrow/stream/269128-miri), which is the official communication channel for Miri.
+
+By the way, if you are still disabling some tests on Miri because Miri used to not support panics/concurrency, it's time to give those tests another try. :)
+So this is a good opportunity to go over your `cfg(miri)` and similar attributes and re-evaluate if they are still needed.
+
+## Using Miri
+
+If this post made you curious and you want to give Miri a try, here's how to do that.
+Assuming you have a crate with some unsafe code, and you already have a test suite (you are testing your unsafe code, right?), you can just install Miri (`rustup +nightly component add miri`) and then run `cargo +nightly miri test` to execute all tests in Miri.
+Note that this requires the nightly toolchain as Miri is still an experimental tool.
+
+Miri is very slow, so it is likely that some tests will take way too long to be feasible.
+You can adjust iteration counts in Miri without affecting non-Miri testing as follows:
+{% highlight rust %}
+let limit = if cfg!(miri) { 10 } else { 10_000 };
+{% endhighlight %}
+If your test suite needs to access OS facilities such as timers or the file system, set `MIRIFLAGS=-Zmiri-disable-isolation` to enable those.
+(Miri will tell you when that is necessary.)
+If your test suite runs into an unsupported operation, please [report an issue](https://github.com/rust-lang/miri/issues).
+However, note that we can only really support sufficiently "generic" operations -- like accessing file systems and network sockets.
+To implement things like `Py_IsInitialized` would mean putting a Python interpreter into Miri; that is not going to happen. ;)
+
+If you want to add Miri to your CI to ensure your test suite keeps working in Miri, please consult our [README](https://github.com/rust-lang/miri/#running-miri-on-ci).
+That document is also a great starting point for any other questions you might have.
+
+Miri is also integrated into the [Rust Playground](https://play.rust-lang.org/): you can select Miri in the "Tools" menu to check the code for Undefined Behavior.
+
+If Miri complains about your code and you do not understand why, we are happy to help!
+The best place to ask for support is our [Zulip stream](https://rust-lang.zulipchat.com/#narrow/stream/269128-miri).
+Questions are much easier to answer if you manage to reproduce the problem in a small self-contained bit of example code (ideally on the playground), but feel free to ask even if you do not know how to reduce the problem.
+
+## Helping Miri
+
+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 ones that are particularly suited for getting started are marked with a green label, but notice that even "E-easy" issues can require some amount of Rust experience -- Miri is not a good codebase for your first steps in Rust.
+Another good starting point is to try to implement the missing bit of functionality that keeps your test suite from working.
+If you need any mentoring, just [get in touch](https://rust-lang.zulipchat.com/#narrow/stream/269128-miri). :)
+
+That's it for now.
+I am totally blown away by how many people (and companies!) are already using and even contributing to Miri.
+This endeavor of re-shaping the way we approach correctness of unsafe code has been way more successful than my wildest dreams.
+I hope Miri can also help you to ensure correctness of your unsafe code, and I am excited for what the next year(s) of Miri development will bring. :D
--- /dev/null
+---
+title: "Announcing: MiniRust"
+categories: rust research
+reddit: /rust/comments/wiwjch/announcing_minirust/
+---
+
+I have been thinking about the semantics of Rust -- as in, the intended behavior of Rust programs when executed, in particular those containing unsafe code -- a lot.
+Probably too much.
+But all of these thoughts are just in my head, which is not very useful when someone else wants to try and figure out how some tricky bit of unsafe Rust code behaves.
+As part of the [Unsafe Code Guidelines](https://github.com/rust-lang/unsafe-code-guidelines/) project, we often get questions asking whether a *concrete* piece of code is fine or whether it has Undefined Behavior.
+But clearly, that doesn't scale: there are just too many questions to be asked, and figuring out the semantics by interacting with an oracle with many-day latency is rather frustrating.
+We have [Miri](https://github.com/rust-lang/miri/), which is a much quicker oracle, but it's also not always right and even then, it can just answer questions of the form "is this particular program fine"; users have to do all the work of figuring out the model that *generates* those answers themselves.
+
+<!-- MORE -->
+
+So I have promised for a long time to find some more holistic way to write down my thoughts on unsafe Rust semantics.
+I thought I could do it in 2021, but I, uh, "slightly" missed that deadline... but better late than never!
+At long last, I can finally present to you: [**MiniRust**](https://github.com/RalfJung/minirust).[^name]
+
+[^name]: I am beginning to wonder if this name was a bad choice. Naming is not my strong suit. Maybe "CoreRust" would have been better? Alas...
+
+The purpose of MiniRust is to describe the semantics of an interesting fragment of Rust in a way that is both precise and understandable to as many people as possible.
+These goals are somewhat at odds with each other -- the most precise definitions, e.g. carried out in the Coq Proof Assistant, tend to not be very accessible.
+English language, on the other hand, is not very precise.
+So my compromise solution is to write down the semantics in a format that is hopefully known to everyone who could be interested: in Rust code.
+Specifically, MiniRust is specified by a *reference interpreter* that describes the step-by-step process of executing a MiniRust program, *including* checking at each step whether the program has Undefined Behavior.
+
+"Hold on", I hear a [Cool Bear](https://fasterthanli.me/articles/) say, "you are defining Rust in Rust code? Isn't that cyclic?"[^bear]
+Well, yes and no. It's not *really* Rust code.
+It's what I call "pseudo Rust", uses only a tiny fragment of the language (in particular, no `unsafe`), and then extends the language with some conveniences to make things less verbose.
+The idea is that anyone who knows Rust should immediately be able to understand what this code means, but also hopefully eventually if this idea pans out we can have tooling to translate pseudo Rust into "real" languages -- in particular, real Rust and Coq.
+Translating it to real Rust means we can actually execute the reference interpreter and test it, and translating it to Coq means we can start proving theorems about it.
+But I am getting waaaay ahead of myself, these are rather long-term plans.
+
+[^bear]: Thanks to fasterthanlime for facilitating the bear's appearance on this blog.
+
+**Update (2023-02-13):** "Pseudo Rust" has now been renamed to "specr lang", the language of the work-in-progress "specr" tool that can translate specr lang into Rust code to make specifications executable. **/Update**
+
+So, if you want to look into my brain to see how I see Rust programs, then please go check out [MiniRust](https://github.com/RalfJung/minirust).
+The README explains the scope and goals, the general structure, and the details of ~~pseudo Rust~~ specr lang, as well as a comparison with some related efforts.
+
+In particular I find that the concept of "places" and "values", which can be rather mysterious, becomes a lot clearer when spelled out like that, but that might just be me.
+I hasten to add that this is *very early work-in-progress*, and it is *my own personal experiment*, not necessarily reflecting the views of anyone else.
+It is also *far from feature-complete*, in fact it has just barely enough to be interesting.
+There are lots of small things missing (like integers that aren't exactly 2 bytes in size, or tuples that don't have exactly 2 elements), but the biggest omission by far is the total lack of an aliasing model.
+And unsized types. And concurrency. And probably other things.
+
+On the other hand, there are many things that it *can* explain in full precision:
+- validity invariants, and how they arise from the mapping between a high-level concept of "values" and a low-level concept of "sequences of bytes"
+- the basic idea of provenance tracking the "allocation" a pointer points to, and how that interacts with pointer arithmetic (including `offset` and `wrapping_offset`)
+- how pointer provenance behaves when doing transmutation between pointers and integers
+- what happens when *casting* between pointers and integers
+- padding (that's why tuples can have 2 elements, so there can be padding between them)
+
+If you are not used to reading interpreter source code, then I guess this can be rather jarring, and there is certainly a *lot* of work that could and should be done to make this more accessible.
+(Like, examples. I hear people like examples.)
+But just being able to talk about these questions with precision *at all* has already lead to some interesting discussions in the UCG WG, some of which made me change my mind -- thanks in particular to @digama0, @JakobDegen, and @alercah for engaging deeply with my ideas.
+So for now it is serving its purpose, and maybe some of you can find it useful, too.
+Hopefully we can even use this as a starting place for seriously tackling the issue of an *official* specification of Rust.
+More on that soon. :)
--- /dev/null
+---
+title: "A New Beginning"
+categories: research rust
+---
+
+I have some very exciting news to share: starting November 1st, I will work at ETH Zürich as an assistant professor!
+Becoming a professor in the first place is a dream come true, and becoming a professor at a place like ETH Zürich is not something I even dared to dream of.
+I still cannot quite believe that this is actually happening (I will be *professor*?!??), but [the news is out](https://twitter.com/CSatETH/status/1548944615285350400) so I guess this is real. :D
+
+<!-- MORE -->
+
+I feel excited and terrified in about equal parts.
+Excited by all the new possibilities, by the prospect of working with students and inspiring the next generation of researchers;
+terrified by all the responsibility and the prospect of having to stand in a classroom and give a lecture in only a few months' time.
+But somehow everyone else seems confident that I can do this, so I guess I'll just play along and hope that I will not prove them wrong...
+
+I am also humbled and eternally thankful for being given this opportunity.
+Being able to work in an environment like ETH is a privilege beyond imagination, and I don't know how I got so lucky.
+I probably used up all my Karma points for the rest of my life, and will do my best to honor this privilege.
+I feel hugely indebted to everyone I worked with, first and foremost of course my PhD advisor [Derek Dreyer](https://people.mpi-sws.org/~dreyer/).
+But I would also like to specifically call out the Rust community, because I don't think this would have happened without Rust -- thanks to *everyone* who contributed to this language that I am essentially building my career on[^rust], and thanks in particular to everyone who indulged in my ideas for how Rust should approach unsafe code and helped me shape that corner of the language.
+
+[^rust]: Before anyone gets worried, I also have some [ideas](https://iris-project.org/) I want to pursue that are unrelated to Rust. But Rust is currently by far the biggest inspiration for new research problems for me, and without Rust I don't think my research would be anywhere near as applied and impactful as it is today, which I am sure played a key role in the decision of ETH to hire me.
+
+So what's next?
+I will soon finish my post-doc at MIT and move back to Europe, and then move to Zürich in October.
+And then I will have to figure out how this being-a-professor thing works. ;)
+My first main priority is building a research group: the "Programming Language Foundations Lab"[^lab].
+So if you are interested in doing a PhD or post-doc working on, well, programming language foundations, and in particular formal foundations for Rust, or if you are an ETH student interested in a Master Thesis in that area -- please [reach out](https://research.ralfj.de/contact.html)!
+I am still figuring out how to do things like hiring people and finding suitable projects, but there is no shortage of open problems that need solving and theorems that need proving. :)
+
+[^lab]: Yes, I have a lab coat. I don't usually wear it though... and if you want to see me wear it, that will cost you some beer.
--- /dev/null
+---
+title: "cargo careful: run your Rust code with extra careful debug checking"
+categories: rust
+reddit: /rust/comments/xogayv/cargo_careful_run_your_rust_code_with_extra/
+---
+
+Did you know that the standard library is full of useful checks that users never get to see?
+There are plenty of debug assertions in the standard library that will do things like check that `char::from_u32_unchecked` is called on a valid `char`, that `CStr::from_bytes_with_nul_unchecked` does not have internal nul bytes, or that pointer functions such as `copy` or `copy_nonoverlapping` are called on suitably aligned non-null (and non-overlapping) pointers.
+However, the regular standard library that is distributed by rustup is compiled without debug assertions, so there is no easy way for users to benefit from all this extra checking.
+
+<!-- MORE -->
+
+[`cargo careful`](https://github.com/RalfJung/cargo-careful) is here to close this gap:
+when invoked the first time, it builds a standard library with debug assertions from source, and then runs your program or test suite with that standard library.
+Installing `cargo careful` is as easy as `cargo install cargo-careful`, and then you can do `cargo +nightly careful run`/`cargo +nightly careful test` to execute your binary crates and test suites with an extra amount of debug checking.
+
+This will naturally be slower than a regular debug or release build, but it is *much* faster than executing your program in [Miri](https://github.com/rust-lang/miri) and still helps find some Undefined Behavior.
+Unlike Miri, it is fully FFI-compatible (though the code behind the FFI barrier is completely unchecked).
+Of course Miri is much more thorough and `cargo careful` will miss many problems (for instance, it cannot detect out-of-bounds pointer arithmetic -- but it *does* perform bounds checking on `get_unchecked` slice accesses).
+
+Note that for now, some of these checks (in particular for raw pointer methods) cause an abrupt abort of the program via SIGILL without a nice error message or backtrace.
+There are probably ways to improve this in the future.
+Meanwhile, if you have some `unsafe` code that for one reason or another you cannot test with Miri, give [`cargo careful`] a try and let me know how it is doing. :)
+
+[`cargo careful`]: https://github.com/RalfJung/cargo-careful
+
+*By the way, I am soon [starting as a professor at ETH Zürich]({% post_url 2022-08-16-eth %}), so if you are interested in working with me on programming language theory as a master student, PhD student, or post-doc, then please [reach out](https://research.ralfj.de/contact.html)!*
--- /dev/null
+---
+title: "From Stacks to Trees: A new aliasing model for Rust"
+categories: rust research
+reddit: /rust/comments/13y8a9b/from_stacks_to_trees_a_new_aliasing_model_for_rust/
+---
+
+Since last fall, [Neven](https://perso.crans.org/vanille/) has been doing an internship to develop a new aliasing model for Rust: Tree Borrows.
+Hang on a second, I hear you say -- doesn't Rust already have an aliasing model?
+Isn't there this "Stacked Borrows" that Ralf keeps talking about?
+Indeed there is, but Stacked Borrows is just one proposal for a possible aliasing model -- and it [has its problems](https://github.com/rust-lang/unsafe-code-guidelines/issues?q=is%3Aopen+is%3Aissue+label%3AA-stacked-borrows).
+The purpose of Tree Borrows is to take the lessons learned from Stacked Borrows to build a new model with fewer issues, and to take some different design decisions such that we get an idea of some of the trade-offs and fine-tuning we might do with these models before deciding on the official model for Rust.
+
+Neven has written a detailed introduction to Tree Borrows [on his blog](https://perso.crans.org/vanille/treebor/), which you should go read first.
+He presented this talk at a recent RFMIG meeting, so you can also [watch his talk here](https://www.youtube.com/watch?v=zQ76zLXesxA).
+In this post, I will focus on the differences to Stacked Borrows.
+I assume you already know Stacked Borrows and want to understand what changes with Tree Borrows and why.
+
+<!-- MORE -->
+
+As a short-hand, I will sometimes write SB for Stacked Borrows and TB for Tree Borrows.
+
+## Two-phase borrows
+
+The main novelty in Tree Borrows is that it comes with proper support for two-phase borrows.
+Two-phase borrows are a mechanism introduced with NLL which allows code like the following to be accepted:
+
+```rust
+fn two_phase(mut x: Vec<usize>) {
+ x.push(x.len());
+}
+```
+
+The reason this code is tricky is that it desugars to something like this:
+
+```rust
+fn two_phase(mut x: Vec<usize>) {
+ let arg0 = &mut x;
+ let arg1 = Vec::len(&x);
+ Vec::push(arg0, arg1);
+}
+```
+
+This code clearly violates the regular borrow checking rules since `x` is mutably borrowed to `arg0` when we call `x.len()`!
+And yet, the compiler will accept this code.
+The way this works is that the `&mut x` stored in `arg0` is split into two phases:
+in the *reservation* phase, `x` can still be read via other references.
+Only when we actually need to write to `arg0` (or call a function that might write to it) will the reference be "activated", and it is from that point onwards (until the end of the lifetime of the borrow) that no access via other references is allowed.
+For more details, see [the RFC](https://github.com/rust-lang/rfcs/blob/master/text/2025-nested-method-calls.md) and [the rustc-dev-guide chapter on two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html).
+The only point relevant for this blog post is that when borrowing happens implicitly for a method call (such as `x.push(...)`), Rust will treat this as a two-phase borrow.
+When you write `&mut` in your code, it is treated as a regular mutable reference without a "reservation" phase.
+
+For the aliasing model, two-phase borrows are a big problem: by the time `x.len()` gets executed, `arg0` already exists, and as a mutable reference it really isn't supposed to allow reads through other pointers.
+Therefore Stacked Borrows just [gives up](https://github.com/rust-lang/unsafe-code-guidelines/issues/85) here and basically treats two-phase borrows like raw pointers.
+That is of course unsatisfying, so for Tree Borrows we are adding proper support for two-phase borrows.
+What's more, we are treating *all* mutable references as two-phase borrows: this is more permissive than what the borrow checker accepts, but lets us treat mutable references entirely uniformly.
+(This is a point we might want to tweak, but as we will see soon this decision actually has some major unexpected benefits.)
+
+This is why we need a tree in the first place: `arg0` and the reference passed to `Vec::len` are both children of `x`.
+A stack is no longer sufficient to represent the parent-child relationships here.
+Once the use of a tree is established, modeling of two-phase borrows is fairly intuitive: they start out in a `Reserved` state which tolerates reads from other, unrelated pointers.
+Only when the reference (or one of its children) is written to for the first time, its state transitions to `Active` and now reads from other, unrelated pointers are not accepted any more.
+(See Neven's post for more details. In particular note that there is one unpleasant surprise lurking here: if there are `UnsafeCell` involved, then a reserved mutable reference actually has to tolerate *mutation* via unrelated pointers!
+In other words, the aliasing rules of `&mut T` are now affected by the presence of `UnsafeCell`. I don't think people realized this when two-phase borrows were introduced, but it also seems hard to avoid so even with hindsight, it is not clear what the alternative would have been.)
+
+## Delayed uniqueness of mutable references
+
+One of the most common source of Stacked Borrows issues is its [very eager enforcement of uniqueness of mutable references](https://github.com/rust-lang/unsafe-code-guidelines/issues/133).
+For example, the following code is illegal under Stacked Borrows:
+
+```rust
+let mut a = [0, 1];
+let from = a.as_ptr();
+let to = a.as_mut_ptr().add(1); // `from` gets invalidated here
+std::ptr::copy_nonoverlapping(from, to, 1);
+```
+
+The reason it is illegal is that `as_mut_ptr` takes `&mut self`, which asserts unique access to the entire array, therefore invalidating the previously created `from` pointer.
+In Tree Borrows, however, that `&mut self` is a two-phase borrow! `as_mut_ptr` does not actually perform any writes, so the reference remains reserved and never gets activated.
+That means the `from` pointer remains valid and the entire program is well-defined.
+The call to `as_mut_ptr` is treated like a read of `*self`, but `from` (and the shared reference it is derived from) are perfectly fine with reads via unrelated pointers.
+
+It happens to be the case that swapping the `from` and `to` lines actually makes this code work in Stacked Borrows.
+However, this is not for a good reason: this is a consequence of the rather not-stack-like rule in SB which says that on a read, we merely *disable all `Unique`* above the tag used for the access, but we keep raw pointers derived from those `Unique` pointers enabled.
+Basically, raw pointers can live longer than the mutable references they are derived from, which is highly non-intuitive and potentially problematic for program analyses.
+With TB, the swapped program is still fine, but for a different reason:
+when `to` gets created first, it remains a reserved two-phase borrow.
+This means that creating a shared reference and deriving `from` from it (which acts like a read on `self`) is fine; reserved two-phase borrows tolerate reads via unrelated pointers.
+Only when `to` is written to does it (or rather the `&mut self` it was created from) become an active mutable reference that requires uniqueness, but that is after `as_ptr` returns so there is no conflicting `&self` reference.
+
+It turns out that consistently using two-phase borrows lets us entirely eliminate this hacky SB rule and also fix one of the most common sources of UB under SB.
+I didn't expect this at all, so this is a happy little accident. :)
+
+However, note that the following program is fine under SB but invalid under TB:
+
+```rust
+let mut a = [0, 1];
+let to = a.as_mut_ptr().add(1);
+to.write(0);
+let from = a.as_ptr();
+std::ptr::copy_nonoverlapping(from, to, 1);
+```
+
+Here, the write to `to` activates the two-phase borrow, so uniqueness is enforced.
+That means the `&self` created for `as_ptr` (which is considered reading all of `self`) is incompatible with `to`, and so `to` is invalidated (well, it is made read-only) when `from` gets created.
+So far, we do not have evidence that this pattern is common in the wild.
+The way to avoid issues like the code above is to *set up all your raw pointers before you start doing anything*.
+Under TB, calling reference-receiving methods like `as_ptr` and `as_mut_ptr` and using the raw pointers they return on disjoint locations is fine even if these references overlap, but you must call all those methods before the first write to a raw pointer.
+Once the first write happens, creating more references can cause aliasing violations.
+
+## No strict confinement of the accessible memory range
+
+The other major source of trouble with Stacked Borrows is [restricting raw pointers to the type and mutability they are initially created with](https://github.com/rust-lang/unsafe-code-guidelines/issues/134).
+Under SB, when a reference is cast to `*mut T`, the resulting raw pointer is confined to access only the memory covered by `T`.
+This regularly trips people up when they take a raw pointer to one element of an array (or one field of a struct) and then use pointer arithmetic to access neighboring elements.
+Moreover, when a reference is cast to `*const T`, it is actually read-only, even if the reference was mutable!
+Many people expect `*const` vs `*mut` not to matter for aliasing, so this is a regular source of confusion.
+
+Under TB, we resolve this by no longer doing any retagging for reference-to-raw-pointer casts.
+A raw pointer simply uses the same tag as the parent reference it is derived from, thereby inheriting its mutability and the range of addresses it can access.
+Moreover, references are not strictly confined to the memory range described by their type:
+when an `&mut T` (or `&T`) gets created from a parent pointer, we initially record the new reference to be allowed to access the memory range describe by `T` (and we consider this a read access for that memory range).
+However, we also perform *lazy initialization*: when a memory location outside this initial range is accessed, we check if the parent pointer would have had access to that location, and if so then we also give the child the same access.
+This is repeated recursively until we find a parent that has sufficient access, or we reach the root of the tree.
+
+This means TB is compatible with [`container_of`-style pointer arithmetic](https://github.com/rust-lang/unsafe-code-guidelines/issues/243) and [`extern` types](https://github.com/rust-lang/unsafe-code-guidelines/issues/276), overcoming two more SB limitations.
+
+This also means that the following code becomes legal under TB:
+
+```rust
+let mut x = 0;
+let ptr = std::ptr::addr_of_mut!(x);
+x = 1;
+ptr.read();
+```
+
+Under SB, `ptr` and direct access to the local `x` used two different tags, so writing to the local invalidated all pointers to it.
+Under TB, this is no longer the case; a raw pointer directly created to the local is allowed to alias arbitrarily with direct accesses to the local.
+
+Arguably the TB behavior is more intuitive, but it means we can no longer use writes to local variables as a signal that all possible aliases have been invalidated.
+However, note that TB only allows this if there is an `addr_of_mut` (or `addr_of`) immediately in the body of a function!
+If a reference `&mut x` is created, and then some other function derives a raw pointer from that, those raw pointers *do* get invalidated on the next write to `x`.
+So to me this is a perfect compromise: code that uses raw pointers has a lower risk of UB, but code that does not use raw pointers (which is easy to see syntactically) can be optimized as much as with SB.
+
+Note that this entire approach in TB relies on TB *not* needing the stack-violating hack mentioned in the previous section.
+If raw pointers in SB just inherited their parent tag, then they would get invalidated together with the unique pointer they are derived from, disallowing all the code that this hack was specifically added to support.
+This means that backporting these improvements to SB is unlikely to be possible.
+
+## `UnsafeCell`
+
+The handling of `UnsafeCell` also changed quite a bit with TB.
+First of all, another [major issue](https://github.com/rust-lang/unsafe-code-guidelines/issues/303) with SB was fixed: turning an `&i32` into an `&Cell<i32>` *and then never writing to it* is finally allowed.
+This falls out of how TB handles the aliasing allowed with `UnsafeCell`: they are treated like casts to raw pointers, so reborrowing an `&Cell<i32>` just inherits the tag (and therefore the permissions) of the parent pointer.
+
+More controversially, TB also changes how precisely things become read-only when an `&T` involves `UnsafeCell` somewhere inside `T`.
+In particular, for `&(i32, Cell<i32>)`, TB allows mutating *both* fields, including the first field which is a regular `i32`, since it just treats the entire reference as "this allows aliasing".[^1]
+In contrast, SB actually figured out that the first 4 bytes are read-only and only the last 4 bytes allow mutation via aliased pointers.
+
+[^1]: This does not mean that we bless such mutation! It just means that the compiler cannot use immutability of the first field for its optimizations. Basically, immutability of that field becomes a [safety invariant instead of a validity invariant]({% post_url 2018-08-22-two-kinds-of-invariants %}): when you call foreign code, you can still rely on it not mutating that field, but within the privacy of your own code you are allowed to mutate it. See [my response here](https://www.reddit.com/r/rust/comments/13y8a9b/comment/jmlvgun/) for some more background.
+
+The reason for this design decision is that the general philosophy with TB was to err on the side of allowing more code, having less UB (which is the opposite direction than what I used with SB).
+This is a deliberate choice to uncover as much of the design space as we can with these two models.
+Of course we wanted to make sure that TB still allows all the desired optimizations, and still has enough UB to justify the LLVM IR that rustc generates -- those were our "lower bounds" for the minimum amount of UB we need.
+And it turns out that under these constraints, we can support `UnsafeCell` with a fairly simple approach: for the aliasing rules of `&T`, there are only 2 cases.
+Either there is no `UnsafeCell` anywhere, then this reference is read-only, or else the reference allows aliasing.
+As someone who thinks a lot about proving theorems about the full Rust semantics including its aliasing model, this approach seemed pleasingly simple. :)
+
+I expected this decision to be somewhat controversial, but the amount of pushback we received has still been surprising.
+The good news is that this is far from set in stone: we can [change TB to treat `UnsafeCell` more like SB did](https://github.com/rust-lang/unsafe-code-guidelines/issues/403).
+Unlike the previously described differences, this one is entirely independent of our other design choices.
+While I prefer the TB approach, the way things currently stand, I do expect that we will end up with SB-like `UnsafeCell` treatment eventually.
+
+## What about optimizations?
+
+I have written a lot about how TB differs from SB in terms of which coding patterns are UB.
+But what about the other side of the coin, the optimizations?
+Clearly, since SB has more UB, we have to expect TB to allow fewer optimizations.
+And indeed there is a major class of optimizations that TB loses: speculative writes, i.e. inserting writes in code paths that would not previously have written to this location.
+This is a powerful optimization and I was quite happy that SB could pull it off, but it also comes at a major cost: mutable references have to be "immediately unique".
+Given how common of a problem "overeager uniqueness" is, my current inclination is that we most likely would rather make all that code legal than allow speculative writes.
+We still have extremely powerful optimization principles around reads, and when the code *does* perform a write that gives rise to even more optimizations, so my feeling is that insisting on speculative writes is just pushing things too far.
+
+On another front, TB actually allows a set of crucial optimizations that SB ruled out by accident: reordering of reads!
+The issue with SB is that if we start with "read mutable reference, then read shared reference", and then reorder to "read shared reference, then read mutable reference", then in the new program, reading the shared reference might invalidate the mutable reference -- so the reordering might have introduced UB!
+This optimization is possible without having any special aliasing model, so SB not allowing it is a rather embarrassing problem.
+If it weren't for the stack-violating hack that already came up several times above, I think there would be a fairly easy way of fixing this problem in SB, but alas, that hack is load-bearing and too much existing code is UB if we remove it.
+Meanwhile, TB does not need any such hack, so we can do the Right Thing (TM): when doing a read, unrelated mutable references are not entirely disabled, they are just made read-only.
+This means that "read shared reference, then read mutable reference" is equivalent to "read mutable reference, then read shared reference" and the optimization is saved.
+(A consequence of this is that retags can also be reordered with each other, since they also act as reads. Hence the order in which you set up various pointers cannot matter, until you do the first write access with one of them.)
+
+## Future possibility: `Unique`
+
+Tree Borrows paves the way for an extension that we have not yet implemented, but that I am quite excited to explore: giving meaning to `Unique`.
+`Unique` is a private type in the Rust standard library that was originally meant to express `noalias` requirements.
+However, it was never actually wired up to emit that attribute on the LLVM level.
+`Unique` is mainly used in two places in the standard library: `Box` and `Vec`.
+SB (and TB) treat `Box` special (matching rustc itself), but not `Unique`, so `Vec` does not come with any aliasing requirements.
+And indeed the SB approach totally does not work for `Vec`, since we don't actually know how much memory to make unique here.
+However, with TB we have lazy initialization, so we don't need to commit to a memory range upfront -- we can make it unique "when accessed".
+This means we can explore giving meaning to the `Unique` in `Vec`.
+
+Now, this might not actually work.
+People actually do blatantly-aliasing things with `Vec`, e.g. to implement arenas.
+On the other hand, `Vec`'s uniqueness would only come in when it is moved or passed *by value*, and only for the memory ranges that are actually being accessed.
+So it is quite possible that this is compatible with arenas.
+I think the best way to find out is to implement `Unique` semantics behind a flag and experiment.
+If that works out, we might even be able to remove all special handling of `Box` and rely on the fact that `Box` is defined as a newtype over `Unique`.
+This would slightly reduce the optimization potential (`Box<T>` is known to point to a memory range at least the size of `T`, whereas `Unique` has no such information), but making `Box` less magic is a long-standing quest so this might be an acceptable trade-off.
+
+I should note that there are many people who think neither `Box` nor `Vec` should have any aliasing requirements. I think it's worth first exploring whether we can have aliasing requirements which are sufficiently light-weight that they are compatible with common coding patterns, but even if we end up saying `Box` and `Vec` behave like raw pointers, it can still be useful to have `Unique` in our toolbox and expose it for unsafe code authors to eke out the last bits of performance.
+
+## Conclusion
+
+These are the major differences between Stacked Borrows and Tree Borrows.
+As you can see, almost all of them are cases where TB allows more code than SB, and indeed TB fixes what I consider to be SB's two biggest problems: overeager uniqueness for mutable references, and confining references and raw pointers to the size of the type they are created with.
+These are great news for unsafe code authors!
+
+What TB *doesn't* change is the presence of "protectors" to enforce that certain references remain valid for the duration of an entire function call (whether they are used again or not); protectors are absolutely required to justify the LLVM `noalias` annotations we would like to emit and they also do enable some stronger optimizations than what would otherwise be possible.
+I do expect protectors to be the main remaining source of unexpected UB from Tree Borrows, and I don't think there is a lot of wiggle-room that we have here, so this might just be a case where we have to tell programmers to adjust their code, and invest in documentation material to make this subtle issue as widely known as possible.
+
+Neven has implemented Tree Borrows in Miri, so you can play around with it and check your own code by setting `MIRIFLAGS=-Zmiri-tree-borrows`.
+If you run into any surprises or concerns, please let us know!
+The [t-opsem Zulip](https://rust-lang.zulipchat.com/#narrow/stream/136281-t-opsem) and the [UCG issue tracker](https://github.com/rust-lang/unsafe-code-guidelines/) are good places for such questions.
+
+That's all I got, thanks for reading -- and a shout out to Neven for doing all the actual work here (and for giving feedback on this blog post), supervising this project has been a lot of fun!
+Remember to read [his write up](https://perso.crans.org/vanille/treebor/) and [watch his talk](https://www.youtube.com/watch?v=zQ76zLXesxA).
--- /dev/null
+---
+title: "Talk about Undefined Behavior, unsafe Rust, and Miri"
+categories: rust
+---
+
+I recently gave a talk at a local Rust meetup in Zürich about Undefined Behavior, unsafe Rust, and Miri.
+The recording is available [here](https://www.youtube.com/watch?v=svR0p6fSUYY).
+It targets an audience that is familiar with Rust but not with the nasty details of unsafe code, so I hope many of you will enjoy it!
+Have fun. :)
--- /dev/null
+---
+title: "Google Open Source Peer Bonus"
+categories: rust
+---
+
+We are all used to spam emails, supposedly from Google, that say "You won" and I just need to send all my data to somewhere to receive my lottery payout.
+When I recently received an email about Google's "Open Source Peer Bonus" program, I almost discarded it as yet another version of that kind of spam.
+But it turns out sometimes these emails are real!
+Meanwhile the [official announcement](https://opensource.googleblog.com/2023/12/google-open-source-peer-bonus-program-announces-second-group-of-2023-winners.html) has been released which lists me as a recipient of this bonus as a thank you for my work on Rust.
+So this one time, it wasn't spam after all!
+
+<!-- MORE -->
+
+Thanks a lot to Google for this program at the $250 reward; it is great to see open source work honored this way.
+I have donated the amount in full to [noyb](https://noyb.eu/en), who I'm sure will be using it [for good](https://noyb.eu/en/noyb-win-first-major-fine-eu-1-million-using-google-analytics).
+
+**Update (2024-01-07):**
+In fact, this is already my second Google Open Source Peer Bonus.
+The first was in the [first half of 2023](https://opensource.googleblog.com/2023/05/google-open-source-peer-bonus-program-announces-first-group-of-winners-2023.html).
+Due to issues with the payment process, it took a while for that bonus to be transferred, but I can confirm that it has now arrived in my bank account.
+I will have to find a suitable non-for-profit to donate this to... or it might be noyb again, we will see.
+**/Update**
--- /dev/null
+---
+title: "Sandboxing All The Things with Flatpak and BubbleBox"
+categories: sysadmin
+---
+
+A few years ago, I have [blogged]({% post_url 2019-03-09-firejail %}) about my approach to sandboxing less-trusted applications that I have to or want to run on my main machine.
+The approach has changed since then, so it is time for an update.
+
+<!-- MORE -->
+
+Over time I grew increasingly frustrated with Firejail: configurations would frequently break on updates,
+and debugging Firejail profiles is extremely hard. When considering all the included files, we are talking
+about many hundred lines of configuration with a subtle interplay of allowlists and blocklists.
+Even when I knew which folder I wanted to give access to, it was often non-trivial to ensure that
+this access would actually be possible.
+
+Now I am instead using a combination of two different approaches: Flatpak and BubbleBox.
+
+## Flatpak
+
+The easiest sandbox to maintain is the sandbox maintained by someone else.
+So when a Flatpak exists for software I want to or have to use, such as Signal or Zoom, that is generally my preferred approach.
+
+Unfortunately, Flatpaks can come with extremely liberal default profiles that make the sandbox mostly pointless.
+The following global overrides help ensure that this does not happen:
+```
+[Context]
+sockets=!gpg-agent;!pcsc;!ssh-auth;!system-bus;!session-bus
+filesystems=~/.XCompose:ro;xdg-config/fontconfig:ro;!~/.gnupg;!~/.ssh;!xdg-documents;!home;!host
+
+[Session Bus Policy]
+org.freedesktop.Flatpak=none
+org.freedesktop.secrets=none
+```
+
+I also use [Flatseal], an amazing application that helps to check which permissions applications get, and change them if necessary.
+
+[Flatseal]: https://flathub.org/apps/com.github.tchx84.Flatseal
+
+## BubbleBox
+
+However, not all software exists as Flatpak.
+Also, sometimes I want software to run basically on my host system (i.e., to use the regular `/usr`), just without access to literally *everything* in my home directory.
+Examples of this are Factorio and VSCodium.
+The latter doesn't work in Flatpak as I want to use it with LaTeX, and realistically this means it needs to run the LaTeX installed via `apt`.
+The official recommendation is to effectively disable the Flatpak sandbox, but that entirely defeats the point, so I went looking for alternatives.
+
+[bubblewrap] provides a very convenient solution: it can start an application in its own private filesystem namespace with full control over which part of the host file system is accessible from inside the sandbox.
+I wrote a small wrapper around bubblewrap to make this configuration a bit more convenient to write and manage;
+this project is called [BubbleBox].
+This week-end I finally got around to adding support for [xdg-dbus-proxy] so that sandboxed applications can now access particular D-Bus functions without having access to the entire bus (which is in general not safe to expose to a sandboxed application).
+That means it's finally time to blog about this project, so here we go -- if you are interested, check out [BubbleBox];
+the project page explains how you can use it to set up your own sandboxing.[^1]
+
+[^1]: One day I should probably rewrite this in Rust... maybe this will be my test project for when [cargo-script](https://rust-lang.github.io/rfcs/3424-cargo-script.html) becomes available.
+
+I should also note that this is not the only bubblewrap-based sandboxing solution.
+[bubblejail] is fairly similar but provides a configuration GUI and a good set of default provides;
+it was a very useful resource when figuring out the right bubblewrap flags to make complex GUI applications work properly.
+(Incidentally, "bubblejail" is also how I called my own script originally, but then I realized that the name is already taken.)
+Joachim Breitner also recently [blogged](https://www.joachim-breitner.de/blog/812-Convenient_sandboxed_development_environment) about his own bubblewrap-based sandboxing script.
+sloonz has a similar [script](https://gist.github.com/sloonz/4b7f5f575a96b6fe338534dbc2480a5d) as well, with a nice yaml-based configuration format and [great explanations](https://sloonz.github.io/posts/sandboxing-1/) for what all the flags exactly do.
+Had their script existed when I started what eventually became BubbleBox, I would have used it as a starting point.
+But it was also fun to figure out my own solution.
+
+Using bubblewrap and xdg-dbus-proxy for this was an absolute joy.
+Both of these components came out of the Flatpak project, but the authors realized that they could be independently useful,
+so in best Unix tradition they turned them into tools that provide all the required mechanism without hard-coding any sort of policy.
+Despite doing highly non-trivial tasks, they are both pretty easy to use and compose and very well-documented.
+Thanks a lot to everyone involved!
+
+[bubblewrap]: https://github.com/containers/bubblewrap
+[BubbleBox]: {{ site.baseurl }}/projects/bubblebox
+[xdg-dbus-proxy]: https://github.com/flatpak/xdg-dbus-proxy
+[bubblejail]: https://github.com/igo95862/bubblejail
margin-top: 0.8em;
}
}
+
+/* Images (~350px wide) floating to the right but only if there is enough space */
+.float-right-350 {
+ float: right;
+ margin-left: 0.8em;
+ margin-bottom: 0.3em;
+}
+@media screen and (max-width:600px) {
+ .float-right-350 {
+ max-width: 300px;
+ float: none;
+ margin: auto;
+ }
+}
</p>
<ul>
<li><a href="mailto:post-AT-ralfj-DOT-de">E-Mail</a>,</li>
- <li>Jabber
: My Jabber-ID is <a href="xmpp:ralf-AT-jabber-DOT-ralfj-DOT-de">ralf-AT-jabber-DOT-ralfj-DOT-de</a> (also see <a href="https://en.wikipedia.org/wiki/Extensible_Messaging_and_Presence_Protocol" target="_blank">the Wikipedia article about Jabber</a>),</li>
+ <li>Jabber (also see <a href="https://en.wikipedia.org/wiki/Extensible_Messaging_and_Presence_Protocol" target="_blank">the Wikipedia article about Jabber</a>),</li>
<li><a href="https://git.ralfj.de/">Git repositories</a>,</li>
<li><a href="https://lists.ralfj.de/">Mailing lists</a>,</li>
<li>a DNS server (incl. DynDNS and DNSSEC),</li>
</p>
<ul>
<li><a href="mailto:post-ÄT-ralfj-PUNKT-de">E-Mail</a>,</li>
- <li>Jabber
: Meine Jabber-ID lautet <a href="xmpp:ralf-ÄT-jabber-PUNKT-ralfj-PUNKT-de">ralf-ÄT-jabber-PUNKT-ralfj-PUNKT-de</a> (siehe auch <a href="https://de.wikipedia.org/wiki/Extensible_Messaging_and_Presence_Protocol" target="_blank">den Wikipedia-Artikel zu Jabber</a>),</li>
+ <li>Jabber (siehe auch <a href="https://de.wikipedia.org/wiki/Extensible_Messaging_and_Presence_Protocol" target="_blank">den Wikipedia-Artikel zu Jabber</a>),</li>
<li><a href="https://git.ralfj.de/">Git-Repositories</a>,</li>
<li><a href="https://lists.ralfj.de/">Mailing-Listen</a>,</li>
<li>ein DNS-Server (inkl. DynDNS und DNSSEC),</li>
The tools were usually not written with general re-usability in mind.
But maybe you are having just the same problem as I did, in which case I hope they can be helpful.
-* [LiLaSS](lilass/): A simple xrandr-based application to configure laptop screens on Linux. If you are using a
+* [BubbleBox](bubblebox): A simple script to sandbox Linux applications.
+* [dyn-nsupdate](dyn-nsupdate): A tool to dynamically and securely update DNS zones via CGI.
+ This provides self-hosted DynDNS services.
+* [git-mirror](git-mirror): This can keep multiple git repositories of the same project in sync automatically.
+* [LiLaSS](lilass): A simple xrandr-based application to configure laptop screens on Linux. If you are using a
Laptop, frequently work both with and without an external screen, and you are not happy with
the configuration options your desktop provides, this may be for you.
-* [dyn-nsupdate](dyn-nsupdate/): A tool to dynamically and securely update DNS zones via CGI.
- This provides self-hosted DynDNS services.
-* [zonemaker](zonemaker/): A small script to generate DNS zone files from Python.
-* [schsh](schsh/): A collection of scripts and configuration files which can be used to grant
+* [Rust-101](rust-101): A small tutorial for the [Rust language](https://www.rust-lang.org).
+* [schsh](schsh): A collection of scripts and configuration files which can be used to grant
someone secure (SSH-based) access to a machine, without giving them a shell or read access
to the entire file system.
-* [Rust-101](rust-101/): A small tutorial for the [Rust language](https://www.rust-lang.org).
-* [git-mirror](git-mirror/): This can keep multiple git repositories of the same project in sync automatically.
+* [zonemaker](zonemaker): A small script to generate DNS zone files from Python.
For some more of my projects, check out the [public git repositories](https://www.ralfj.de/git/)
hosted on my server and my [GitHub profile](https://github.com/RalfJung/).
# Site settings
-baseurl: "/research"
-url: "https://www.ralfj.de"
+baseurl: ""
+url: "https://research.ralfj.de"
timezone: "Europe/Berlin"
defaults:
-../ralf/_includes/
\ No newline at end of file
+../personal/_includes
\ No newline at end of file
-../ralf/_layouts/
\ No newline at end of file
+../personal/_layouts
\ No newline at end of file
-../ralf/_plugins/
\ No newline at end of file
+../personal/_plugins
\ No newline at end of file
-../ralf/_sass/
\ No newline at end of file
+../personal/_sass
\ No newline at end of file
sort: 2
---
-<h3>E-Mail Address</h3>
+<p><b>Email:</b> ralf DOT jung AT inf DOT ethz DOT ch</p>
-<p>research AT ralfj DOT de</p>
+<p><b>Phone:</b> +41 44 632 5598</p>
-<h3>Work Address</h3>
-
-<p>
-MIT CSAIL, 32-G978A (PDOS)<br/>
-32 Vassar St<br/>
-Cambridge, MA 02139<br/>
-USA
+<p><b>Office / Mail:</b><br/>
+<a href='https://ethz.ch/staffnet/de/service/raeume-gebaeude/orientierung/gebaeude.html?args0=CNB' target='_blank'>CNB</a> H 109<br/>
+Universitätstrasse 6<br/>
+8092 Zürich<br/>
+Switzerland
</p>
title: Ralf Jung
---
-<div style="float:right; margin-left:0.8em; margin-bottom: 0.3em"><img src="me.jpg"></div>
+<div class="float-right-350"><img style="max-width: 350px; width: 100%;" src="me.jpg" srcset="me.jpg, me-2x.jpg 2x"></div>
-<p>I am a post-doctoral researcher in the <a href="https://pdos.csail.mit.edu/">PDOS group</a> at <a href="https://www.csail.mit.edu/" target="_blank">MIT CSAIL</a> under the supervision of <a href="https://people.csail.mit.edu/kaashoek/" target="_blank">Frans Kaashoek</a> and <a href="https://people.csail.mit.edu/nickolai/" target="_blank">Nickolai Zeldovich</a>.<br>
-Previously, I completed my <a href="thesis.html">PhD</a> at <a href="https://www.mpi-sws.org/">MPI-SWS</a> and <a href="https://www.uni-saarland.de/" target="_blank">Saarland University</a> in Saarbrücken, Germany; my advisor was <a href="https://people.mpi-sws.org/~dreyer/">Derek Dreyer</a>.</p>
+<p>I am assistant professor at <a href='https://ethz.ch' target="_blank">ETH Zürich</a>, leading the <a href="https://plf.inf.ethz.ch/" target="_blank">Programming Language Foundations Lab</a>.
+We are part of the <a href='https://pls.inf.ethz.ch/' target="_blank">Institute for Programming Languages and Systems</a>.</br>
+Previously, I completed my <a href="thesis.html">PhD</a> at <a href="https://www.mpi-sws.org/">MPI-SWS</a> and <a href="https://www.uni-saarland.de/" target="_blank">Saarland University</a> in Saarbrücken, Germany; my advisor was <a href="https://people.mpi-sws.org/~dreyer/">Derek Dreyer</a>.
+I also did a post-doc in the <a href="https://pdos.csail.mit.edu/">PDOS group</a> at <a href="https://www.csail.mit.edu/" target="_blank">MIT CSAIL</a>.
+</p>
-<p><i>I am on the academic job market this year (fall 2021), mostly looking for faculty positions in Europe.</i></p>
+<!-- <p><i>I am offering up to two fully funded PhD positions in my newly founded research group at <a href="https://ethz.ch/en/the-eth-zurich/working-teaching-and-research.html">ETH Zürich</a>, with flexible start date.
+I am looking for strong students that want to do research at the foundations of programming language theory, in program verification and separation logic, with a focus on Rust and Iris.
+Knowledge of Coq is greatly appreciated. Interested candidates can <a href="contact.html">contact me directly</a>.
+Please explain why you are interested in a PhD in this field and what your prior experience is. Also include a CV and possible contacts for recommendation letters.
+Note that doing a PhD at ETH Zürich generally requires a Master's degree, but there is a <a href="https://inf.ethz.ch/doctorate/direct-doctorate-computer-science.html">direct doctorate program</a> that you can enter with a Bachelor's degree (application deadline December 15th).</i></p> -->
<p>My two main lines of work are about <a href="https://www.rust-lang.org/">Rust</a> and <a href="https://iris-project.org/">Iris</a>.<br>
-On the Rust side, I am working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts.
-One key result here is our <a href="https://plv.mpi-sws.org/rustbelt/popl18/">type safety proof</a>, which also describes a methodology for establishing type safety of well-encapsulated unsafe code.
-My goal is to make unsafe Rust just as safe as safe Rust by means of formal verification.<br>
-On the Iris side, besides continuing development of its logical foundations, I am interested in applying Iris to new problem domains; recently I started working on modular verification of fault-tolerant distributed system components.<br>
+On the Rust side, me and my group are working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts.
+As part of this we are developing <a href="https://github.com/rust-lang/miri/">Miri</a>, a practical tool for detecting Undefined Behavior bugs in unsafe Rust code, which has become a part of the standard toolbox of unsafe code authors.
+Meanwhile, <a href="https://github.com/minirust/minirust">MiniRust</a> is our work-in-progress proposal for a precise specification of unsafe Rust, that I hope to integrate into an official Rust specification eventually.
+My long-term goal is to make unsafe Rust just as safe as safe Rust by means of formal verification based on rigorous foundations for all key components of the language.<br>
+On the Iris side, I am continuing development of its logical foundations.
+We are making Iris fit for specifying and verifying programming languages at scale using a more modular approach.
+The long-term goal is for Iris to be able to handle the full scale of complexities that arise when doing foundational verification of real languages.<br>
For some more information, check out my <a href="https://www.ralfj.de/blog/categories/research.html">research blog</a>, my <a href="cv.pdf">CV</a>, and my <a href="research-statement.pdf">research statement</a>.</p>
<p>In my free time, I like to run internet services myself and work on free software.
<h2>Conference and journal papers</h2>
+<h3>2023</h3>
+
+<ul><li>
+ <b>Grove: a Separation-Logic Library for Verifying Distributed Systems</b><br/>
+ Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich <br>
+ <i>In <a href="https://sosp2023.mpi-sws.org/index.html">SOSP 2023</a></i><br>
+ [<a href="https://iris-project.org/pdfs/2023-sosp-grove.pdf">paper</a>] [<a href="https://arxiv.org/abs/2309.03046">extended version</a>]
+</li></ul>
+
+<ul><li>
+ <b>Verifying vMVCC, a high-performance transaction library using multi-version concurrency control</b><br/>
+ Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich <br>
+ <i>In <a href="https://www.usenix.org/conference/osdi23">OSDI 2023</a></i><br>
+ [<a href="https://pdos.csail.mit.edu/papers/vmvcc:osdi23.pdf">paper</a>] [<a href="https://pdos.csail.mit.edu/projects/vmvcc.html#vmvcc">paper website</a> (incl. Coq formalization)]
+</li></ul>
+
<h3>2022</h3>
+<ul><li>
+ <b>Later Credits: Resourceful Reasoning for the Later Modality</b><br/>
+ Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer <br>
+ <i>In <a href="https://icfp22.sigplan.org/">ICFP 2022</a></i><br>
+ [<a href="https://plv.mpi-sws.org/later-credits/paper-later-credits.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/later-credits/">paper website</a> (incl. Coq formalization)]
+</li></ul>
+
<ul><li>
<b>Simuliris: A separation logic framework for verifying concurrent program optimizations</b><br/>
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer<br>
<b>GhostCell: Separating Permissions from Data in Rust</b><br/>
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer<br>
<i>In <a href="https://icfp21.sigplan.org/">ICFP 2021</a></i><br>
- [<a href="http://plv.mpi-sws.org/rustbelt/ghostcell/paper.pdf">paper</a>] [<a href="http://plv.mpi-sws.org/rustbelt/ghostcell/">paper website</a> (incl. Coq formalization)]
+ [<a href="https://plv.mpi-sws.org/rustbelt/ghostcell/paper.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/rustbelt/ghostcell/">paper website</a> (incl. Coq formalization)]
</li></ul>
<ul><li>
<ul><li>
<b>Unifying Worlds and Resources</b><br/>
Ralf Jung, Derek Dreyer<br>
- <i>At <a href="http://users-cs.au.dk/birke/hope-2015/">HOPE 2015</a>: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects</i><br>
+ <i>At <a href="https://users-cs.au.dk/birke/hope-2015/">HOPE 2015</a>: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects</i><br>
[<a href="iris/talk-hope2015.pdf">slides</a>] [<a href="https://www.youtube.com/watch?v=9Dyna88piek&list=PLnqUlCo055hX6SsmMr1AmW6quMjvdMPvK&index=10" target="_blank">YouTube</a>]
</li></ul>
-../ralf/style.scss
\ No newline at end of file
+../personal/style.scss
\ No newline at end of file
<p>RustBelt is built on top of <em>Iris</em>, a language-agnostic framework, implemented in the Coq proof assistant, for building higher-order concurrent separation logics. This dissertation begins by giving an introduction to Iris, and explaining how Iris enables the derivation of complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is exploited crucially to introduce the <em>lifetime logic</em>, which provides a novel separation-logic account of <em>borrowing</em>, a key distinguishing feature of the Rust type system.</p>
-<p style="color:red">
-This thesis has received an <a href="https://awards.acm.org/about/2020-doctoral-dissertation" style="color:red;font-weight:bold;">Honorable Mention for the ACM Doctoral Dissertation Award</a>,
-the <a href="https://sigplan.org/Awards/Dissertation/#2021_Ralf_Jung__Max_Planck_Institute_for_Software_Systems_and_Saarland_University" style="color:red;font-weight:bold;">ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award</a> (as one of two recipients),
-an <a href="https://www.mpg.de/prizes/otto-hahn-medal" style="color:red;font-weight:bold;">Otto Hahn Medal</a>,
-the <a href="https://etaps.org/2021/doctoral-dissertation-award" style="color:red;font-weight:bold;">ETAPS Doctoral Dissertation Award</a>,
-and the Saarland University <a href="https://www.uni-saarland.de/universitaet/aktuell/news/artikel/nr/24072.html" style="color:red;font-weight:bold;">Dr. Eduard Martin-Preis</a>.
+<p style="font-weight:bold">
+This thesis has received an <a href="https://awards.acm.org/about/2020-doctoral-dissertation" style="font-weight:bold;">Honorable Mention for the ACM Doctoral Dissertation Award</a>,
+the <a href="https://sigplan.org/Awards/Dissertation/#2021_Ralf_Jung__Max_Planck_Institute_for_Software_Systems_and_Saarland_University" style="font-weight:bold;">ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award</a> (as one of two recipients),
+an <a href="https://www.mpg.de/prizes/otto-hahn-medal" style="font-weight:bold;">Otto Hahn Medal</a>,
+the <a href="https://etaps.org/2021/doctoral-dissertation-award" style="font-weight:bold;">ETAPS Doctoral Dissertation Award</a>,
+and the Saarland University <a href="https://www.uni-saarland.de/universitaet/aktuell/news/artikel/nr/24072.html" style="font-weight:bold;">Dr. Eduard Martin-Preis</a>.
</p>
<h3>Download and references</h3>
git diff --cached
git commit -m "site upload"
-rsync ./ ralfj.de:/srv/www.ralfj.de/docroot/research/ -aP --exclude .git
+rsync ./ ralfj.de:/srv/research.ralfj.de/docroot/ -aP --exclude .git
#/bin/bash
cd "$(dirname "$0")"
-ralf/upload.sh
+personal/upload.sh
research/upload.sh
projects / web.git / commitdiff
