forum: https://internals.rust-lang.org/t/https-www-ralfj-de-blog-2017-08-11-types-as-contracts-evaluation-html/5753
---
-Some weeks ago, I described [Types as Contracts]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}) as an approach for how to go about defining Rust's aliasing-related [undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}).
+Some weeks ago, I described [Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) as an approach for how to go about defining Rust's aliasing-related [undefined behavior]({% post_url 2017-07-14-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](https://github.com/solson/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.
Unsurprisingly, some of miri's test cases started to fail once I properly implemented the rules I wanted to have checked.
Some of these turned out to be [compiler](https://github.com/rust-lang/rust/issues/43457) [bugs](https://github.com/rust-lang/rust/issues/43481), but others are actually examples of code violating the proposed rules.
In the following, I describe the patterns that I found.
-I assume that you are familiar with Types as Contracts as introduced in my [previous post]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
+I assume that you are familiar with Types as Contracts as introduced in my [previous post]({% post_url 2017-07-17-types-as-contracts %}).
-## 1.1 Ownership Passing Via Raw Pointers
+### 1.1 Ownership Passing Via Raw Pointers
I already mentioned this in the original post: `mem::swap` triggers a lock violation in the strictest interpretation of the model.
{% highlight rust %}
This list is not exhaustive by any means; there are problems of this sort pretty much whenever raw pointers are used in non-trivial ways.
-## 1.2 Uninitialized memory
+### 1.2 Uninitialized memory
Any place that calls `mem::uninitialized` instantly has validation blow up because the returned `T` is, obviously, not actually a valid `T` -- it is, after all, completely uninitialized.
However, it turns out that `mem::uninitialized` is causing other problems as well (e.g. around uninhabited types), and [better APIs for handling uninitialized data have already been proposed](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung).
-## 1.3 `Arc::drop`
+### 1.3 `Arc::drop`
This is the most interesting case I found. The `Arc` destructor ends up calling `Arc::drop_slow`, which is implemented as follows:
{% highlight rust %}
There were also some changes affecting the rules of where validation calls are emitted in some corner cases, but there weren't really any interesting things to learn there.
At some point I will write down the exact rules in full detail; until then it is really the general approach that matters much more than such corner cases.
-## 2.1 Suspension of Write Locks
+### 2.1 Suspension of Write Locks
In the original proposal, on every borrow `y = &[mut] x;`, the write locks on `x` would be *suspended*.
This means that the locks get released, but will be re-acquired (or *recovered*) automatically when the lifetime of the borrow ends.
So, I will have to go back to the drawing board and figure out a different way to identify write locks.
I have some ideas, but I am not very happy with them.
-## 2.2 Unsafe Code
+### 2.2 Unsafe Code
As already indicated in the original post, the way I suggest to handle the problems with raw pointers described in [§1.1](#11-ownership-passing-via-raw-pointers) is by relaxing the validation performed around unsafe code.
Specifically, the code that emits MIR validation statements now detects if a function is unsafe, contains an unsafe block, or (in the case of closures) is defined inside an unsafe block/function.
Both of these options are certainly worth exploring.
-# 3 Testing Your Own Code
+## 3 Testing Your Own Code
The implementation of the model as described above (well, with the open problems mentioned in [§2.1](21-suspension-of-write-locks)) actually landed upstream in rustc and miri, so you can play around with this yourself!
To do so, you need to install Rust nightly and miri.
Notice however that miri currently supports virtually no interaction with the surrounding operating system, like file access or spawning threads.
-# 4 Future Work
+## 4 Future Work
As usual, there are so many things that could be done next.
Speaking of the implementation, the problem around write locks described in [§2.1](21-suspension-of-write-locks) is not the only issue; another problem I still have to solve is to properly acquire and release locks on padding bytes and enum discriminants.
While [§1.1](#11-ownership-passing-via-raw-pointers) is "fixed" by exempting unsafe code from the full range of checks, and the trouble with uninitialized memory ([§1.2](#12-uninitialized-memory)) will hopefully be solved as a side-effect of [changing the way uninitialized memory is handled](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung), this still leaves `Arc::drop` ([§1.3](13-arcdrop)) as an open problem.
+Notice that relaxing validation around unsafe code does not help here; the invalid data actually flows between functions, and so far the plan for unsafe code is to still enforce type validity when function boundaries are crossed.
This comes down to a judgment call: We could relax validation sufficiently (e.g., relaxing validation in entire modules when they do certain unsafe things, and not validating private fields of structs that we cannot access) to make this code legal, or we could declare that code to actually be UB.
The concrete problem in `Arc` can be fixed fairly easily as I have shown; the question is whether this kind of code is something that programmers actually expect to be legal -- and if they do, whether we can do anything about that (by providing documentation, or tools, or whatever else is necessary).
Of course, it may also turn out that this shows that the entire approach is not actually feasible.
After all, we want miri to also detect UB related to e.g. illegal pointer arithmetic.
These issues are far from settled, and I do have some interesting ideas here that I want so share with you.
-Finally, there is of course the discussion around how to handle raw pointers; I already talked in [§3](#22-unsafe-code) about some of the options that could be explored here.
+Finally, there is of course the discussion around how to handle raw pointers; I already talked in [§2.2](#22-unsafe-code) about some of the options that could be explored here.
Unfortunately, today is the last day of my internship, so I will no longer be able to work on all of this full-time like I did the last three months.
Still, I certainly intend to stay involved. This problem is way too interesting to just let it go :)
-As always, please comment with your thoughts on the topic.
+As always, please [comment](https://internals.rust-lang.org/t/https-www-ralfj-de-blog-2017-08-11-types-as-contracts-evaluation-html/5753) with your thoughts on the topic.
I am particularly curious about what kind of test cases you are throwing at miri, and how it is doing!
-**Update**: I added a proposal for how to fix the `Arc` problem.
+**Update:** I added a proposal for how to fix the `Arc` problem. **/Update**
projects / web.git / blobdiff