Ralf's Ramblings: Internship
Barriers and Two-phase Borrows in Stacked Borrows
My internship (“research assistantship”) with Mozilla has ended several weeks ago, and this post is a report of the most recent tweaks I made to Miri and Stacked Borrows. Neither project is by any means “done”, of course. However, both have reached a fairly reasonable state, so I felt some kind of closing report made sense. Also, if I ever want to finish my PhD, I’ll have to seriously scale down the amount of time I work on Rust – so at least from my side, things will move more slowly from now on.
In particular, installing Miri and running your test suite in it is now just a single command away! Scroll all the way down if you are not interested in the rest.
Stacked Borrows Implemented
Three months ago, I proposed Stacked Borrows as a model for defining what kinds of aliasing are allowed in Rust, and the idea of a validity invariant that has to be maintained by all code at all times. Since then I have been busy implementing both of these, and developed Stacked Borrows further in doing so. This post describes the latest version of Stacked Borrows, and reports my findings from the implementation phase: What worked, what did not, and what remains to be done. There will also be an opportunity for you to help the effort!
This post is a self-contained introduction to Stacked Borrows. Other than historical curiosity and some comparison with my earlier work on Types as Contracts there is no reason to read the original post at this point.
Two Kinds of Invariants: Safety and Validity
When talking about the Rust type system in the context of unsafe code, the discussion often revolves around invariants: Properties that must always hold, because the language generally assumes that they do. In fact, an important part of the mission of the Unsafe Code Guidelines strike force is to deepen our understanding of what these invariants are.
However, in my view, there is also more than one invariant, matching the fact that there are (at least) two distinct parties relying on these invariants: The compiler, and (authors of) safely usable code. This came up often enough in recent discussions that I think it is worth writing it down properly once, so I can just link here in the future. :)
Stacked Borrows: An Aliasing Model For Rust
In this post, I am proposing “Stacked Borrows”: A set of rules defining which kinds of aliasing are allowed in Rust. This is intended to answer the question which pointer may be used when to perform which kinds of memory accesses.
This is a long-standing open question of many unsafe code authors, and also by compiler authors who want to add more optimizations. The model I am proposing here is by far not the first attempt at giving a definition: The model is heavily based on ideas by @arielb1 and @ubsan, and of course taking into account the lessons I learned last year when I took my first stab at defining such a model, dubbed “Types as Contracts”.
Pointers Are Complicated, or: What's in a Byte?
This summer, I am again working on Rust full-time, and again I will work (amongst other things) on a “memory model” for Rust/MIR. However, before I can talk about the ideas I have for this year, I have to finally take the time and dispel the myth that “pointers are simple: they are just integers”. Both parts of this statement are false, at least in languages with unsafe features like Rust or C: Pointers are neither simple nor (just) integers.
I also want to define a piece of the memory model that has to be fixed before we can even talk about some of the more complex parts: Just what is the data that is stored in memory? It is organized in bytes, the minimal addressable unit and the smallest piece that can be accessed (at least on most platforms), but what are the possible values of a byte? Again, it turns out “it’s just an 8-bit integer” does not actually work as the answer.
I hope that by the end of this post, you will agree with me on both of these statements. :)
Thoughts on Compile-Time Function Evaluation and Type Systems
For some time now (since the 1.26 release, to be precise), Rust has a very powerful machinery for CTFE, or compile-time function evaluation. Since then, there have been various discussions about which operations should be allowed during CTFE, which checks the compiler should do, how this all relates to promotion and which kinds of guarantees we should be able to expect around CTFE. This post is my take on those topics, and it should not be surprising that I am going to take a very type-system centric view. Expect something like a structured brain dump, so there are some unanswered questions towards the end as well.
Back at Mozilla
After my internship last year has ended, I naturally became somewhat less active in the Rust community as I could not work on Rust full-time any more.
Well, for the following months I am going to be back full-time. :)
Thanks to @aturon, I am able to work as a research assistant for Mozilla during this summer (until the end of November).
I don’t really know what a “research assistant” is, but I am going to continue the work on Rust memory models, and hopefully also have some time to make progress on union semantics.
So Long, and Thanks for All the Fish
Yesterday was the last day of my Rust internship at Mozilla. I can hardly believe that twelve weeks have passed since that post, but my calendar insists. If you want to see what I have done, you can go read the posts that I wrote during the internship. (I almost kept up with the plan of bi-weekly blog posts…) You can also watch the 10-minute video version of this that I made for the internship presentation. The recording is available on Air Mozilla; my talk starts at 2h 14:30.
Types as Contracts: Implementation and Evaluation
Some weeks ago, I described Types as Contracts as an approach for how to go about defining Rust’s aliasing-related undefined behavior. One key property of this approach is that it is executable, which means we can actually have a program (in this case, miri) tell us whether some particular Rust test case exhibits undefined behavior or not. I have since then spent most of my time completing and refining this implementation, and running it on miri’s test suite to exercise various bits of the standard library and see whether they are actually following the rules I have been suggesting.
This post is my report on what I found, and how the approach itself changed in response to these findings. It also explains how you can run miri yourself and have it check your code for undefined behavior according to this model. Finally, I discuss some of the things that I would like to look at going forward.
Types as Contracts
Over the last couple of weeks of my internship, I have been working on a proposal for the “Unsafe Code Guidelines”. I got some very encouraging feedback at the Mozilla All-Hands, and now I’d like to put this proposal out there and start having a discussion.
Undefined Behavior and Unsafe Code Guidelines
Last year, the Rust unsafe code guidelines strike team was founded, and I am on it. :-) So, finally, just one year later, this post is my take at what the purpose of that team is.
Exploring MIR Semantics through miri
It’s now been two weeks since my internship started (two weeks already, can you believe it?). In other words, if I want to post “weekly or bi-weekly” updates, I better write one today ;) .
As already mentioned, the goal for this internship is to experiment with unsafe code guidelines by implementing them in miri. Before I tackle that, however, it seemed sensible for me to grab some low-hanging fruit in miri just to make myself familiar with the codebase. It turns out I entered “unsafe code guidelines” territory much quicker than expected. This post is about what I found, and it also serves as a nice demonstration of how we envision my unsafe code guidelines workflow to look like.
How to Specify Program (Undefined) Behavior?
This summer, I am given the awesome opportunity of spending three months in the Mozilla offices in Portland, working on Rust. I am extremely grateful that Mozilla is providing this opportunity to me; hopefully I can give something back by making some hands-on contributions to the Rust ecosystem.