add thesis DOI
[web.git] / personal / _posts / 2017-08-11-types-as-contracts-evaluation.md
1 ---
2 title: "Types as Contracts: Implementation and Evaluation"
3 categories: internship rust
4 forum: https://internals.rust-lang.org/t/https-www-ralfj-de-blog-2017-08-11-types-as-contracts-evaluation-html/5753
5 ---
6
7 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 %}).
8 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.
9 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.
10
11 This post is my report on what I found, and how the approach itself changed in response to these findings.
12 It also explains how you can run miri yourself and have it check your code for undefined behavior according to this model.
13 Finally, I discuss some of the things that I would like to look at going forward.
14
15 <!-- MORE -->
16
17 ## 1 Rule Violations in libstd and miri's Test Suite
18
19 Unsurprisingly, some of miri's test cases started to fail once I properly implemented the rules I wanted to have checked.
20 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.
21 In the following, I describe the patterns that I found.
22 I assume that you are familiar with Types as Contracts as introduced in my [previous post]({% post_url 2017-07-17-types-as-contracts %}).
23
24 ### 1.1 Ownership Passing Via Raw Pointers
25
26 I already mentioned this in the original post:  `mem::swap` triggers a lock violation in the strictest interpretation of the model.
27 {% highlight rust %}
28 // Defined elsewhere: unsafe fn ptr::swap_nonoverlapping<T>(x: *mut T, y: *mut T) { ... }
29
30 pub fn swap<T>(x: &mut T, y: &mut T) {
31     Validate(Acquire, [x, y]);
32     let x = x as *mut T;
33     let y = y as *mut T;
34     unsafe {
35         Validate(Release, [x, y]);
36         ptr::swap_nonoverlapping(x, y, 1);
37     }
38 }
39 {% endhighlight %}
40 The problem is that `ptr::swap_nonoverlapping` takes a raw pointer, so `swap` sees no reason to release its write locks on the memory covered by `x` and `y`.
41 That makes it UB for `ptr::swap_nonoverlapping` to access that memory.
42
43 Raw pointers sneakily transferring ownership cannot just lead to functions accessing memory that the model does not allow them to access, it can also lead to overlapping mutable references.
44 We can see this in `[T]::split_at_mut`:
45 {% highlight rust %}
46 fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T]) {
47     let len = self.len();
48     let ptr = self.as_mut_ptr();
49
50     unsafe {
51         assert!(mid <= len);
52
53         (from_raw_parts_mut(ptr, mid),
54          from_raw_parts_mut(ptr.offset(mid as isize), len - mid))
55     }
56 }
57 {% endhighlight %}
58 The problem is that when `from_raw_parts_mut(ptr, mid)` returns a `&mut [T]`, that overlaps with `self`, so we have two aliasing mutable references in scope.
59 This makes acquire-validation of the return value of `from_raw_parts_mut(ptr, mid)` fail.
60
61 Another example of this pattern is `AtomicBool::get_mut`:
62 {% highlight rust %}
63 pub fn get_mut(&mut self) -> &mut bool {
64     unsafe { &mut *(self.v.get() as *mut bool) }
65 }
66 {% endhighlight %}
67 `self.v.get()` returns a `*mut u8`, which then gets turned into a `&mut bool`.
68 However, this again overlaps with `self`.
69
70 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.
71
72 ### 1.2 Uninitialized memory
73
74 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.
75 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).
76
77 ### 1.3 `Arc::drop`
78
79 This is the most interesting case I found.  The `Arc` destructor ends up calling `Arc::drop_slow`, which is implemented as follows:
80 {% highlight rust %}
81 unsafe fn drop_slow(&mut self) {
82     let ptr = self.ptr.as_ptr();
83
84     // Destroy the data at this time, even though we may not free the box
85     // allocation itself (there may still be weak pointers lying around).
86     ptr::drop_in_place(&mut self.ptr.as_mut().data);
87
88     if self.inner().weak.fetch_sub(1, Release) == 1 {
89         atomic::fence(Acquire);
90         Heap.dealloc(ptr as *mut u8, Layout::for_value(&*ptr))
91     }
92 }
93
94 fn inner(&self) -> &ArcInner<T> {
95     // This unsafety is ok because while this arc is alive we're guaranteed
96     // that the inner pointer is valid. Furthermore, we know that the
97     // `ArcInner` structure itself is `Sync` because the inner data is
98     // `Sync` as well, so we're ok loaning out an immutable pointer to these
99     // contents.
100     unsafe { self.ptr.as_ref() }
101 }
102 {% endhighlight %}
103
104 When `drop_slow` is executed, it first uses `drop_in_place` to drop the user data in the `Arc`.
105 Next, it calls `inner`, and this is where things go wrong.
106 The reason validation fails is that when `inner` calls `self.ptr.as_ref()`, that returns an `&ArcInner<T>`.
107 This return value is validated, like all return values are.
108 However, remember that we already dropped the `data` field of the `ArcInner`!
109 We don't actually have a fully valid `&ArcInner<T>`; only the `weak` and `strong` fields may still be used.
110 Nevertheless, the type of `inner` says that there is a valid shared reference to `ArcInner` being passed around, making this code UB.
111
112 Notice that even if `inner` did not care about the types, validation would still fail when `drop_slow` goes on calling the safe function `Layout::for_value` and passes it the invalid `&ArcInner<T>`.
113
114 To fix this, we have to make sure that the type `&ArcInner` is not used after `data` is dropped.
115 The following would work, for example:
116 {% highlight rust %}
117 unsafe fn drop_slow(&mut self) {
118     let ptr = self.ptr.as_ptr();
119
120     let layout = Layout::for_value(&*ptr);
121
122     // Destroy the data at this time, even though we may not free the box
123     // allocation itself (there may still be weak pointers lying around).
124     ptr::drop_in_place(&mut (*ptr).data);
125     // We must not use the type &(mut) ArcInner from now on, because that
126     // type is actually no longer valid.
127
128     if (*ptr).weak.fetch_sub(1, Release) == 1 {
129         atomic::fence(Acquire);
130         Heap.dealloc(ptr as *mut u8, layout)
131     }
132 }
133 {% endhighlight %}
134
135 ## 2 Changes to the Model
136
137 There were a whole bunch of other test failures, but they all turned out to be bugs in the implementations or even the model, rather than legit violations of the "Types as Contracts" idea.
138 In particular, it turned out that suspensions were actually not modeling borrowing of mutable data properly.
139
140 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.
141 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.
142
143 ### 2.1 Suspension of Write Locks
144
145 In the original proposal, on every borrow `y = &[mut] x;`, the write locks on `x` would be *suspended*.
146 This means that the locks get released, but will be re-acquired (or *recovered*) automatically when the lifetime of the borrow ends.
147 First of all, this actually fails to detect some cases that should be considered contract violations, like passing an `&mut bool` to a function and then having that function write something invalid (i.e., something that is not a boolean) into the reference.
148 To fix that, I added a new table to the global state of the program that would record suspended *lvalues* and their type (rather than suspended memory regions).
149 When the lifetime of the suspension ends, we perform a full re-acquire of the given lvalue at the given type, acquiring all the write locks again and also checking other invariants, like whether `bool` values are valid.
150
151 However, it turned out that this model was still too naive.
152 I failed to account for the fact that the borrow checker actually accepts programs like the following:
153 {% highlight rust %}
154 fn foo(s: (i32, i32)) {
155     Validate(Acquire, [s]);
156     let x;
157     {
158         Validate(Suspend('y), [s.1]);
159         let y = &/*'y*/ s.1;
160         Validate(Acquire, [*y]);
161
162         Validate(Suspend('x), [s]);
163         x = &/*'x*/ s;
164         Validate(Acquire, [*x]);
165     EndRegion('y); }
166 EndRegion('x); }
167 {% endhighlight %}
168 Let us step through this code while considering what happens with the locks.
169 Initially, we acquire `s`, so the memory occupied by the pair will be write-locked by `foo`.
170 When the borrow of `s.1` happens, we release the write lock and suspend `s.1` at type `i32`, making sure we re-acquire the write lock when the lifetime `'y` of the borrow.
171 Nothing interesting happens when `*y` gets acquired.
172 Next, the entire `s` gets borrowed, so we will try to release all the write locks on it during suspension -- but at this point, we don't even have a write lock of `s.1`!
173 Furthermore, due to this second borrow (that has a longer lifetime than the first borrow), we actually do *not* want to re-acquire the write lock on `s.1` when `'y` ends, we will want to wait until `'x` ends and keep the read lock until then.
174
175 What we really want to do is *count* how many shared borrows happened of `s.1` and `s.2`, respectively, and only acquire the write lock again once that count reaches 0.
176 This is complicated a lot once `RefCell` enters the game: The fact that we take a shared borrow does not mean that there won't also be mutable borrows again for the same region of memory.
177 This is demonstrated by the following example (with comments explaining what happens to the locks; adding all the `Validate` calls just makes this code unreadable):
178 {% highlight rust %}
179 fn test2(r: &mut RefCell<i32>) {
180     let x = &*r; // releasing write lock, first suspension recorded
181     let mut x_ref = x.borrow_mut();
182     let x_inner : &mut i32 = &mut *x_ref;
183     let x_inner_shr = &*x_inner; // releasing inner write lock, recording suspension
184     let y = &*r; // second suspension for the outer write lock
185     let x_inner_shr2 = &*x_inner; // 2nd suspension for inner write lock
186     /* ... */
187 }
188 {% endhighlight %}
189 At the end of this function, we actually have four aliasing shared borrows covering the content of the `RefCell`: `x`, `y`, `x_inner_shr` and `x_inner_shr2`.
190 There are two mutable references, both of which currently suspended (`x_inner` and `r`).
191
192 Once both `x_inner_shr` and `x_inner_shr2` have expired (i.e, their lifetime has ended), we will want to recover the write lock on `x_inner`.
193 Then `x_inner` expires, releasing the write lock.
194 Finally, once both `x` and `y` expire, `r` gets recovered and we again acquire the write lock.
195
196 To make that happen, we need to be able to track multiple suspended write locks for a location.
197 In implementing that, an interesting question came up:  What *identifies* a write lock?
198 I ended up using the lifetime of the lock as the identifier, but that doesn't actually work.
199 Notice that in the above example, both `x_inner` and `r` have the *same* lifetime, even though they are clearly corresponding to distinct write locks.
200 So, I will have to go back to the drawing board and figure out a different way to identify write locks.
201 I have some ideas, but I am not very happy with them.
202
203 ### 2.2 Unsafe Code
204
205 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.
206 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.
207 In that case, we still perform validation of the arguments passed to us, but we immediately release all locks again.
208 The same happens for data returned to us from other functions.
209 No further validation is happening inside the unsafe function.
210 In other words, we enforce the type invariants when data passes between functions, but we do not enforce any invariant *within* such functions.
211
212 I am aware that this part of the proposal is particularly controversial.
213 I do not know of an alternative that actually works with the raw pointers, and that performs validation purely based on the types of variables as they are passed around (rather than, say, also taking some form of provenance or "derived-from" relation into account).
214 In discussions, two possible solutions to this problems became apparent:
215
216 * We could try to find some kind of API that's slightly safer than raw pointers, and somehow does not lose all lifetime information.
217   Unsafe code using that API, and not using raw pointers, would still be subject to full validation and thus also enjoy the full set of optimizations.
218 * We could try to incorporate some form of provenance tracking into this model.
219
220 Both of these options are certainly worth exploring.
221
222 ## 3 Testing Your Own Code
223
224 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!
225 To do so, you need to install Rust nightly and miri.
226 Lucky enough, rustup makes this really easy.
227 (Unfortunately, I have very little Windows experience. If you manage to get this all running on Windows, I'm happy to link to your instructions for how to do that.)
228 On Linux and macOS, you can use the following commands to install everything you need, and run `test.rs` in miri:
229 ```
230 rustup install nightly
231 git clone https://github.com/solson/miri.git && cd miri
232 cargo +nightly install xargo # xargo is needed to build a libstd that miri can work with
233 xargo/build.sh # build that libstd
234 cargo +nightly build --release
235 MIRI_SYSROOT=~/.xargo/HOST cargo +nightly run --release --bin miri -- -Zmir-emit-validate=1 test.rs
236 ```
237 The flag `-Zmir-emit-validate=1` turns on generation of the MIR validation statements.
238 If you set it to `2`, full validation will performed even in unsafe functions.
239 Notice however that the flag only affects the code generated when miri actually runs; the script in `xargo/build.sh` controls validation for code in libstd.
240
241 If you find anything odd and things don't work as expected, please [report a bug](https://github.com/solson/miri/issues).
242 Notice however that miri currently supports virtually no interaction with the surrounding operating system, like file access or spawning threads.
243
244
245 ## 4 Future Work
246
247 As usual, there are so many things that could be done next.
248
249 miri's test suite is rather small, but still large enough to keep me busy, so I have not yet looked at the much more extensive test suite that comes with rustc -- but that certainly something I want to do eventually.
250 I am sure this will uncover bugs in corner-cases of my implementation, and it may also uncover new interesting cases of rules being violated.
251 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.
252
253 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.
254 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.
255 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.
256 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).
257 Of course, it may also turn out that this shows that the entire approach is not actually feasible.
258
259 Interestingly, the [discussion](https://internals.rust-lang.org/t/types-as-contracts/5562) of my previous post introducing Types as Contracts was to a large extend not even about this model, but about the underlying model of what memory and pointers are, and how to write a checker that actually faithfully models what LLVM does.
260 After all, we want miri to also detect UB related to e.g. illegal pointer arithmetic.
261 These issues are far from settled, and I do have some interesting ideas here that I want so share with you.
262
263 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.
264
265 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.
266 Still, I certainly intend to stay involved. This problem is way too interesting to just let it go :)
267
268 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.
269 I am particularly curious about what kind of test cases you are throwing at miri, and how it is doing!
270
271 **Update:** I added a proposal for how to fix the `Arc` problem. **/Update**