2 title: "Two Kinds of Invariants: Safety and Validity"
3 categories: internship rust
4 forum: https://internals.rust-lang.org/t/two-kinds-of-invariants/8264
7 When talking about the Rust type system in the context of unsafe code, the discussion often revolves around *invariants*:
8 Properties that must always hold, because the language generally assumes that they do.
9 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.
11 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.
12 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. :)
18 The most prominent invariant in Rust is probably what I will call the *safety invariant*: This is the invariant that every safe function can assume holds.
19 This invariant depends on the type, so I will also speak of data being *safe at type `T`*, meaning the data satisfies the safety invariant.
20 (In fact, types come with [more than one safety invariant to appropriately handle sharing]({% post_url 2018-01-31-sharing-for-a-lifetime %}), but that is not our concern this time.)
22 For example, when you write a function `fn foo(x: bool)`, you can assume that `x` is safe for `bool`: It is either `true` or `false`.
23 This means that every safe operation on `bool` (in particular, case distinction) can be performed without running into [undefined behavior]({% post_url 2017-07-14-undefined-behavior %}).
25 In fact, this is the main point of the safety invariant:
27 > *The safety invariant ensures that safe code, no matter what it does, executes safely -- it cannot cause undefined behavior when working on this data.*
29 Based on that, it should not be hard to fill in the invariant for some more types.
30 For example, `&bool` is an aligned, non-NULL reference to allocated read-only memory (because safe code can dereference) such that the data stored in that memory is safe at `bool` (because safe code can work on that `bool` after dereferencing).
31 This kind of "structural recursion" is happening everywhere for safety invariants: `x` is safe for `(T, U)` if `x.0` is safe for `T` and `x.1` is safe for `U`.
32 As far as enums is concerned, for example `x` is safe for `Option<T>` if either the discriminant is `None`, or it is `Some` and the data is safe for `T`.
33 Similarly, `x` is never safe for `!` -- there just is no valid discriminant that `x` could have.
35 When we talk about integer types like `i32`, it is tempting to say that *all* data is safe at `i32`.
36 However, that does not actually work: As [I discussed in a previous post]({% post_url 2018-07-24-pointers-and-bytes %}), the "bytes" that make up data have more possible states than just `0..256`.
37 In particular, they can be uninitialized (`undef` or `poison` in LLVM).
38 Some operations like `if x != 0 { ... }` are undefined behavior if `x` is uninitialized, so sticking with our theme that the safety invariant must be strong enough to support safe execution of safe code, we have to declare that `x` is only safe at `i32` if it is initialized.
40 For reference types, some of the details are [harder to define]({% post_url 2018-04-05-a-formal-look-at-pinning %}), but we can still roughly say that a pointer is safe for `&'a mut T` if it is aligned, non-NULL and points to allocated memory that, for lifetime `'a`, no other pointer accesses, and such that the data stored in memory at that location is safe for `T`.
41 Similarly (and [ignoring interior mutability]({% post_url 2018-01-31-sharing-for-a-lifetime %})), a pointer is safe for `&'a T` if it is aligned, non-NULL and points to allocated memory that is not mutated for lifetime `'a` and such that the data stored in memory is safe for `T`. The safety of `&bool` that we discussed above is just an instance of this general definition.
42 In particular, it is impossible to have a safe `&!` because it would have to point to a safe `!`, which does not exist.
44 The safety invariant gets particularly interesting for higher-order data like function pointers or trait objects.
45 For example, when is `f` safe at type `fn(bool) -> i32`?
46 We can again figure this out by asking: What can safe code *do* with `f`?
47 The only thing safe code can do is call the function!
48 So, `f` is safe at `fn(bool) -> i32` if, whenever you call that function with data that is safe at `bool`, the function runs without causing undefined behavior, and *if* it returns (as opposed to diverging or unwinding), then it returns data that is safe at `i32`.[^1]
49 This generalizes to arbitrary function types in the expected manner.
51 [^1]: This is not fully precise yet; beyond the return value we also have to take into account side-effects that might be observable by other functions. But those details are not the point of this post.
53 ### Custom Safety Invariants
55 So far, we have talked about built-in types only.
56 However, safety invariants become really interesting once we talk about user-defined types.
57 A key property of the Rust type system is that *users can define their own safety invariants*.
58 (This is by far not exclusive to the Rust type system, of course, but it is a property *not* covered by the usual discussions about "type soundness". See [this talk by Derek Dreyer](https://www.youtube.com/watch?v=8Xyk_dGcAwk) if you want dive a bit deeper.)
60 To pick one example (that I already used in [one of my first blog posts]({% post_url 2016-01-09-the-scope-of-unsafe %})), let us look at `Vec`.
61 `Vec` is roughly defined as follows (the real definition just groups the first two fields together as a `RawVec`):
64 ptr: Unique<T>, // pointing to the heap-allocated backing store holding all the data
65 cap: usize, // number of elements that fit the backing store
66 len: usize, // number of elements that are actually initialized in the backing store
69 From what we said so far, the safety invariant for `Vec<T>` (structurally demanding safety of its fields) would be not very useful -- `Unique<T>` is just a non-NULL raw pointer, and `usize` can be anything initialized.
71 For `Vec` to work, however, `ptr` will be pointing to valid memory of size `cap * mem::size_of::<T>()`, and the first `len` items in that memory must be safe at `T`.
72 This is an invariant that all the unsafe code implementing `Vec` maintains, and it is the invariant that the safe API surface of `Vec` expects the outside world to uphold.
73 The reason this works is that the fields mentioned in this invariant are all private, so safe code cannot break the invariant and use that broken invariant to cause havoc.
74 Again, the safety invariant is about ensuring safe execution of safe code.
75 Unsafe code can of course break this invariant, but then it is just Doing It Wrong (TM).
77 Thanks to privacy and an abstraction barrier, types in Rust can define *their own safety invariant*, and they can then expect the outside world to respect that invariant.
78 As we have seen with `Vec`, when generic types are involved, these custom safety invariants will often have a "structural" element in that being safe at `Vec<T>` is defined in terms of being safe at `T`.
80 ## An Invariant for the Compiler
82 We want the compiler to make *some* type-based assumptions about data -- in fact, we already do that: `Option<bool>` is stored in a way that exploits that `bool` only has two possible values.
83 When passing around an `enum` with `repr(u32)` (or any other integer type), we tell LLVM that it may assume the value to be one of the enum variants.
84 For reference types, we tell LLVM that they are always aligned and dereferencable.
85 And there are probably more of these attributes we are using that I am not aware of.
87 So, we need an invariant that the compiler may assume *always* holds, justifying the optimizations we are already doing (and more we want to do in the future).
88 There is no *a priori* reason that the invariant the compiler relies on is the same as the safety invariant that safe code relies on.
89 To make it easier to talk about this distinction, let us call the compiler-facing invariant *validity*, so that we can ask if some data is *valid at type `T`*.
90 Because the compiler assumes that all data is always valid at its given type, we make it instantaneous undefined behavior to ever violate validity.
92 > *The validity invariant is exploited by the compiler to perform optimizations (e.g. enum layout optimizations).*
94 Now, can't we just say that the validity invariant is the same as the safety invariant, and be done?
95 I think there are several problems with that approach.
97 First of all, notice that for user-defined invariants, this plainly does not work.
98 For example, if you look at [the code that grows a `Vec`](https://github.com/rust-lang/rust/blob/674ef668f13c52a1fadbf01b24d8da1e12d15e70/src/liballoc/raw_vec.rs#L687-L688), you can see that it *first* updates the `ptr` and *then* updates the `cap`.
99 Between these two updates, the safety invariant of `Vec` is violated.
100 But that's okay, because this is carefully controlled unsafe code -- and by the time the `Vec` reaches safe code again, the invariant is reestablished.
101 (And because we can assume there are no data races, there is no problem with concurrency either.)
103 > *Unsafe code only has to uphold safety invariants at the boundaries to safe code.*
105 Notice that the "boundary" is not necessarily where the `unsafe` block ends.
106 The boundary occurs where the unsafe code provides a public API that safe code is intended to use -- that might be at the module boundary, or it might even be at the crate level.
107 That is where safe code should be able to rely on safety, so that it can interact with the unsafe code without triggering undefined behavior, and hence that is where the safety invariants come into play.
109 This is in strong contrast to validity, which must *always* hold.
110 Layout optimizations and LLVM's attributes are in effect throughout unsafe code, so it is never okay to ever have invalid data.
111 (With the sole restriction of data which *the compiler statically knows is not initialized*: If you write `let b: bool;`, that data in `b` is kept inaccessible *even to unsafe code*, and it does not have to satisfy any invariant. This works because the compiler knows about `b` not being initialized.)
113 > *Unsafe code must always uphold validity invariants.*
115 So we clearly cannot just pick the same invariant for both, or else it would be impossible to write `Vec`.
116 We *might* want to just ignore user-defined invariants when it comes to validity, but I think that would be ill-advised.
118 First of all, validity is part of the definition of undefined behavior.
119 I think we want to eventually check for as much undefined behavior as is possible, and when we define undefined behavior, we should strive to make it as "checkable" as we can.
120 If you go back up and look at safety for types like `fn(bool) -> i32`, you can see that this is inherently *not* checkable -- checking if `f` is safe at `fn(bool) -> i32` requires solving the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)!
122 Moreover, when I did my [evaluation of Types as Contracts last year]({% post_url 2017-08-11-types-as-contracts-evaluation %}) (which made an attempt to enforce a fairly strong invariant, albeit still weaker than how we defined safety above, throughout the entire program execution), I found plenty of cases of unsafe code temporarily violating the safety invariant.
123 For example, `Arc`'s destructor calls [`Layout::for_value`](https://doc.rust-lang.org/beta/std/alloc/struct.Layout.html#method.for_value) with a reference to a struct that contains a deallocated `Box`.
124 Plenty of unsafe code passes around `&mut T` where the `T` is not yet fully initialized.
125 We *could* decide that all of that code is incorrect and should use raw pointers, but I think it is too late for that.
127 ## Validity Invariants
129 Instead, one thing I would like to do in the near future is get a better understanding of what our validity invariants are.
130 First of all, this is a topic that comes up again and again in unsafe code discussions.
131 Secondly, because validity invariants are supposed to be checkable, we can talk about them *precisely* without having to give everyone PhD-level courses in separation logic (if you read my previous posts on invariants, some of which I linked to above and which were all about safety invariants[^2], you know what I mean).
132 We can just talk about which checks one would have to do e.g. in Miri to enforce the invariant.
133 And finally, validity invariants have "wiggle room".
135 [^2]: I am aware that I inadvertently used the term "valid at type `T`" in those prior posts. It is hard to come up with consistent terminology...
137 With that last point, I mean that we can make a conservative choice now (making as few things valid as we can), and later expand the amount of data we consider valid without breaking existing code.
138 Weakening the invariant can only lead to code that used to have undefined behavior, now being well-defined.
139 This is in contrast to safety invariants, which we cannot weaken or strengthen -- some unsafe code might *consume* data assuming the invariant and hence break if we make it weaker, another piece of code might *produce* data that must satisfy the invariant and hence break if we make it stronger.
141 So, let us look at some examples, and how the validity invariant is constrained by optimizations that we are already performing.
142 If Rust's layout algorithm exploits an invariant for enum optimizations (e.g. `Option<&i32>`), then our hands are bound to make that part of validity or that layout is just incorrect.
143 As already mentioned, we also pass on a bunch of attributes to LLVM telling it about various things we know, based on the variable's type.
144 And finally, all safe data must also be valid, so the safety invariant also imposes a constraint.
146 For `bool`, we stick to the same invariant as for safety: It must be `true` or `false`.
147 This invariant is already exploited by enum layout optimizations, so violating it *at any time* can break your code.
148 More generally speaking, validity requires correct enum discriminants.
149 One consequence of this is that no data is valid at `!`.
151 Similar to safety, validity is structural -- so validity for `(T, U)` requires that the first field is valid at `T`, and the second field is valid at `U`.
153 What about references?
154 This is where it gets interesting.
155 For a type like `&i32`, we tell LLVM that it is aligned and non-NULL, and we exploit some of that with enum layout optimizations, so that is something validity must require.
156 But do we want to require that an `&bool` *always* points to a valid `bool`?
157 As the examples I mentioned in the previous section showed, there is unsafe code out there that this would break (and people bring up examples for this every time uninitialized data is discussed).
158 It is often useful to be able to call a method that takes `&mut` on a partially initialized data structure *if you know what that method does because it is part of the same crate*.
159 Doing all that with raw pointers is much less ergonomic, and making people write less ergonomic code will inadvertently lead to more bugs.
160 Moreover, the *benefits* of making this validity for reference structural (i.e., `&T` is valid only if it points to a valid `T`) seem slim (though @comex [came up with an optimization that would require this](https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153/25?u=ralfjung)).
162 A consequence of this is would be that while `&!` does not have a safe inhabitant, it *is* possible to have data that is valid for `&!`.
163 After all, it does not have to point to a valid `!` (which would be impossible).
165 One point that we *already* assume, however, is that references are dereferencable.
166 We even tell LLVM that this is the case.
167 It seems natural to make that part of validity.
168 However, it turns out that if we [adapt Stacked Borrows]({% post_url 2018-08-07-stacked-borrows %}), we do not need to: The aliasing model already implicitly enforces all references to be dereferencable (concretely, references get "activated" when they come in scope, which affects "shadow data" that is stored together with each byte in memory and can only succeed if the reference points to allocated memory).
169 For theoretical reasons, I would like not to make dereferencability part of validity.
170 I think it is desirable if a value that is valid at some point, will always be considered valid for the rest of program execution.
171 That is true for invariants like "a `bool` must be `true` or `false`", but it is not true when we also require a reference to be dereferencable and then that memory gets deallocated.
172 On some level, it doesn't even matter where this fact that references are dereferencable comes from, so I should probably not waste as much space on this discussion. ;)
174 Another interesting case is validity of a `union`.
175 This has been [discussed a lot](https://github.com/rust-lang/rust/issues/32836#issuecomment-406872221), and my personal opinion is that validity makes no restrictions whatsoever for a `union`.
176 They do not have to be valid according to any one of their variants, and can contain arbitrary (even uninitialized) data -- but no firm decision has been made yet.
178 As one last example, there are open questions even around the validity for types as simple as `i32`.
179 When we talked about safety, I explained that uninitialized data is *not* safe at `i32`.
181 My gut feeling is that it should not be (i.e., validity should require that `i32` be initialized to *some* value), but I cannot demonstrate any tangible benefit and [there are good examples for allowing uninitialized data in a `u8`](https://github.com/rust-lang/rfcs/pull/1892#issuecomment-412262716).
185 I have talked about two kinds of invariants that come with every type, the safety invariant and the validity invariant.
186 For unsafe code authors, the slogan summarizing this post is:
188 > *You must always be valid, but you only must be safe in safe code.*
190 I think we have enough experience writing unsafe code at this point that we can reasonably discuss which validity invariants make sense and which do not -- and I think that it is high time that we do so, because many unsafe code authors are wondering about these exact things all the time.
192 The plan is to open issues in the [UCG RFCs repo](https://github.com/rust-rfcs/unsafe-code-guidelines/) soon-ish, one issue for each type family that we need to make decisions on wrt. validity.
193 Meanwhile, if you have any comments or questions, feel free to join us in the [forum](https://internals.rust-lang.org/t/two-kinds-of-invariants/8264)!
projects / web.git / blob