---
title: "Types as Contracts"
categories: internship rust
+forum: https://internals.rust-lang.org/t/types-as-contracts/5562
---
-Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url
+Over the last couple of weeks of my [internship]({% post_url
2017-05-23-internship-starting %}), I have been working on a proposal for the "Unsafe Code Guidelines".
I got some very encouraging feedback at the [Mozilla All-Hands](https://internals.rust-lang.org/t/recapping-this-weeks-mozilla-all-hands/5465),
and now I'd like to put this proposal out there and start having a discussion.
<!-- MORE -->
Warning: Long post is long. You have been warned.
-If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}) first.
+If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({% post_url 2017-07-14-undefined-behavior %}) first.
## 1 It's in the Types
Borrowing some terminology from related fields, we can see the function type as stating a *contract*: The `&mut` say that `simple` expects to be called with non-aliasing pointers.
If we violate the contract, all bets are off.
-To realize this idea, we need to define, for every type, what is the contract associated with that type. When are elements of any given type *valid*?
-For some types, that's simple: `i32` is any four-byte value. `bool` is one byte, either `0` or `1`.
+To realize this idea, we need to define, for every type, what is the contract associated with that type. When is some piece of storage *valid* at any given type?
+For some types, that's simple: `i32` is any fully initialized four-byte value. `bool` is one byte, either `0` (representing `false`) or `1` (representing `true`).
Compound types like `(T, U)` are defined in terms of their constituent types: The first component must be a valid `T`, the second component a valid `U`.
Where it gets interesting is the reference types: `&mut T` says that we have a (non-null, properly aligned) pointer.
## 2 Specification Framework
-I have [previously written about my thoughts on undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}):
+I have [previously written about my thoughts on undefined behavior]({% post_url 2017-07-14-undefined-behavior %}):
> I also think that tooling to *detect* UB is of paramount importance [...].
In fact, specifying a dynamic UB checker is a very good way to specify UB!
Following this, I will in the following describe how we could check the contracts expressed by Rust's types for violations.
I am considering a MIR program; if a Rust program is supposed to be checked, it has to be translated to MIR first.
-(You can [read up on my explanation]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
-The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).[^1]
+(You can [read up on my explanation]({% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
+The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({% post_url 2017-06-06-MIR-semantics %}).[^1]
The extra state in my proposal consists of something akin to a reader-writer lock for every memory location.
I am first going to describe these locks and how they affect program behavior, before explaining contract validation.
When a lock is acquired, we record which stack frame is the owner of this lock (starting at 0 for `main`, and counting up).
Now, on every read access, we check whether there is a write lock of this location held *by another function*.
If yes, the access is UB.
-Furthermore, write accesses and acquiring a write lock are UB if there is a read lock held *or* if there is a write lock held by another function.
-Finally, acquiring a read lock is UB if there is a write lock held by anyone, including the function requesting a read lock.
+Furthermore, write accesses are UB if there is a read lock held *or* if there is a write lock held by another function.
+Finally, acquiring a lock makes sure that the new lock is not in conflict with existing locks:
+Acquiring a read lock is UB if there is a write lock held by anyone, including the function requesting a read lock; and acquiring a write lock is UB is there is any lock held by anyone.
Locks are typically released automatically when they expire.
To this end, the function acquiring a lock can optionally specify the *lifetime* of the lock.
To this end, the `LockInfo` is removed from the location's `locks` and put into a `HashMap<Lifetime, (Location, LockInfo)>` which is stored somewhere separately from the program's memory.
When the `EndRegion` corresponding to the given lifetime is reached, the lock is reacquired and put back into the `locks` of the given location.
-### 2.2 Validation
+### 2.2 Examples
-With the lock mechanism established, we can now look at the core of the proposal: Validating the contract described by a type.
-This is done by a new MIR statement, `Validate`, which takes two arguments: An *operation* (which we will discuss shortly), and a list of `(Lvalue, Ty)` pairs defining which lvalues is supposed to be validated at which type.
-Crucially, this is a non-erased type -- all the lifetime information must be present.
-
-The most important validation operation is *acquire validation*.
-As the name indicates, this is about acquiring the appropriate locks.
-It also otherwise makes sure that values are valid at the given type, e.g., references have to be non-NULL and aligned.
-
-The core of acquire validation is an operation with a signature roughly like this:
-{% highlight rust %}
-fn acquire_validate(lval: Lvalue, ty: Ty, mutbl: Mutability, lft: Option<Lifetime>)
-{% endhighlight %}
-Why are mutability and lifetime showing up here?
-The reason is that reference types have a "transitive" effect down the type hierarchy: `&T` makes everything reachable through this reference read-only, even if `T` involves `&mut`.
-Similarly, in case of nested references, it is the *outermost* reference that defines the lifetime for which access through this pointer is granted.
-(The compiler makes sure that inner references always have longer lifetimes than outer references.)
-
-`acquire_validate` recursively traverses the type hierarchy.
-When it encounters a primitive type like `i32`, it acquires a lock of `size_of::<ty>` many locations starting at `lval` for lifetime `lft` -- this will be a write or read lock depending on whether `mutbl` says this data is mutable or not.[^2]
-In other words, memory is locked "at the leaves" of the type structure, rather than locking immediately when we see a reference type.
-We will come back later to why this is necessary.
-Validation also makes sure that the value stored in memory is valid at the given type.
-For a `u32`, this just amounts to checking that the memory is properly initialized.
-
-[^2]: For simplicity, we pretend lvalues are just locations in memory. Actually, lvalues can also refer to variables not in memory (like non-addressable stack locals), but these do not need to be locked. Furthermore, lvalues for unsized types carry the additional information stored in a fat pointer, i.e., a length (for slices) or a vtable (for trait objects); this is handled appropriately when validating the respective types.
-
-For compound types like tuples, `struct` or `enum`, validation proceeds recursively on the fields.
-In particular, the enum discriminant is checked to be in-range (in particular, this empty enums always invalid).
-However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here.
-
-Finally, at a reference type, two things happen.
-First, the reference itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
-The reference is also checked to be non-NULL and properly aligned for the type it points to.
-Furthermore, validation proceeds recursively after *dereferencing* the reference.
-Crucially, the `mutbl` and `lft` for this recursive call are taking the reference type into account:
-If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime.
-If `mutbl` was mutable, it becomes immutable when following a shared reference.
-
-There are two other validation operations besides acquire validation: release validation, and suspend validation.
-These serve to release the appropriate locks before handing references to foreign code, and to handle the operation of taking a reference.
-(Bear with me for just a little longer, we will see examples of this soon.)
-Suspend validation takes an additional parameter, namely the lifetime for which locks are to be suspended.
-Both operations recursively follow the type just like acquire validation, and for all memory they visit, they release/suspend *write* locks.
-Read locks are not touched, which corresponds to the fact that shared references are `Copy` and hence never "given up":
-Shared references always remain usable until their lifetime expires, at which point the read lock is released automatically.
-
-Validation statements are emitted during MIR construction in the following places:
-- At the beginning of the function, we perform acquire validation of the arguments.
-- When taking a reference, we suspend the referee for the reference lifetime and acquire the referent.
-- When calling another function, we release the arguments and acquire the return value.
-
-### 2.3 Examples
-
-After all this rather dry theory, let us look at some examples demonstrating how validation works, and how it enables optimizations.
+With the lock mechanism established, we can now perform type validation in MIR.
+To this end, we add a new `Validate` statement to the language.
+This statement takes a list of `(Lvalue, Ty)` pairs to be validated, and a *validation operation*.
+The operation can be *acquire*, *suspend (for a lifetime)* or *release*, indicating whether memory locks are acquired, suspended, or released.
+Before explaining type validation in general, let us look at some examples.
#### Validating function arguments
I mentioned above that we want this case to be UB, because we want to be able to reorder the two stores.
Indeed, it will turn out that the validation describes above triggers UB here.
-There are no references taken and no other function is called, so the only validation that happens is acquiring the arguments at the beginning of the function.
-This validates our contract with the caller.
-`x` is of reference type, so validation will first acquire the write lock for the memory used to store `x` itself (that's somewhere on the stack).
-Next, it will follow the reference and recursively validate whatever `*x` is valid at type `i32`.
-In the recursive call, the `lft` will still be `None` because the lifetime of the reference outlives the function call.
+We perform acquire validation of the arguments immediately after a function is called.
+This validates the function's contract with the caller.
+`x` is of reference type, so validation will follow the reference and recursively validate whatever `*x` is valid at type `i32`.
The recursive call then acquires the write lock for `*x` and checks that memory is initialized.
+The lock is acquired for the entire duration of the function call, based on the fact that the lifetime of the reference outlives the function.
This completes validating `x`.
Validation of `y` proceeds exactly the same way.
In particular, validation will acquire a write lock for `*y`.
Furthermore, we want to eliminate the load from `x` at the end, and instead re-use `x_val`, arguing that since `x` is a shared reference, it is UB for `nop` to change its value.
In the beginning of `example`, during acquire validation, we acquire the read lock for `*x` and the write lock for `*y` and `*z`.
-The release validation before calling `fun` releases all write locks covered by `x` and `z`.
-For `x`, this doesn't actually do anything, but the write lock on `z` is released here.
+When we pass a mutable reference to `fun`, we explicitly acknowledge that `fun` has the right to modify this memory.
+This means that we have to *release* any write locks that we may hold on `x` or `z`, which is done by performing release validation on all function arguments.
+For `x`, this doesn't actually do anything as we only hold a read lock, but the write lock on `z` is released here.
(We assume there is no implicit reborrowing of `z` going on here. The curly braces make it so that `z` is moved, not borrowed, to `fun`.)
-So, when `fun` is called, we hold the read lock for `x` and the write lock for `y`.
+So, when `fun` is called, we still hold the read lock for `x` and the write lock for `y`.
Consequently, if `fun` were to access `y` or write to `x`, we know that's UB -- so we can rely on this not to happen and perform our desired optimizations.
Notice that this optimization is extremely hard to perform e.g. in C, because to know that `fun` cannot access `y`, the compiler needs to do whole-program alias analysis -- a notoriously hard problem.
#### Validating taking a reference
In the last example, we deliberately *moved* `z` to `fun` to side-step any discussions about borrowing.
-However, typically, you would actually *reborrow* `z`, leading to additional validation calls around the operation that takes a reference.
-We will look at that case now.
-Let us also say that `fun` actually returns a reference with the same lifetime as `z`.
+However, typically, you would actually *reborrow* `z`.
+As we will see in this example, to properly model transferring ownership of (re)borrowed memory to other functions, we will perform suspend and acquired validation around the operation that takes a reference.
+To better demonstrate this, let us also say that `fun` actually returns a reference with the same lifetime as `z`.
Overall, our code now looks like this (with all reborrowing being explicit):
{% highlight rust %}
// Defined elsewhere: fn fun<'z>(x: &i32, z: &'z mut (i32, i32)) -> &'z mut i32 { ... }
fn example(x: &i32, y: &mut i32, z: &mut (i32, i32)) {
- Validate(Acquire, [x, y]);
+ Validate(Acquire, [x, y, z]);
let x_val = *x;
let y_val = *y;
{ // 'inner begins here
- Validate(Suspend('z), [z]);
+ Validate(Suspend('inner), [z]);
let z_for_fun = &'inner mut z;
Validate(Acquire, [z_for_fun]);
This models the fact that, no matter what we do with the newly created reference, we know that when `'inner` ends, we get our exclusive access back.
After the suspension, we don't hold a lock any more for what is now `*z_for_fun`, so we immediately acquire a write lock again.
However, following the type of `z_for_fun`, we will acquire this lock only for lifetime `'inner`.
-(Releasing and then acquiring the write lock may sound somewhat redundant.
-However, notice that, if we were to take a shared reference, we would now acquire a read lock rather than a write lock.)
+For this to work, validation needs to know the *non-erased type* of the lvalues -- all the lifetime information must be present, so we can acquire the lock for the right lifetime.
+(Suspending and then acquiring the write lock may sound somewhat redundant.
+However, notice that, if we were to take a shared reference, we would now acquire a read lock rather than a write lock.
+Furthermore, even here, the overall effect is far from a no-op: The suspended lock will stay around even if the reacquired lock is released. In fact, this is exactly what happens next.)
Next, we call `fun`.
-At this point, we release our write lock on `*z_for_fun` again.
-However, notice that the suspended lock of `*z` stays around -- so while we gave up control of `z` (aka `z_for_fun`) for lifetime `'inner`, we still know that we will get control back when `'inner` ends!
+At this point, we release our write lock on `*z_for_fun` again, as usual when passing a mutable reference to a function.
+(The acquire-release of `z_for_fun` is indeed redundant here, but notice that the two validation statements arise from two separate MIR operations: taking a reference and calling a function.
+These operations just happen to occur immediately after one another here.)
+However, the suspended lock of `*z` stays around -- so while we gave up control of `z` (aka `z_for_fun`) for lifetime `'inner`, we still know that we will get control back when `'inner` ends!
`fun` is now free to do whatever it wants, as long as it does not violate our still-existing write lock of `*y` and the read lock of `*x`.
When `fun` returns, we obtain a new mutable reference.
When we come to the write to `*y`, we know that this write is redundant because (a) we held the write lock for `*y` all the time, so nobody else could have written to it without triggering UB, and (b) we know `z_inner` does not alias with `y` (or else we would already have UB), so we ourselves have not written to `*y` either.
Hence, we may optimize away the write.
-### 2.4 `UnsafeCell`
+### 2.3 Validation
-This concludes the examples.
-I hope you now have an idea of how memory locks and validation affect the execution when "bad" references are passed around, and how they validate the assumptions we need to make for optimizations that reorder memory accesses.
+The examples should already give you a good idea of what `Validate` does.
+It is time to look at this statement in some more depth.
+Remember that it takes a validation operation and a list of lvalue-type pairs as arguments.
+The most important validation operation is *acquire validation*.
+As the name indicates, this is about acquiring the appropriate locks.
+It also otherwise makes sure that values are valid at the given type, e.g., references have to be non-NULL and aligned.
+
+The core of acquire validation is an operation with a signature roughly like this:
+{% highlight rust %}
+fn acquire_validate(lval: Lvalue, ty: Ty, mutbl: Mutability, lft: Option<Lifetime>)
+{% endhighlight %}
+Why are mutability and lifetime showing up here?
+The reason is that reference types have a "transitive" effect down the type hierarchy: `&T` makes everything reachable through this reference read-only, even if `T` involves `&mut`.
+Similarly, in case of nested references, it is the *outermost* reference that defines the lifetime for which access through this pointer is granted.
+(The compiler makes sure that inner references always have longer lifetimes than outer references.)
+
+As we have seen in the examples, `acquire_validate` recursively traverses the type hierarchy.
+When it encounters a primitive type like `i32`, it acquires a lock of `size_of::<ty>` many locations starting at `lval` for lifetime `lft` -- this will be a write or read lock depending on whether `mutbl` says this data is mutable or not.[^2]
+In other words, memory is locked "at the leaves" of the type structure, rather than locking immediately when we see a reference type.
+We will come back later to why this is necessary.
+Validation also makes sure that the value stored in memory is valid at the given type.
+For a `u32`, this just amounts to checking that the memory is properly initialized.
+
+[^2]: For simplicity, we pretend lvalues are just locations in memory. Actually, lvalues can also refer to variables not in memory (like non-addressable stack locals), but these do not need to be locked. Furthermore, lvalues for unsized types carry the additional information stored in a fat pointer, i.e., a length (for slices) or a vtable (for trait objects); this is handled appropriately when validating the respective types.
+
+For compound types like tuples, `struct` or `enum`, validation proceeds recursively on the fields.
+In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type).
+However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here.
-One topic that did not come up yet is interior mutability.
+Finally, when encountering a box or reference type, two things happen.
+First, the pointer itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
+The pointer is also checked to be non-NULL and properly aligned for the type it points to.
+Furthermore, validation proceeds recursively after *dereferencing* the pointer.
+Crucially, for the case of validating a reference, the `mutbl` and `lft` for this recursive call are taking the type into account:
+If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime.
+If `mutbl` was mutable, it becomes immutable when following a shared reference.
+
+Acquire validation is performed at the beginning of every function (acquiring the function arguments) and upon returning from another function (acquiring the return value).
+These are the places when we rely on other functions providing valid data to us.
+
+There are two other validation operations besides acquire validation: release validation, and suspend validation.
+Both operations recursively follow the type just like acquire validation, and for all memory they visit, they release/suspend *write* locks.
+Read locks are not touched, which corresponds to the fact that shared references are `Copy` and hence never "given up":
+Shared references always remain usable until their lifetime expires, at which point the read lock is released automatically.
+
+Release validation occurs before calling a function, when the function arguments are released.
+This grants the functions write access to memory that we are explicitly passing along.
+
+Suspend validation occurs before taking a reference, using the lifetime of the new reference.
+This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
+
+**Update:** It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
+
+To summarize, validation statements are emitted during MIR construction in the following places:
+- At the beginning of the function, we perform acquire validation of the arguments.
+- When taking a reference, we suspend the referee for the reference lifetime and acquire the referent.
+- When calling another function, we release the arguments and acquire the return value.
+
+
+### 2.4 `UnsafeCell`
+
+I hope you now have an idea of how memory locks and validation enforce the assumptions that are encoded in Rust's types.
+One topic that needs special treatment in this context is interior mutability.
If a function takes an `x: &Cell<i32>`, following the rules above, it will acquire a read lock of `*x` for the duration of the function call, making `*x` immutable.
Clearly, we do not want to do that -- calling `x.set` *will* actually mutate `*x`, and mutating through a shared reference is exactly the point of using `Cell`!
-Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/beta/core/cell/struct.UnsafeCell.html).
-We can use this for our purposes: To adjust validation for interior mutability, we *stop* our recursive descent and do not do anything when reaching an `UnsafeCell`.
+Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/stable/core/cell/struct.UnsafeCell.html).
+We can use this for our purposes: To adjust validation for interior mutability, we *stop* our recursive descent and do not do anything when reaching an `UnsafeCell` *while `mutbl` indicates we are in immutable mode* -- `&mut UnsafeCell` is not affected.
In particular, no locks are acquired.
This justifies calling `set` on a shared reference and having the value changed.
Of course, it also means we cannot do some of the optimizations we discussed above -- but that's actually exactly what we want!
I have described a mechanism to validate the contract expressed by Rust's types, in particular, the uniqueness and read-only guarantees provided by reference types.
This validation describes what (safe) code can assume about its variables at run-time, and it enables some code motion optimizations that would otherwise require whole-program alias analysis.
-
I said before that I think providing a way to *detect* UB is crucial, and the framework laid out above is designed with this in mind.
In fact, I have been working on a miri-based implementation of this mechanism:
[This rustc branch](https://github.com/RalfJung/rust/tree/mir-validate) adds the new `Validate` statement to MIR and adds a MIR pass to insert validation statements as described above, while [this miri branch](https://github.com/RalfJung/miri/tree/mir-validate) adds memory locks to miri and implements type-based validation.
You have reached the end of this blog post.
Thanks a lot for reading.
If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
-If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly.
-The concrete proposal will sure need some fixing here and there, but my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
+If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly or add a note in the [forum](https://internals.rust-lang.org/t/types-as-contracts/5562) for any ammendments that turned out to be necessary.
+The concrete proposal will sure need some fixing here and there.
+It is also not complete yet.
+I already mentioned that there are open questions around unsafe code.
+Other areas of future work include `static` variables and the `NonZero` type.
+Nevertheless, my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
So, keep the comments flowing -- and safe hacking.
+**Update**: I did some refactoring of the post, reordering sections 2.2 and 2.3 to hopefully make it all flow better. Thanks for all the helpful feedback!
+
#### Footnotes
projects / web.git / blobdiff