Ralf's Ramblings: Internship

Aug 22, 2018 • internshiprust • EditsPermalink

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. :)

Read more...

Aug 7, 2018 • internshiprust • EditsPermalink

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”.

Read more...

Jul 24, 2018 • internshiprust • EditsPermalink

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. :)

Read more...

Jul 19, 2018 • internshiprust • EditsPermalink

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.

Read more...

Jul 11, 2018 • internshiprust • EditsPermalink

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.

Read more...

Aug 12, 2017 • internshiprust • EditsPermalink

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.

Read more...

Aug 11, 2017 • internshiprust • EditsPermalink

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.

Read more...

Jul 17, 2017 • internshiprust • EditsPermalink

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.

Read more...

Jul 14, 2017 • internshiprust • EditsPermalink

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.

Read more...

Jun 6, 2017 • internshiprust • EditsPermalink

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.

Read more...

May 23, 2017 • internshiprust • EditsPermalink

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.

Read more...