// 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.)
+(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 just 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.
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`.
+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.
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 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, but my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
+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.
#### Footnotes
projects / web.git / blobdiff