2 title: "Two Kinds of Invariants"
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 us 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 This is in strong contrast to validity, which must *always* hold.
106 Layout optimizations and LLVM's attributes are in effect throughout unsafe code, so it is never okay to ever have invalid data.
108 > *Unsafe code must always uphold validity invariants.*
110 So we clearly cannot just pick the same invariant for both.
111 We *might* want to just ignore user-defined invariants when it comes to validity, but I think that would be ill-advised.
113 First of all, validity is part of the definition of undefined behavior.
114 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.
115 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)!
117 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.
118 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`.
119 Plenty of unsafe code passes around `&mut T` where the `T` is not yet fully initialized.
120 We *could* decide that all of that code is incorrect and should use raw pointers, but I think it is too late for that.
122 ## Validity Invariants
124 Instead, one thing I would like to do in the near future is get a better understanding of what our validity invariants are.
125 First of all, this is a topic that comes up again and again in unsafe code discussions.
126 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).
127 We can just talk about which checks one would have to do e.g. in Miri to enforce the invariant.
128 And finally, validity invariants have "wiggle room".
130 [^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...
132 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.
133 Weakening the invariant can only lead to code that used to have undefined behavior, now being well-defined.
134 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.
136 So, let us look at some examples, and how the validity invariant is constrained by optimizations that we are already performing.
137 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.
138 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.
139 And finally, all safe data must also be valid, so the safety invariant also imposes a constraint.
141 For `bool`, we stick to the same invariant as for safety: It must be `true` or `false`.
142 This invariant is already exploited by enum layout optimizations, so violating it *at any time* can break your code.
143 More generally speaking, validity requires correct enum discriminants.
144 One consequence of this is that no data is valid at `!`.
146 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`.
148 What about references?
149 This is where it gets interesting.
150 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.
151 But do we want to require that an `&bool` *always* points to a valid `bool`?
152 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).
153 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*.
154 Doing all that with raw pointers is much less ergonomic, and making people write less ergonomic code will inadvertently lead to more bugs.
155 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)).
157 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 `&!`.
158 After all, it does not have to point to a valid `!` (which would be impossible).
160 One point that we *already* assume, however, is that references are dereferencable.
161 We even tell LLVM that this is the case.
162 It seems natural to make that part of validity.
163 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).
164 For theoretical reasons, I would like not to make dereferencability part of validity.
165 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.
166 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.
167 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. ;)
169 Another interesting case is validity of a `union`.
170 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`.
171 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.
173 As one last example, there are open questions even around the validity for types as simple as `i32`.
174 When we talked about safety, I explained that uninitialized data is *not* safe at `i32`.
176 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).
180 I have talked about two kinds of invariants that come with every type, the safety invariant and the validity invariant.
181 For unsafe code authors, the slogan summarizing this post is:
183 > *You must always be valid, but you must not always be safe.*
185 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.
187 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.
188 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