the Ruby syntax actually means something else master
authorRalf Jung <post@ralfj.de>
Fri, 5 Jun 2020 07:31:56 +0000 (09:31 +0200)
committerRalf Jung <post@ralfj.de>
Fri, 5 Jun 2020 07:31:56 +0000 (09:31 +0200)
ralf/_config.yml
ralf/_posts/2018-07-13-arc-synchronization.md
ralf/_posts/2019-07-14-uninit.md
ralf/_posts/2019-10-20-type-soundness.md [new file with mode: 0644]
ralf/_posts/2019-11-18-stacked-borrows-paper.md [new file with mode: 0644]
ralf/_posts/2019-11-25-how-to-panic-in-rust.md [new file with mode: 0644]
ralf/_posts/2020-04-04-layout-debugging.md [new file with mode: 0644]
research/publications.html

index d63d639..31c8333 100644 (file)
@@ -17,7 +17,7 @@ readmes:
       - name: "zonemaker"
       - name: "schsh"
       - name: "rust-101"
-        src: "rust/rust-101"
+        src: "rust/my/rust-101"
       - name: "git-mirror"
 
 defaults:
index a91f8b2..7579dcf 100644 (file)
@@ -173,7 +173,7 @@ I said that `Mutex`/`RwLock` are good enough *most of the time*.
 However, `Arc` is one of those cases where the overhead induced by an exclusive lock is just way too big, so it is worth using a more optimized, unsafe implementation.
 As such, you are going to find plenty of atomic accesses in [the source code of `Arc`](https://github.com/rust-lang/rust/blob/c0955a34bcb17f0b31d7b86522a520ebe7fa93ac/src/liballoc/sync.rs#L201).
 
-And it turns out, as Hai and Jacques-Henri noticed when attempting to prove correctness of [`Arc::get_mut`](https://doc.rust-lang.org/stable/std/sync/struct.Arc.html#method.get_mut), that there is one place where `Relaxed` as used as an ordering, [but it really should have been `Acquire`](https://github.com/rust-lang/rust/pull/52031).
+And it turns out, as Hai and Jacques-Henri noticed when attempting to prove correctness of [`Arc::get_mut`](https://doc.rust-lang.org/stable/std/sync/struct.Arc.html#method.get_mut), that there is one place where `Relaxed` was used as an ordering, [but it really should have been `Acquire`](https://github.com/rust-lang/rust/pull/52031).
 Discussing the exact details of the bug would probably fill another blog post (`Arc` is *really* subtle), but the high-level story is exactly like in our example above: Thanks to `Acquire`, an ordering is induced between the code that follows the `get_mut` and the code in another thread that dropped the last other `Arc`, decrementing the reference count to 1.
 The PR that fixed the problem contains [some more details in the comments](https://github.com/rust-lang/rust/pull/52031/files).
 With `Relaxed`, no such ordering is induced, so we have a data race.
index 0b16076..b25a052 100644 (file)
@@ -54,7 +54,7 @@ However, if you [run the example](https://play.rust-lang.org/?version=stable&mod
 ## What *is* uninitialized memory?
 
 How is this possible?
-The answer is that, in the "abstract machine" that is used to specify the behavior of our program, every byte in memory cannot just have a value in `0..256` (this is Rust/Ruby syntax for a left-inclusive right-exclusive range), it can also be "uninitialized".
+The answer is that, in the "abstract machine" that is used to specify the behavior of our program, every byte in memory cannot just have a value in `0..256` (this is Rust syntax for a left-inclusive right-exclusive range), it can also be "uninitialized".
 Memory *remembers* if you initialized it.
 The `x` that is passed to `always_return_true` is *not* the 8-bit representation of some number, it is an uninitialized byte.
 Performing operations such as comparison on uninitialized bytes is [undefined behavior]({% post_url 2017-07-14-undefined-behavior %}).
diff --git a/ralf/_posts/2019-10-20-type-soundness.md b/ralf/_posts/2019-10-20-type-soundness.md
new file mode 100644 (file)
index 0000000..a8b9dbb
--- /dev/null
@@ -0,0 +1,14 @@
+---
+title: 'What Type Soundness Theorem Do You Really Want to Prove?'
+categories: rust research
+---
+
+My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the [SIGPLAN blog](https://blog.sigplan.org/) on the idea of "semantic typing".
+This is the methodology behind [RustBelt](https://plv.mpi-sws.org/rustbelt/popl18/), so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on.
+In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.
+
+The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets.
+If you are interested in formal methods for type systems and in particular for Rust, you should check it out!
+It's a great read:
+
+> ["What Type Soundness Theorem Do You Really Want to Prove?" on *PL Perspectives*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/)
diff --git a/ralf/_posts/2019-11-18-stacked-borrows-paper.md b/ralf/_posts/2019-11-18-stacked-borrows-paper.md
new file mode 100644 (file)
index 0000000..49d7dc7
--- /dev/null
@@ -0,0 +1,24 @@
+---
+title: "Stacked Borrows: An Aliasing Model for Rust (the paper)"
+categories: research rust
+reddit: /rust/comments/dy8avz/stacked_borrows_an_aliasing_model_for_rust_the/
+---
+
+I have [blogged]({% post_url 2019-05-21-stacked-borrows-2.1 %}) a [few]({% post_url 2019-04-30-stacked-borrows-2 %}) times before about [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md), my proposed aliasing model for Rust.
+But I am a researcher, and what researchers (are expected to) do is write papers---so that's what we did for Stacked Borrows as well.
+After a lot of work, I can now finally present to you our paper [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/) (thanks to open access, the paper is available under the CC-BY 4.0 license).
+
+<!-- MORE -->
+
+If you have already read my blog posts, the paper does not say much you have not seen already.
+However, the paper is the most coherent and most complete introduction to Stacked Borrows so far.
+So if you were always confused by some aspect of Stacked Borrows, or if you have not read the previous blog posts, the paper is a great way to learn about Stacked Borrows.
+
+If there is nothing new, you may wonder what took us so long, then, and why we needed 4 people for that?
+The answer is that my coauthor Hai, with some help from Jeehoon and me, took on the Herculean task of [formalizing Stacked Borrows in Coq](https://gitlab.mpi-sws.org/FP/stacked-borrows) and then formally verifying that some key optimizations are actually sound under that model.
+Those proofs turned out to be more complex to carry out than we expected, but now I am sure that what I claimed about Stacked Borrows in previous posts is actually correct.
+(In fact we were not able to complete the proof in time for the conference submission deadline, but lucky enough the reviewers were convinced enough by the informal description and the evaluation with Miri that they still accepted the paper.)
+
+Let me also use this opportunity to thank Mozilla and the Rust community for their help with this project.
+This work would not have been possible without Mozilla hiring me for two internships, without all the great feedback that you all gave me in response to my blog posts, and without all the support that I got in implementing Stacked Borrows, testing the standard library and a growing number of external crates in Miri, and fixing Stacked Borrows errors as they came up.
+Thank you all so much for working with me on this, this has been (and will hopefully continue to be) great fun. :-)
diff --git a/ralf/_posts/2019-11-25-how-to-panic-in-rust.md b/ralf/_posts/2019-11-25-how-to-panic-in-rust.md
new file mode 100644 (file)
index 0000000..f840aa6
--- /dev/null
@@ -0,0 +1,177 @@
+---
+title: "How to Panic in Rust"
+categories: rust
+forum: https://internals.rust-lang.org/t/how-to-panic-in-rust/11368
+---
+
+What exactly happens when you `panic!()`?
+I recently spent a lot of time looking at the parts of the standard library concerned with this, and it turns out the answer is quite complicated!
+I have not been able to find docs explaining the high-level picture of panicking in Rust, so this feels worth writing down.
+
+<!-- MORE -->
+
+(Shameless plug: the reason I looked at this is that @Aaron1011 implemented unwinding support in Miri.
+I wanted to see that in Miri since forever and never had the time to implement it myself, so it was really great to see someone just submit PRs for that out of the blue.
+After a lot of review rounds, this landed just recently.
+There [are still some rough edges](https://github.com/rust-lang/miri/issues?q=is%3Aissue+is%3Aopen+label%3AA-panics), but the foundations are solid.)
+
+The purpose of this post is to document the high-level structure and the relevant interfaces that come into play on the Rust side of this.
+The actual mechanism of unwinding is a totally different matter (and one that I am not qualified to speak about).
+
+*Note:* This post describes panicking as of [this commit](https://github.com/rust-lang/rust/commit/4007d4ef26eab44bdabc2b7574d032152264d3ad).
+Many of the interfaces described here are unstable internal details of libstd, and subject to change any time.
+
+## High-level structure
+
+When trying to figure out how panicking works by reading the code in libstd, one can easily get lost in the maze.
+There are multiple layers of indirection that are only put together by the linker,
+there is the [`#[panic_handler]` attribute](https://doc.rust-lang.org/nomicon/panic-handler.html) and the ["panic runtime"](https://github.com/rust-lang/rfcs/blob/master/text/1513-less-unwinding.md) (controlled by the panic *strategy*, which is set via `-C panic`) and ["panic hooks"](https://doc.rust-lang.org/std/panic/fn.set_hook.html),
+and it turns out panicking in `#[no_std]` context takes an entirely different code path... there is just a lot going on.
+To make things worse, [the RFC describing panic hooks](https://github.com/rust-lang/rfcs/blob/master/text/1328-global-panic-handler.md) calls them "panic handler", but that term has since been re-purposed.
+
+I think the best place to start are the interfaces controlling the two indirections:
+
+* The *panic runtime* is used by libstd to control what happens after the panic information has been printed to stderr.
+  It is determined by the panic *strategy*: either we abort (`-C panic=abort`) or we unwind (`-C panic=unwind`).
+  (The panic runtime also provides the implementation for [`catch_unwind`](https://doc.rust-lang.org/std/panic/fn.catch_unwind.html) but we are not concerned with that here.)
+
+* The *panic handler* is used by libcore to implement (a) panics inserted by code generation (such as panics caused by arithmetic overflow or out-of-bounds array/slice indexing) and (b) the `core::panic!` macro (this is the `panic!` macro in libcore itself and in `#[no_std]` context in general).
+
+Both of these interfaces are implemented through `extern` blocks: listd/libcore, respectively, just import some function that they delegate to, and somewhere entirely else in the crate tree, that function gets implemented.
+The import only gets resolved during linking; looking locally at that code, one cannot tell where the actual implementation of the respective interface lives.
+No wonder that I got lost several times along the way.
+
+In the following, both of these interfaces will come up a lot; when you get confused, the first thing to check is if you just mixed up panic *handler* and panic *runtime*.
+(And remember there's also panic *hooks*, we will get to those.)
+That happens to me all the time.
+
+Moreover, `core::panic!` and `std::panic!` are *not* the same; as we will see, they take very different code paths.
+libcore and libstd each implement their own way to cause panics:
+
+* libcore's `core::panic!` does very little, it basically just delegates to the panic *handler* immediately.
+* libstd's `std::panic!` (the "normal" `panic!` macro in Rust) triggers a fully-featured panic machinery that provides a user-controlled [panic *hook*](https://doc.rust-lang.org/std/panic/fn.set_hook.html).
+  The default hook will print the panic message to stderr.
+  After the hook is done, libstd delegates to the panic *runtime*.
+
+    libstd also provides a panic *handler* that calls the same machinery, so `core::panic!` also ends up here.
+
+
+Let us now look at these pieces in a bit more detail.
+
+## Panic Runtime
+
+The [interface to the panic runtime](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L53) (introduced by [this RFC](https://github.com/rust-lang/rfcs/blob/master/text/1513-less-unwinding.md)) is a function `__rust_start_panic(payload: usize) -> u32` that gets imported by libstd, and that is later resolved by the linker.
+
+The `usize` argument here actually is a `*mut &mut dyn core::panic::BoxMeUp` -- this is where the "payload" of the panic (the information available when it gets caught) gets passed in.
+`BoxMeUp` is an unstable internal implementation detail, but [looking at the trait](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panic.rs#L268-L281) we can see that all it really does is wrap a `dyn Any + Send`, which is the [type of the panic payload](https://doc.rust-lang.org/std/thread/type.Result.html) as returned by `catch_unwind` and `thread::spawn`.
+`BoxMeUp::take_box` returns a `Box<dyn Any + Send>`, but as a raw pointer (because `Box` is not available in the context where this trait is defined); `BoxMeUp::get` just borrows the contents.
+
+The two implementations of this interface Rust ships with are [`libpanic_unwind`](https://github.com/rust-lang/rust/tree/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libpanic_unwind) for `-C panic=unwind` (the default on most platforms) and [`libpanic_abort`](https://github.com/rust-lang/rust/tree/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libpanic_abort) for `-C panic=abort`.
+
+## `std::panic!`
+
+On top of the panic *runtime* interface, libstd implements the default Rust panic machinery in the internal [`std::panicking`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs) module.
+
+#### `rust_panic_with_hook`
+
+The key function that almost everything passes through is [`rust_panic_with_hook`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L439-L441):
+{% highlight rust %}
+fn rust_panic_with_hook(
+    payload: &mut dyn BoxMeUp,
+    message: Option<&fmt::Arguments<'_>>,
+    file_line_col: &(&str, u32, u32),
+) -> !
+{% endhighlight %}
+This function takes a panic source location, an optional unformatted panic message (see the [`fmt::Arguments`](https://doc.rust-lang.org/std/fmt/struct.Arguments.html) docs), and a payload.
+
+Its main job is to call whatever the current panic hook is.
+Panic hooks have a [`PanicInfo`](https://doc.rust-lang.org/core/panic/struct.PanicInfo.html) argument, so we need a panic source location, format information for a panic message, and a payload.
+This matches `rust_panic_with_hook`'s arguments quite nicely!
+`file_line_col` and `message` can be used directly for the first two elements; `payload` gets turned into `&(dyn Any + Send)` through the `BoxMeUp` interface.
+
+Interestingly, the *default* panic hook entirely ignores the `message`; what you actually see printed is [the `payload` downcast to `&str` or `String`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L176-L182) (whatever works).
+Supposedly, the caller should ensure that formatting `message`, if present, gives the same result.
+(And the ones we discuss below do ensure this.)
+
+Finally, `rust_panic_with_hook` dispatches to the current panic *runtime*.
+At this point, only the `payload` is still relevant -- and that is important: `message` (as the `'_` lifetime indicates) may contain short-lived references, but the panic payload will be propagated up the stack and hence must be `'static`.
+The `'static` bound is quite well hidden there, but after a while I realized that [`Any`](https://doc.rust-lang.org/std/any/trait.Any.html) implies `'static` (and remember `dyn BoxMeUp` is just used to obtain a `Box<dyn Any + Send>`).
+
+#### libstd panicking entry points
+
+`rust_panic_with_hook` is a private function to `std::panicking`; the module provides three entry points on top of this central function, and one that circumvents it:
+
+* the [`begin_panic_handler`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L332), the default panic handler implementation that backs (as we will see) panics from `core::panic!` and built-in panics (from arithmetic overflow or out-of-bounds array/slice indexing).
+  This obtains as input a [`PanicInfo` ](https://doc.rust-lang.org/core/panic/struct.PanicInfo.html), and it has to turn that into arguments for `rust_panic_with_hook`.
+  Curiously, even though the components of `PanicInfo` and the arguments of `rust_panic_with_hook` match up pretty well and seem like they could just be forwarded, that is *not* what happens.
+  Instead, libstd entirely *ignores* the `payload` component of the `PanicInfo`, and sets up the actual payload (passed to `rust_panic_with_hook`) such that it contains [the formatted `message`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L350).
+
+    In particular, this means that the panic *runtime* is irrelevant for `no_std` applications.
+  It only comes into play when libstd's panic handler implementation is used.
+  (The panic *strategy* selected via `-C panic` still has an effect as it also influences code generation.
+  For example, with `-C panic=abort` code can become simpler as it does not need to support unwinding.)
+
+* [`begin_panic_fmt`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L316), backing the [format string version of `std::panic!`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/macros.rs#L22-L23) (i.e., this is used when you pass multiple arguments to the macro).
+  This basically just packages the format string arguments into a `PanicInfo` (with a [dummy payload](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panic.rs#L56)) and calls the default panic handler that we just discussed.
+
+* [`begin_panic`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L392), backing the [single-argument version of `std::panic!`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/macros.rs#L16).
+  Interestingly, this uses a very different code path than the other two entry points!
+  In particular, this is the only entry point that permits passing in an *arbitrary payload*.
+  That payload is just [converted into a `Box<dyn Any + Send>`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L419) so that it can be passed to `rust_panic_with_hook`, and that's it.
+  
+    In particular, a panic hook that looks at the `message` field of the `PanicData` it is passed will *not* be able to see the message in a `std::panic!("do panic")`, but it *will* see the message in a `std::panic!("panic with data: {}", data)` as the latter passes through `begin_panic_fmt` instead.
+  That seems quite surprising. (But also note that `PanicData::message()` is not stable yet.)
+
+* [`rust_panic_without_hook`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/panicking.rs#L496) is the odd one out: this entry point backs [`resume_unwind`](https://doc.rust-lang.org/nightly/std/panic/fn.resume_unwind.html), and it actually does *not* call the panic hook.
+  Instead, it dispatches to the panic runtime immediately.
+  Like, `begin_panic`, it lets the caller pick an arbitrary payload.
+  Unlike `begin_panic`, the caller is responsible for boxing and unsizing the payload; `update_count_then_panic` just forwards that pretty much verbatim to the panic runtime.
+
+## Panic Handler
+
+All of the `std::panic!` machinery is really useful, but it relies on heap allocations through `Box` which is not always available.
+To give libcore a way to cause panics, [panic handlers were introduced](https://github.com/rust-lang/rfcs/blob/master/text/2070-panic-implementation.md).
+As we have seen, if libstd is available, it provides an implementation of that interface to wire `core::panic!` into the libstd panic machinery.
+
+The [interface to the panic handler](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panicking.rs#L78) is a function `fn panic(info: &core::panic::PanicInfo) -> !` that libcore imports and that is later resolved by the linker.
+The [`PanicInfo` ](https://doc.rust-lang.org/core/panic/struct.PanicInfo.html) type is the same as for panic hooks: it contains a panic source location, a panic message, and a payload (a `dyn Any + Send`).
+The panic message is represented as [`fmt::Arguments`](https://doc.rust-lang.org/std/fmt/struct.Arguments.html), i.e., a format string with its arguments that has not been formatted yet.
+
+## `core::panic!`
+
+On top of the panic handler interface, libcore provides a [minimal panic API](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panicking.rs).
+The [`core::panic!`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/macros/mod.rs#L10-L26) macro creates a `fmt::Arguments` which is then [passed to the panic handler](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panicking.rs#L82).
+No formatting happens here as that would require heap allocations; this is why `PanicInfo` contains an "uninterpreted" format string with its arguments.
+
+Curiously, the `payload` field of the `PanicInfo` that gets passed to the panic handler is always set to [a dummy value](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panic.rs#L56).
+This explains why the libstd panic handler ignores the payload (and instead constructs a new payload from the `message`), but that makes me wonder why that field is part of the panic handler API in the first place.
+Another consequence of this is that [`core::panic!("message")`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/macros/mod.rs#L15) and [`std::panic!("message")`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libstd/macros.rs#L16) (the variants without any formatting) actually result in very different panics: the former gets turned into `fmt::Arguments`, passed through the panic handler interface, and then libstd creates a `String` payload by formatting it.
+The latter, however, directly uses the `&str` as a payload, and the `message` field remains `None` (as already mentioned).
+
+Some elements of the libcore panic API are lang items because the compiler inserts calls to these functions during code generation:
+* The [`panic` lang item](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panicking.rs#L39) is called when the compiler needs to raise a panic that does not require any formatting (such as arithmetic overflow); this is the same function that also backs single-argument [`core::panic!`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/macros/mod.rs#L15).
+* The [`panic_bounds_check`](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/panicking.rs#L55) lang item is called on a failed array/slice bounds check.
+  It calls into the same method as [`core::panic!` with formatting](https://github.com/rust-lang/rust/blob/4007d4ef26eab44bdabc2b7574d032152264d3ad/src/libcore/macros/mod.rs#L21-L24).
+
+## Conclusion
+
+We have walked through 4 layers of APIs, 2 of which are indirected through imported function calls and resolved by the linker.
+That's quite a journey!
+But we have reached the end now.
+I hope you [didn't panic](https://en.wikipedia.org/wiki/Phrases_from_The_Hitchhiker%27s_Guide_to_the_Galaxy#Don't_Panic) yourself along the way. ;)
+
+I mentioned some things as being surprising.
+Turns out they all have to do with the fact that panic hooks and panic handlers share the `PanicInfo` struct in their interface, which contains *both* an optional not-yet-formatted `message` and a type-erased `payload`:
+* The panic *hook* can always find the already formatted message in the `payload`, so the `message` seems pointless for hooks.
+  In fact, `message` can be missing even if `payload` contains a message (e.g., for `std::panic!("message")`).
+* The panic *handler* will never actually receive a useful `payload`, so that field seems pointless for handlers.
+
+Reading the [panic handler RFC](https://github.com/rust-lang/rfcs/blob/master/text/2070-panic-implementation.md), it seems like the plan was for `core::panic!` to also support arbitrary payloads, but so far that has not materialized.
+However, even with that future extension, I think we have the invariant that when `message` is `Some`, then either `payload == &NoPayload` (so the payload is redundant) or `payload` is the formatted message (so the message is redundant).
+I wonder if there is any case where *both* fields will be useful -- and if not, couldn't we encode that by making them two variants of an `enum`?
+There are probably good reasons against that proposal and for the current design; it would be great to get them documented somewhere. :)
+
+There is a lot more to say, but at this point, I invite you to follow the links to the source code that I included above.
+With the high-level structure in mind, you should be able to follow that code.
+If people think this overview would be worth putting somewhere more permanently, I'd be happy to work this blog post into some form of docs -- I am not sure what would be a good place for those, though.
+And if you find any mistakes in what I wrote, please let me know!
diff --git a/ralf/_posts/2020-04-04-layout-debugging.md b/ralf/_posts/2020-04-04-layout-debugging.md
new file mode 100644 (file)
index 0000000..66000e0
--- /dev/null
@@ -0,0 +1,92 @@
+---
+title: "Debugging rustc type layouts"
+categories: rust
+forum: https://internals.rust-lang.org/t/psa-debugging-rustc-type-layouts/12082
+---
+
+This post is a "public service announcement" for people working on the guts of rustc.
+I wish I had known about this a year ago, so I hope this post can make this feature more widely known.
+
+<!-- MORE -->
+
+When working with MIR in rustc, one key data structure that comes up a lot is [`Layout`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_target/abi/struct.Layout.html) (formerly `LayoutDetails`), usually paired up with a type in a `TyAndLayout` (formerly `TyLayout`).
+This data structure describes everything that there is to know about how a type "looks like" in memory: size and alignment of the entire type, at which offset we can find which field, how enum variants are represented, which "niche" can be used in this type to optimize enums.
+
+`Layout` is quite versatile and can be hard to interpret, and when debugging Miri I regularly have to know what exactly the `Layout` of a certain type looks like or what exactly some aspect of `Layout` actually *means* in practice.
+While debugging MIR is easy via `rustc --emit mir` or the "MIR" button on the playground, debugging `Layout` was much more tedious.
+But not any more. :)
+
+All you have to do is enter the following code in [the playground](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=7abc008aed2669466d4ebe79ee7767fe):
+
+{% highlight rust %}
+#![feature(rustc_attrs)]
+
+#[rustc_layout(debug)]
+type T = (u8, u16);
+{% endhighlight %}
+
+The (permanently) unstable `rustc_layout` attribute [can now be used](https://github.com/rust-lang/rust/pull/69901) to dump some information about the type it is attached to (also works with `struct`/`enum`/`union` definitions).
+In this case, it prints:
+
+```
+error: layout_of((u8, u16)) = Layout {
+    fields: Arbitrary {
+        offsets: [
+            Size {
+                raw: 0,
+            },
+            Size {
+                raw: 2,
+            },
+        ],
+        memory_index: [
+            0,
+            1,
+        ],
+    },
+    variants: Single {
+        index: 0,
+    },
+    abi: ScalarPair(
+        Scalar {
+            value: Int(
+                I8,
+                false,
+            ),
+            valid_range: 0..=255,
+        },
+        Scalar {
+            value: Int(
+                I16,
+                false,
+            ),
+            valid_range: 0..=65535,
+        },
+    ),
+    largest_niche: None,
+    align: AbiAndPrefAlign {
+        abi: Align {
+            pow2: 1,
+        },
+        pref: Align {
+            pow2: 3,
+        },
+    },
+    size: Size {
+        raw: 4,
+    },
+}
+```
+
+That is quite a lot, but it contains all the key information about this type:
+the fields are at offsets 0 and 2, the type has alignment 2 (but preferred alignment 8) and size 4.
+We can also see that it uses the `ScalarPair` abi which is relevant for Miri and when passing data as arguments to another function.
+To learn more about what all this information means, see [the `Layout` type docs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_target/abi/struct.Layout.html).
+
+**Update:** After a suggestions by @jschievink, this can now also be used to print the [underlying type and layout](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=1de2bed0c0d0f9171bfb41969f5028fb) of named opaque types, which is particularly useful [for generators](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=de99ab78a4d77bceee6760021b19de7d). **/Update**
+
+So the next time you work with `Layout` and wonder how exactly the niche gets represented, or whether an `enum` can have `ScalarPair` abi (hint: yes it can), you can easily look at a few examples to see how rustc thinks about this type internally.
+This is basically the type-level equivalent of `--emit mir`.
+I have wanted this since forever, so much that some time ago I wrote an awful hack for this based on rustc debug tracing.
+Only very recently did I learn about the `rustc_layout` attribute and then I had to immediately extend it to support dumping all the information.
+Now `Layout` can be debugged in the browser on the playground, which is so much more convenient. :D
index e2b610f..f8ae0b6 100644 (file)
@@ -5,6 +5,22 @@ slug: Publications
 
 <!-- <h3>Under Submission</h3> -->
 
+<h3>2020</h3>
+
+<ul><li>
+  <b>The Future is Ours: Prophecy Variables in Separation Logic</b><br/>
+  Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs<br>
+  In <a href="https://popl20.sigplan.org/">POPL 2020</a><br>
+  [<a href="https://plv.mpi-sws.org/prophecies/paper.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/prophecies/">paper website</a>  (incl. appendix and Coq formalization)]
+</li></ul>
+
+<ul><li>
+  <b>Stacked Borrows: An Aliasing Model for Rust</b><br/>
+  Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer<br>
+  In <a href="https://popl20.sigplan.org/">POPL 2020</a><br>
+  [<a href="https://plv.mpi-sws.org/rustbelt/stacked-borrows/paper.pdf">paper</a>] [<a href="https://plv.mpi-sws.org/rustbelt/stacked-borrows/">paper website</a>  (incl. appendix and Coq formalization)]
+</li></ul>
+
 <h3>2018</h3>
 
 <ul><li>
@@ -78,8 +94,28 @@ slug: Publications
 
 <h3>2013</h3>
 <ul><li>
-  <b>An Intermediate Language To Formally Justify Memory Access Reordering</b> (Bachelor's Thesis)<br/>
+  <b>An Intermediate Language To Formally Justify Memory Access Reordering</b> <span style="white-space: nowrap">(Bachelor's Thesis)</span><br/>
   Ralf Jung, Supervisor: Sebastian Hack, Advisor: Sigurd Schneider<br>
-  [<a href="bachelor/bachelor.pdf">pdf</a>] [<a href="bachelor/bachelor-talk.pdf">slides</a>] [<a href="bachelor/bachelor.zip">coq</a>]
+  [<a href="bachelor/bachelor.pdf">thesis</a>] [<a href="bachelor/bachelor-talk.pdf">slides</a>] [<a href="bachelor/bachelor.zip">coq</a>]
 </li></ul>
 </p>
+
+<h2>Workshop Talks</h2>
+
+<h3>2019</h3>
+
+<ul><li>
+  <b>Logical Atomicity in Iris: the Good, the Bad, and the Ugly</b><br/>
+  Ralf Jung<br>
+  At <a href="https://iris-project.org/workshop-2019/">Iris Workshop 2019</a><br>
+  [<a href="iris/logatom-talk-2019.pdf">slides</a>]
+</li></ul>
+
+<h3>2015</h3>
+
+<ul><li>
+  <b>Unifying Worlds and Resources</b><br/>
+  Ralf Jung, Derek Dreyer<br>
+  At <a href="http://users-cs.au.dk/birke/hope-2015/">HOPE 2015</a>: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects<br>
+  [<a href="iris/talk-hope2015.pdf">slides</a>] [<a href="https://www.youtube.com/watch?v=9Dyna88piek&amp;list=PLnqUlCo055hX6SsmMr1AmW6quMjvdMPvK&amp;index=10" target="_blank">YouTube</a>]
+</li></ul>