Documentation should only refine types (or why Pin::get_unchecked_mut is a ticking bomb)

language design Unsafe Code Guidelines
21

you can't safely convert from Pin<&mut T> to &mut T

Sorry, that was abusive notation. In the original post I used &'static mut T to avoid this concern and then dropped it for simplicity. All posts are written with &'static mut T in mind.

Line 6 is UB, but wouldn't be UB if not for line 5. However, the only unsafe code is the conversion on line 4, so the UB has to be attributed to the conversion. That's equivalent to saying that the conversion has the safety postcondition "don't access the returned reference after deallocating it".

I think this example is a pre-condition. The unsafe code violates the pre-condition.

/// Pre: ptr is non-null, aligned, and dereferenceable
/// Pre: *ptr is initialized and satisfies aliasing for &'a
unsafe fn as_ref_unchecked<'a>(ptr: *const i32) -> &'a i32;
// There is no lifetime that simultaneously satisfies the drop and println lines.

one example is Rc::get_mut_unchecked

This is not a (low- to high-level) conversion function per se. An Rc<T> points to an RcBox<T>, not a T, so we don't just change the type, we also change the pointer value. But I don't think it really matter for the concern of examples where a post-condition extends a type. I also think in this case it's a pre-condition.

/// Pre: *this.as_ptr() satisfies aliasing for &'a mut
unsafe fn get_mut_unchecked<'a>(this: &'a mut Rc<T>) -> &'a mut T;

Similarly for RefCell::try_borrow_unguanded.

Note that those examples don't restrict what you can do with the result, but what you can do with the input. While Pin::get_unchecked_mut restricts what you can do with the result. It's not stated as a property of the input (in particular the correct version would say "the pointed content is actually not pinned" but that would be a different semantics and not solve the intent of why get_unchecked_mut exists).

the UB would be caused immediately at the point of conversion

Yes, I'd argue that. (Note that it's not because UB happens there, that it's visible there at runtime.)

But that reasoning is only valid if lifetimes affect runtime semantics

I'm not sure what runtime semantics mean. Lifetimes affect semantics indeed, this is why we can say [&'a mut T] ⊆ [&'b mut T] if 'a outlives 'b. If they did not affect semantics then those would be the same set of behaviors.

it would be too unpredictable and difficult to reason about for unsafe code authors

That's an interesting point. I'm curious to know more about this, because in my opinion, if we say that unsafe authors shouldn't need to reason about lifetime, then we essentially cancel the notion of lifetime which is one of the most powerful tool of Rust.

given an &mut str, you can call the unsafe as_bytes_mut to get an &mut [u8]

This is a very interesting example. I think this is a valid example that builds on the RustHorn idea to describe the end value when borrowing.

Let's look at its different properties:

  • This is a high- to low-level conversion function.
  • High- to low-level conversion functions may have post-condition refining their result to still allow round-tripping back to the high-level version (e.g. from NonNull<T> to *mut T we need the post-condition that *mut T is non-null otherwise we can't go back) but this doesn't make the function unsafe, it is just additional information.
  • High- to low-level conversion functions are usually safe. However here, the round-trip is automatic due to the temporary borrow. So we have to prove during the high- to low-level conversion that the low- to high-level conversion is valid (because it happens automatically at the end of the borrow). This is what the post-condition is doing.
  • However, the post-condition still refines the type. Being valid UTF-8 at end of lifetime restricts the set of behaviors of &mut [u8]. So we are still refining the type.
/// Post: result must be valid UTF-8 at end of lifetime
unsafe fn as_bytes_mut(self: &mut str) -> &mut [u8];
// [&mut str].typ ⊆ [&mut [u8]].doc ⊆ [&mut [u8]].typ

Because you can always safely forget that the slice must be valid UTF-8 at end of lifetime, you can safely call functions taking &mut [u8].

I'll try to write a summary of the thread in the original post because my initial worry is solved by Ralf's blog post. We are now discussing a less important part of my worry (that I didn't expect existed in Rust, but I see why it's a pragmatic choice, and my dream language is probably yet to come and will learn from Rust's experience, might be a future Rust edition).

22

I updated the original post with a summary of the thread. Note that for me, the most concerning aspect was [T].doc ⊆ [T].val and this is already true. The rest is much less important and just about optimization. So on my side, this could be closed. But I'm happy to discuss the optimization limitations in case there's something I still don't understand.

23

... No? What you can do is temporarily put non-UTF-8 in the buffer, but it must be valid UTF-8 when the borrow expires and the &mut str is usable again.

This isn't the case, though. UB can time travel, so saying "when" it happens is difficult, but it cannot travel over a synchronization point.

let mut rc = Rc::new(BigData::new());

let r = Rc::get_mut_unchecked(&mut rc);

// A

if prompt_user("cause issues on purpose?")? {
    // B
    drop(rc);
    // C
}

// D

dbg!(&*r);

// E

Here at point A, no UB is present. If the user declines to cause issues, we dbg! the BigData, drop the Rc, and exit. If the user chooses to cause issues, we have UB.

This is a valid transformation of the program which maintains semantics (as allocation is not considered observable), and in fact does not reduce UB at all:

if prompt_user("cause issues on purpose?")? {
    unreachable_unchecked();
}

let mut rc = Rc::new(BigData::new());
let r = Rc::get_mut_unchecked(&mut rc);
dbg!(&*r);

Whether there is UB is a dynamic question (is the reference used after (any clone of) the rc is touched), and not a static question. Lifetimes are an annotation that are used to control what safe code can do, and thus can be used to create a sound interface which cannot be used to cause UB, but they have no impact on on program semantics.

Just as a silly example, it's perfectly sound to do get_mut_unchecked::<'static> to get &'static mut T, so long as the reference is only used in regards to the unsafe invariants. Lifetimes are a property of a sound API, but not of any execution.

I think you're missing a word there, I don't understand what you're trying to say.

There's two levels here. There's the operational semantics of the Abstract Machine. This is what is used to define what actually happens when you follow any given execution of the program; the runtime semantics. The Abstract Machine as currently defined has no concept of lifetimes at all! (And the concrete machine (the actual CPU) definitely doesn't.) Instead it just says when an operation is valid, and when an operation is invalid (and an invalid operation is Undefined in the math sense). You might be interested in reading RalfJ's overview(s) of the Stacked Borrows model for the Abstract Machine's memory model / reference semantics.

Then at the API level (which seems to be the one you're exclusively considering) there's the static semantics of a type, which encompass every possible thing you can do. (It's not true in practice[1], but it's a useful comparison to pretend that) *mut T and &mut T have the same operational semantics; what is a valid operation on one is also valid on the other*. The difference is purely* in the static semantics: what you can do with the value in purely safe code, and thus the bounds on unknown code which allow you to write a sound API implemented with unsafe code.

To reiterate: lifetimes are a property of an API. They are a tool for constraining how someone (is told they) can use an API. But below the static API definition is the actual implementation details; these details are encapsulated in the sound API, but the details purely care about maintaining the soudness of operational semantics (over all possible safe uses of the API).

When using APIs these are quite often the same thing (because the upstream API can change its own encapsulated details within what the API describes, so you can't rely on implementation details), but the core language semantics itself need be more strongly written such that there is room to write any unsafe code at all.

  1. the difference is in how they're lowered to the Abstract Machine; *mut T uses a Raw Stacked Borrows tag, and &mut T uses a Uniq Stacked Borrows tag; additionally, dealing &mut T inserts Retag operations that aren't present with *mut T. ↩︎

2 Likes
24

Yes, forgetting that the slice must be valid UTF-8 at end of lifetime doesn't change the fact that it is valid UTF-8 at end of lifetime. Look at the implementation of str::make_ascii_lowercase:

fn make_ascii_lowercase(self: &mut str) {
    // SAFETY: safe because we transmute two types with the same layout.
    let me: &mut [u8] = unsafe { self.as_bytes_mut() };
    me.make_ascii_lowercase()
}
// For reference, the type of <&mut [u8]>::make_ascii_lowercase:
fn make_ascii_lowercase(self: &mut [u8]);

Let's ignore the safety documentation, it looks outdated. The correct safety documentation would be: safe because we only call <&mut [u8]>::make_ascii_lowercase which only changes ascii bytes to ascii bytes which preserves UTF-8 validity.

To be able to call <&mut [u8]>::make_ascii_lowercase we need to forget that we have a documented &mut [u8] because this function takes a &mut [u8] without documentation. Note however, that although this function doesn't have a safety documentation, it has a correctness documentation (essentially a post condition that all bytes in [A-Z] are mapped to [a-z]). And this correctness documentation is critical to prove the that calling str::as_bytes_mut is safe (i.e. its post-condition is satisfied).

Here at point A, no UB is present

The program doesn't pass the borrow-checker. You can't drop rc while holding a reference.

Whether there is UB is a dynamic question

Yes and no. It depends on the statement:

  • An execution triggers UB. This is indeed dynamic.
  • A program has UB. This is static. It means that at least one execution triggers UB.

In the case you describe there's 2 options depending how the program is documented:

  • It is documented that the user is not allowed to answer yes to the prompt. In that case, the program is well-defined (it has no UB).
  • The user behavior is not documented. In that case the program has UB on second line, because there are execution paths that reach this point and that line explicitly says it's UB if it's reached.

Lifetimes are an annotation that are used to control what safe code can do, and thus can be used to create a sound interface which cannot be used to cause UB, but they have no impact on on program semantics.

I totally agree with that but at the same time I think this is where we have different opinions (and mine is probably too theoretical). I would put it this way: Lifetimes are a part of the type system. As such, they describe the semantics of programs. They don't change how programs run though because they are not part of programs. I think our opinion differs in the way we look at type system features:

  • In your case, this is a way to prevent behaviors such that safe code stays safe. That's why you mention types (and lifetimes) as being part of the API. And I agree with this, that's one way to see types (and lifetimes).
  • In my case, I mostly see types (and lifetimes) as a way to describe the possible set of behaviors of a program. If someone uses the program by only assuming that it satisfies its type (i.e. it can have any behavior described by the type and none outside), then that usage is safe.

In the end I think both opinions are just the two sides of the same thing. It depends on what we focus. In your case you focus on how something is used. In my case I focus on what it is.

Just as a silly example, it's perfectly sound to do get_mut_unchecked::<'static> to get &'static mut T, so long as the reference is only used in regards to the unsafe invariants. Lifetimes are a property of a sound API, but not of any execution.

In my opinion, get_mut_unchecked::<'static> is only sound if only the returned pointer is used to access the content from now on. The programmer must prove this when calling get_mut_unchecked as part of the safety documentation. I'm not sure what you mean by "lifetimes are not a property of any execution". I would instead say: lifetimes describe a property of pointers for all executions.

I mean that if there is UB at a given code location, it doesn't necessarily mean that something bad (like a crash) happens when reaching that code location. Something bad may not happen, may happen before, or after, because the whole program is possibly mis-compiled.

Then at the API level (which seems to be the one you're exclusively considering) there's the static semantics of a type

Yes, by semantics I mean what you call static semantics. And it is defined using the operational semantics (which I call behavior). I like that you use the word API, because API is a contract between 2 things. And types (and lifetimes) are indeed a contract. Except that in your case it's a contract between 2 programmers (the implementer and the user). In my case it's a contract between the program and its context:

  • The program says "I have this type", which means that it cannot have more behaviors than the semantics of the type.
  • The context says "I support this type", which means that it is well-defined for all behaviors in the semantics of the type.

the details purely care about maintaining the soudness of operational semantics (over all possible safe uses of the API).

I believe that this is only possible if the API is correct, i.e. its semantics contains all possible behaviors of the implementation. I'm assuming the language is powerful enough to distinguish all disjoint sets of behaviors. This might actually not be true in practice. I'm curious to see an example though because I believe that if no context can distinguish between 2 disjoint sets of behavior then the difference between those sets is probably not relevant in practice since it won't affect any execution.

the core language semantics itself need be more strongly written such that there is room to write any unsafe code at all.

I don't understand what you mean here. Do you have an example?

25

A simple restatement should suffice: if you are only allowed to use the safe APIs as the safe APIs describe, there is no room for unsafe use of the APIs. If you have [T].typ == [T].doc == [T].val, there is no room to write unsafe using the type (because all valid behaviors are safe).

This is in active disagreement with most unsafe code authors. The use of &'static as an "'unsafe" alternative is not uncommon. I think we've also blessed Box::from_raw(Box::leak(x)) as not UB? (Though we would still prefer if you used Box::into_raw and don't quote me on this.)

26

If it's currently valid UTF-8, then sure, you can forget about the slice entirely and it will still be valid UTF-8 at the end of the lifetime. I guess you could also convert it to an immutable slice and forget about the rule. But if you plan to keep using the slice as mutable, you can't forget about the "must be valid UTF-8 at end of lifetime" rule.

By the same token, if you have a reference returned by Pin::get_unchecked_mut, you can always forget about it entirely. But if you plan to keep using the reference, you can't forget about the "must drop before repurposing memory" rule.

That said… I suppose there is a clear difference between the two. str::as_bytes_mut is converting from "unique reference to subtype" to "unique reference to supertype" (or as you'd say, from a higher-level representation to a lower-level one). It makes sense that you would have to make sure the memory satisfies the subtype again before the borrow expires. But Pin::get_unchecked_mut seems to be converting from "unique reference to supertype" to "unique reference to subtype", at least in the special case of Pin<&'static mut T> where "pinned T" is guaranteed to be a subtype of "non-pinned T" (because you can safely convert from the latter to the former with Pin::static_mut). Surely, when converting from "unique reference to supertype" to "unique reference to subtype", the validation can happen at the point of conversion?

Well, no, because Pin<&mut T> is not a unique reference. The Drop rule exists precisely because such types may have extra references to them from the outside.

From the compiler's perspective, any mutable reference to an !Unpin type is non-unique, and Pin has nothing to do with it. But safe code that has a mutable reference is allowed to perform operations on it like mem::swap or even take_mut, which only make sense if the reference is unique. (The data also must be movable, but that's a separate issue.) So from a "safety invariant" perspective – that is, in this case, what unsafe code must guarantee before calling arbitrary safe code – &mut T is unique and Pin<&mut T> is not.

So Pin::get_unchecked_mut actually converts from "non-unique reference to supertype" to "unique reference to subtype" (again, assuming 'static). This is similar to Rc::get_mut_unchecked, which effectively converts from "non-unique reference to type" to "unique reference to type". In both cases, it's unsound to pass the returned &mut T to arbitrary safe code if there are any other aliasing references that might potentially be used simultaneously. There are some differences. Pin::get_unchecked_mut changes the pointee type; Rc::get_mut_unchecked does not. Rc::get_mut_unchecked typically requires the entire object to be uniquely referenced; pinned types can have parts of them be uniquely referenced and parts not.

But in both cases, since the returned reference is not really unique (despite having a type saying it is), it's not as simple as being able to temporarily do whatever you want with the memory as long as you put it back before the borrow expires. You have an additional obligation, or postcondition, to avoid conflicts with other aliasing references. And that applies for the entire duration of the borrow, not just its start and end.

…Or at least, that's one way to interpret it. Just like with raw-pointer-to-reference conversion, you could counter-argue that Rc::get_mut_unchecked expresses its requirement in its type signature through the returned lifetime; as mentioned before, we don't want inferred lifetimes to affect runtime semantics, but there's at least some sort of moral equivalence. From that perspective, Pin::get_unchecked_mut really is the odd one out.

But perhaps that oddity is an illusion caused by the fact that Rust doesn't idiomatically use shared mutable references. We do have semantically similar types, such as Rc<RefCell<T>>. And you could imagine unsafe conversions from Rc<RefCell<SubType>> to Rc<RefCell<SuperType>> or vice versa. If Rust hypothetically did idiomatically use shared mutable references, there might be a lot of functions taking Rc<RefCell<T>>, and this type of conversion might be necessary in order to call one. In either conversion direction, the returned pointer would be valid for some uses, but would have a obligation lasting for its entire lifetime. When converting from Rc<RefCell<SubType>> to Rc<RefCell<SuperType>> , you must not perform operations through the converted reference that would make the data invalid for SubType. When converting from Rc<RefCell<SuperType>> to Rc<RefCell<SubType>>, if you perform an operation on another reference that causes the data to be invalid for SubType, you must cease performing any operations through the converted reference. Those are fairly analogous to the requirements for Pin::unchecked_mut, I think.

1 Like
27

Ok, I think I came up with an example. Tell me if that's what you had in mind.

Let's assume the user wants to write this (for some reason the first 2 lines can't be swapped):

fn foo(xs: &mut Vec<u8>, n: usize) {
    let ys = &mut xs[.. n];
    xs.truncate(n);
    ys.make_ascii_uppercase();
}

There should be a sound way to do this by using unsafe. One way is to use the "raw parts" unsafe API of Vec and reimplement truncate. But let's assume that Vec only had its safe API (since if I understand correctly, you argue that it should be possible to use unsafe on top of a safe API). So the user would write something like:

/// Pre: xs must look like &mut Vec<T> except for the first n items which may alias
unsafe fn truncate_unchecked<T>(xs: *mut Vec<T>, n: usize) {
    // Safe: Only used to call truncate which doesn't touch the first n items.
    // (Note that this relies on the correctness documentation of truncate.)
    let xs = unsafe { &mut *xs };
    xs.truncate(n);
}

And then they would update their function to use this version of truncate:

fn foo(xs: &mut Vec<u8>, n: usize) {
    let p: *mut Vec<u8> = xs;
    // Safe: No previous alias.
    let ys = &mut unsafe { &mut *p }[.. n];
    // Safe: Only the first n items are previously aliased.
    unsafe { truncate_unchecked(p, n) };
    ys.make_ascii_uppercase();
}

And this actually passes Miri. Here are the playground links:

  • before doesn't compile
  • after compiles and passes Miri

(EDIT: Just realized that Vec<u8> is not the best example because u8 is trivially dropped. Here is a similar playground using Vec<Box<u8>> and introducing a bug caught by Miri, to make sure the code is not sound for unexpected reasons.)

So I think I see why you argue that one might want typ ⊊ val for an API. I agree that this provides flexibility. However, I would weakly argue that this is more of a matter of API design. Let's use the following definitions:

  • impl is the semantics of your existing implementation
  • uses is the semantics that existing usages rely on
  • union is the union of the semantics of all your implementations (past, current, and future)
  • inter is the intersection of the semantics of all possible usages you want to support (past, current, and future)
  • safe is the semantics of your safe API
  • unsafe is the semantics of your unsafe API
  • EDIT: valid is the validity semantics of your safe API

You have impl ⊆ union ⊆ inter ⊆ uses and unsafe ⊆ safe. You want to pick unsafe such that union ⊆ unsafe ⊆ inter, i.e. you won't break your unsafe API when improving your implementation and you won't need to change your unsafe API to support all your users (past, present, and future). Once you picked unsafe, you pick safe as the smallest safe API on top of unsafe. You might end up in 2 scenarios:

  • safe ⊆ inter in which case you don't need an unsafe API and may just provide the safe API
  • safe ⊈ inter in which case you need the unsafe API for users who actually need some behaviors to be absent of your API but which are in your safe API, i.e. safe \ inter.

EDIT: Currently, you pick safe such that usage is sound. You get valid for free. You probably have valid ⊆ safe but functions that return Self make it more complicated. If valid is still too high, then you need to pick unsafe ⊆ valid ∩ safe to support all users (including unsafe ones).

What does this have to do with the Vec::truncate example? I believe that the user (in particular in a world where typ = val), instead of implementing their own truncate_unchecked unsafe function on top of the safe truncate function, should have contacted the Vec implementer to ask for a truncate_unchecked function. There could have been 2 answers:

  • You should use the "raw parts" API. This unsafe API gives you the union semantics so you can do anything sound. This is not a nice answer because the user still has to implement its own truncate from the raw parts.
  • Oops, we forgot to add it to our unsafe API (because we wrote the safe API first). They add truncate_unchecked with the same definition as truncate and make the definition of truncate simply call the unsafe version with a simple safety proof that the whole vector is not aliased which trivially implies the pre-condition of the unsafe function.

I would argue that API designers should think about the unsafe API first. The safe API is just a trivial wrapper around the unsafe API. I agree this is harder to do and being able to avoid that looks appealing, which is apparently the current convention in Rust: just focus on the safe API, and because typ ⊊ val anyway, most unsafe usage can be implemented on top of the safe API. The drawback being that Rust is now only a low-level language because of that, i.e. its high-level types are just used for soundness and not for all the optimizations they could. I think this is still a good situation. In particular given that so early in the design of Rust, after-the-fact flexibility for users is much more important than optimizations.

I see, so that would be another example where typ ⊊ val, i.e. the compiler can't use lifetimes to optimize. If we ever want to improve this, we would need a new notion of lifetime with a semantics that have to describe all behaviors. Probably not necessary or urgent (as with the &mut vs Pin difference or any other typ ⊊ val examples) given the other difficulties that Rust is facing.

28

Does it pass miri if you use -Zmiri-tag-raw-pointers?

29

Yes, -Zmiri-tag-raw-pointers doesn't change the outcome:

  • The Vec<Box<u8>> version with n - 1 triggers UB according to Miri (explicit bug to make sure we don't have something that trivially passes)
  • The Vec<Box<u8>> version with n doesn't trigger UB according to Miri
1 Like
30

That is a different kind of flexibility. Yes, the language provides the user a lot of choice about which promises the user makes to the language.

But, entirely orthogonal to that, the language also lets the user see basically everything. This is about the promises the language makes to the user. I can just take my MaybeUninit<u8> and go look at the secret parts of any type, and the language is fine with that. If I ensure that the byte is initialized, I can do assume_init() and start checking its bits. And the result of that has to be consistent, i.e., if I do this multiple times with the same "value" (e.g. the same &mut) I have to get the same result.

Your proposal violates that property. Your proposal only works in languages where users cannot "see" things like how a pointer/reference is actually represented on the machine.

Your are talking entirely past me here. My argument has nothing to do with Pin.

I think I see what you mean.

How would you feel about the third answer (which is usually what we do): refine the documentation of truncate to explain in which extra circumstances (that are not clear from its type signature) it can be used as well.

This has the advantage of avoiding duplication of code and API surface.

I still don't quite see how this could be useful for optimizations, given just how much is observable in Rust. This feels like you almost want optimizations on the level of Haskell where you can define equations that code must satisfy and the compiler will just rewrite with these equations. That is awesome, but it also makes it super hard to detect UB in the resulting code, since we'd basically have to verify that these equations hold (which is undecidable).

Basically, somewhere further down this road lies an axiomatic semantics much like that of C, where we make a bunch of high-level statements (equations, of sorts) that are supposed to hold true and then have fun making sure they are all true. (In the case of C, I think the resulting axiomatic system is both unsatisfiable and also not specific enough to be useful.) That's why in Rust we are thinking of the fundamental language specification in a very operational way, like an interpreter -- like Miri. The compiler is then required to perfectly implement that interpreter, except that it may assume that the program never runs into the "error" conditions that we explicitly classify as UB.

So, this program will always print the same number twice, and no optimization may change that:

fn foo(r: &mut i32) {
  println!("{:p}", r);
}

fn main() {
  let mut x = 5;
  let r = &mut x;
  println!("{:p}", r);
  foo(r);
}

Your proposed optimization of moving the data r points to somewhere else and passing that reference to foo would break this property, and is thus not allowed.

1 Like
31

I think there's some mismatch in the communication. I think it comes from the fact that you take Rust as it is (because your job is to come up with a way, e.g. typ ⊆ val, to explain the current situation), while I look at what it could be, i.e. typ = val = opt (no compromise between flexibility and optimization). Note that I initially naively thought that typ = val = opt until this thread. This is why I initially claim doc ⊆ typ (the statement is of course doc ⊆ val when you don't have typ = val, because you eventually want doc ⊆ opt).

So I totally agree with what you say and describe. This is the current Rust with typ ⊆ val where programmers use &mut T as a low-level type. The language essentially adapts to what the programmers do. So the language can't completely decide where it goes. This is a pragmatic approach, and probably the right one given the current Rust adoption (i.e. we don't believe that programmers can change their code to satisfy typ = val, i.e. use lower-level types like NonNull<T> or *mut T instead of &mut T; maybe such migration is not even possible with a Rust edition change and thus simply out of the question). I guess eventually, a better language will replace Rust. And that's probably also the right approach. We're still figuring out how to do multi-level programming languages. So this thread is just a note for future language designers: specify your language before mass adoption or be ready to break early users (in particular, don't let users rely on compiler implementation details like some code not being optimized).

32

I think that what I said applies not just to Rust as-is but also to Rust how it could be. In safe languages, the language spec has a form of "monotonicity"; you can get away with not spec'ing some details now and then later either expose them to the programmer via some new primitive or starting to exploit it in optimizations. You seem to suggest we could do something similar in Rust. I disagree with that.

In Rust, doing the same is much, much harder -- the Rust spec has no such "monotonicity", because it allows low-level inspection of program state. We have to basically decide about all optimizations up-front, or at least decide about the guarantees unsafe has to uphold that optimizations can be rely on. I do not know of a way to write a precise spec that would still let us discover new guarantees later.

For example, we either have Stacked Borrows (or another aliasing model) or we don't. If we don't have it, and say that's the spec, then we don't get to add it later. Adding it later would impose new requirements on unsafe code, which is a breaking change. This is just a fundamental problem with languages that explicitly support unsafe code. It is not because of some accidental decisions made in Rust in the part.

1 Like
33

I'm not sure what you mean by monotonicity. I don't think I rely on that. Here's how I used to see Rust until this thread:

  1. First comes the calculus, i.e. a grammar and operational semantics for programs. There is no notion of unsafe here, no lifetimes, no types, just low-level code. In particular, because there are no types, traits inference and other type-directed code generation is already resolved.
  2. Then comes the compiler, i.e. a function from Rust calculus to a Target calculus preserving a notion of behavior (usually some bisimulation). Because there are many ways to translate preserving behavior, compilers usually optimize to select the "best" target program (according to some user-chosen criteria like -O3 or -Oz). Note that there are no types yet, compilers optimize a priori with their own whole program analysis (which doesn't work for dynamic libraries and requires LTO for static libraries). This is the most precise information they can get.
  3. Comes the type system, i.e. a grammar and semantics for types, and typing rules for programs. Types classify programs and usually exclude "bad" programs. Typing rules preserve this semantics. Programmers use type checkers to avoid some manual proofs (usually this is all manual proofs, but in Rust this is just some of them). At this stage comes unsafe and lifetimes into play. There's 2 usage of unsafe: in expressions (e.g. unsafe blocks) to mark parts of the program containing manual proofs, and in types (e.g. unsafe functions) to extend the semantics of types (e.g. [unsafe fn(T) -> S] ⊇ [fn (T) -> S]) which can then be refined through documentation. Note that here comes type-directed code generation into play too.
  4. Because type systems are whole-program analyses and compilers are also programs, compilers themselves can be optimized by using type information to optimize faster and better. This of course requires that type information is correct (i.e. if p has type T then p ∈ [T].opt). This also enables library optimization without LTO because types are a contract that communicates whole-program analysis information through the different parts of a program.

In all of this, no monotonicity was used. Programs have a well-defined operational semantics. It is possible to extend the calculus with new constructs but their semantics shouldn't change the semantics of previous programs not using the new constructs. (If one really wants to change the semantics of an existing construct, they just introduce a new one and deprecate the old, forcing users to migrate their code.) Types have well-defined semantics too (with typ = val = opt). There is no wiggle room. It is possible to extend the type system with new types and this won't change the semantics of existing types. (Similarly to programs, to change the semantics of an existing type, a new one may be added deprecating the old one.) Unlike for programs, because types are sets of programs, they naturally come with a notion of sub-typing. As such, new types naturally interact with old types. This permits to migrate at a lower cost.

Now, why is this not somehow restrictive? It is, like all type systems. You might not find the right type for your program such that it type checks. But I think, this is where Rust shines. The unsafe capability of the type systems allows exactly that: if a program doesn't type check although it should (i.e. it is not a "bad" program), the user may lower some types, add documentation, and manually prove the typing rules side conditions. However, this is still somehow restrictive (which is why so much Rust code uses &mut T instead of *mut T). If there are not enough types to chose from (i.e. the type lattice has coarse granularity), then the required documentation and manual proofs might be too big and the user will just rewrite the program differently (like in other programming languages) or just use the wrong types (like now). This is why for my vision to work it is critical to regularly add new types to the lattice as usage demands it (like NonNull<T>, Pin<&mut T>, etc).

A few reasons why I believe current Rust differs from the Rust I describe are:

  • Rust designed safe Rust before unsafe Rust. It should be the opposite (safe Rust is a particular subset of unsafe Rust where proofs are automatisable and automated). This is the same as API design. Library authors should first design their unsafe API (i.e. their real API), then derive their safe API from it (for users who prefer to avoid manual proofs to the price of not being able to write some programs).
  • Rust got massive adoption before providing tools (e.g. Stacked Borrows) to reject programs that are not well-typed (including manual proofs, i.e. unsafe). So ill-typed programs spread uncontrolled and now it is hard to break those programs, so the type system is modified with typ ≠ val to make those ill-typed programs well-typed.
  • Rust needs a good sub-typing story (included bounded sub-typing) such that it is easy to switch between low and high level types, otherwise users won't do it.
34

I think I found what you mean by impossible. We disagree on the definition of flexibility probably. Let me define those terms:

  • accessibility = the number of well-typed programs that don't use unsafe
  • completeness = the number of well-typed programs (regardless of using unsafe)
  • flexibility = completeness - accessibility = the number of additional well-typed programs thanks to unsafe
  • optimization = how much type information the compiler can use

I believe there is a trade-off between optimization and accessibility, and I think that's what you mean:

  • optimization + accessibility = constant

My claim is that there is no trade-off between completeness and optimization, you can take both as big as you want (thanks to unsafe). But by doing so you reduce accessibility. Which is what my proposal is doing. And which is probably why it's not a good idea if Rust wants to remain accessible.

I still believe a language providing enough types can let the programmer choose between optimization (typ = val) and accessibility (typ ≠ val), but the programs written in these different subsets might not interoperate well. This would need concrete examples to check.

35

Also in particular, this defines the requirements that the compiler imposes onto the program -- i.e., it defines when exactly a program has Undefined Behavior.

No, they cannot, unfortunately -- and that seems to be the core of our disagreement. We have unsafe code, and unsafe code is effectively untyped code. If you consider unsafe code to be well-typed, then there are basically no useful invariants to be gleaned from the type system.

(Also, type systems are not whole-program analyses. They are intraprocedural and rely on summaries of other functions, i.e., function types. This is a local analysis; it does not need to see the source code of the entire program at once, only the source code of the local module and the summaries of the rest of the code.)

The only source of information the compiler may use is what has been defined in step 1, in the operational semantics. That's why I keep talking about Rust being different than your usual high-level language without unsafe code.[*] So, the only sense in which the type system helps us do optimizations is indirectly:

  • We can observe that the type system enforces a certain invariant (e.g., aliasing constraints).
  • We can find a way to adjust our operational semantics so that violating that invariant becomes Undefined Behavior. Usually the invariant we implicitly encode here is weaker than what the type system enforces. That's okay, it gives unsafe code some wiggle-room. It's also pretty much necessary since the actual invariant is rather complicated -- to even state the invariant you need something like RustBelt. In contrast, Undefined Behavior is something that we want to be computable/decidable on a given execution; this is required to have tools like Miri.
  • Now the compiler can assume that the invariant encoded by the operational semantics is upheld, and it can optimize based on that invariant.

My Stacked Borrows paper argues this in somewhat more detail. Notice however that once we pinned down the operational semantics, we can no longer do this. That is the "non-monotonicity" that I mentioned.

[*] Well, actually Haskell and OCaml and all the other high-level languages do have unsafe code -- unsafePerformIO, Obj.magic, and so on. They just don't usually talk about it. Which is quite bad if you ask me. But that is a separate discussion.

1 Like
36

Well, actually Haskell and OCaml and all the other high-level languages do have unsafe code -- unsafePerformIO, Obj.magic, and so on. They just don't usually talk about it. Which is quite bad if you ask me. But that is a separate discussion.

I actually think this is the discussion: how to design an automated type system with a sound escape hatch.

There's 2 sorts of sound type systems: automated and manual (i.e. typing relies on manual proofs). Automated sound type systems usually have an escape hatch because they're too restrictive. And there's 2 sorts of escape hatches: sound and unsound (i.e. whether the type system is still sound with the escape hatch). For example:

  • Manual sound type system: C (almost all typing rules have manual conditions, e.g. signed arithmetic should not overflow)
  • Automated sound type system with unsound escape hatch: Haskell, OCaml
  • Automated sound type system with sound escape hatch: Rust

For an escape hatch to be sound, it needs to come with a sound typing rule. And this typing rule requires manual proof by definition of an escape hatch.

In Rust, escape hatches use the unsafe keyword (at least in my dreams) indicating the presence of a manual proof for soundness. They come with a typing rule used to prove the soundness of the type system.

Escape hatches are not eternal. Eventually, after enough research, some coding patterns relying on escape hatches may be automated and thus not need the escape hatch anymore (removing documentation and proofs). Escape hatches are just a way to escape the automated part of the type system. And types is the language that the automated and manual parts of the type system use to agree for soundness (my initial concern for this thread, if documentation doesn't refine types then the manual part doesn't talk the same language as the automated part).

Finally, it's not because proofs are manual that they can't be automatically verified. There's 2 options:

  • Incomplete dynamic check (doesn't need the proof): Miri.
  • Complete static check (needs the proof): RustBelt.

[U]nsafe code is effectively untyped code.

Interesting, that's probably indeed the core disagreement.

I see 2 reasons why unsafe code can be typed:

  • Unsafe is part of the type system, so code can't be unsafe unless we talk about types.
  • If unsafe code cannot be typed, then how would it be possible to prove soundness for programs with unsafe code?

That's probably a terminology issue though.

Note that for me a program is well-typed if the manual proofs are correct (the automated proofs are correct as a theorem). It is possible for a program to type-check but not be well-typed, because the type-checker only checks the automated parts of typing rules. The manual parts of the typing rules still need to hold for the program to be well-typed. This might be a vocabulary problem we have.

type systems are not whole-program analyses

It's probably a terminology issue here too. You can do whole-program analysis with local analyses because you control the interfaces (types and documentation) and can provide arbitrary information from one local analysis to another. It's just a modular way to do whole-program analyses (which is needed for scalability).

The only source of information the compiler may use is what has been defined in [the calculus].

I'm not sure why this is needed. What is the issue with also using type invariants? This is useful to avoid rediscovering stuff (faster compiler).

We can observe that the type system enforces a certain invariant

That's an interesting way to look at it, but I believe it to be equivalent to the compiler assuming that type invariants hold.

We can find a way to adjust our operational semantics [...] Now the compiler can assume that the invariant encoded by the operational semantics is upheld, and it can optimize based on that invariant.

This looks to me that when you think you adjust the operational semantics, you actually adjust the set of sound programs in the type system. In particular, the semantics of all types is included in this set. As such all programs satisfy the invariant you encode. For me, the operational semantics is fixed. It is part of the calculus which preexists the type system. You can adjust everything you want in the type system though, like the set of sound programs (which usually only includes well-defined programs as defined by the calculus, e.g. all their reduction paths end to a value).

37

There is another way to set this all up, and I think it is the way you are proposing. I will use terminology from this article for that.

  • We start with the syntactic type system that Rust has, i.e., what is implemented by the type checker (I include the borrow checker in that).
  • We define a semantic type system that makes precise the invariants maintained by the syntactic type system, and prove its soundness against the syntactic type system.
  • Now we make the semantic type system the "ground truth" and we say that all code, safe and unsafe, must follow the rules of the semantic type system.

This could be done, but I think there are several major and minor problems with that.

  1. [minor] Being "semantically well-typed" only really makes sense as a notion on a safe fn. So it is unclear what (if anything) is require for unsafe fn here. But we need to require something so that the compiler can do its optimizations.
  2. [major] The semantic type system is super complicated. I literally wrote a PhD thesis on it, and there are very few people that fully understand this type system. That basically means that the vast majority of the community is excluded from discussing the actual specification of the rules that Rust programs must follow.
  3. [major] The syntactic type system does not uniquely define the semantic type system. There are many different semantic type systems that all match the same syntactic typing rules. This means there are choices to be made here, and due to point (2), it is hard to have a community-inclusive discussion of those choices. To make things worse, we might not even realize when we are making choices. For example, the model I defined in my thesis excludes Pin.
  4. [major] Due to point (2), very few people will be able to actually understand the precise rules their code has to follow. Even fewer will be able to prove that their code follows the rules. What does the rest do? We would hope they can at least run something like Miri, but with this approach, Miri is impossible. The actual condition for code to be well-defined is "must be well-typed in this semantic type system", and that is very undecidable. There's not even a well-defined notion of "this particular execution trace matches the semantic type system". It's all just hopeless.

Due to all of these reasons, I think this is the wrong approach to follow for Rust. We should not make some semantic type system the basis for defining what the compiler is allowed to assume. Instead, we should have an operational semantics with an explicit notion of UB, and the only assumption the compiler is allowed to make is that code will never hit any of the UB cases in the operational semantics.

I very strongly believe that if the disaster which is UB in C teaches us anything, it is that the only UB we may have in a language is UB that we can test for fully automatically at least on a per-execution basis, i.e., UB which is amenable to a tool like Miri. (This is already de-facto violated be 'relaxed' atomic memory accesses, and that causes me no end of frustration. But at least that is a feature only used by tiny amounts of unsafe code. And once they get the out-of-thin-air problem fixed it should be possible to at least do this in theory, if not in practice, so that's something.)

3 Likes
38

Oh. Huh.

For example, with x and y initially zero,

// Thread 1:
r1 = y.load(std::memory_order_relaxed); // A
x.store(r1, std::memory_order_relaxed); // B
// Thread 2:
r2 = x.load(std::memory_order_relaxed); // C 
y.store(42, std::memory_order_relaxed); // D

is allowed to produce r1 == r2 == 42 because, although A is sequenced-before B within thread 1 and C is sequenced-before D within thread 2, nothing prevents D from appearing before A in the modification order of y, and B from appearing before C in the modification order of x. The side-effect of D on y could be visible to the load A in thread 1 while the side effect of B on x could be visible to the load C in thread 2. In particular, this may occur if D is completed before C in thread 2, either due to compiler reordering or at runtime.

I sort of understand how this is allowed by the definition of the relaxed memory order, but it is in fact odd that this allows "out of thin air" sequenced-before reads to read a value written sequenced-after.

Cppreference says that C being sequenced-before D implies that C strongly-happens-before D. Strongly-happens-before is the strongest possible (cross-thread) relation between two operations.

If I'm reading cppreference correctly, this means that the visible sequence of side effects for C (in this execution) includes D, which C strongly-happens-before.

I would have naively assumed (hoped?) that this kind of shenaniganry was impossible or at least required llvm.unordered style ordering.

Out-of-order operation on the hardware (such that the write in D resolves before (A and B resolve and) the read in C resolves) leading to nontransitive observed happens-before is honestly kinda cursed.

At least C++14+ says that a read cannot observe (values dependent on) a write which carries a dependency on the read itself?

I would like to promptly forget that this exists and never see a relaxed atomic operation which carries a dependency on a relaxed atomic operation on a different location. I would like my data-race-free programs to not violate causality, thanks.

39

Out-of-thin-air values used to be something that everyone agreed weren't wanted and weren't produced by actual implementations; it was just surprisingly difficult to formalize how to ban them.

Then it turned out that, surprise, the right sequence of compiler optimizations can produce them:

https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1217r2.html

(But it's still true that they're not produced by actual hardware reordering.)

That paper also discusses possible fixes.

Not sure if there's been any progress in the three years since the paper; the paper's GitHub issue is barren, but I don't really understand how WG21 works.

1 Like
40

... now I'm even more upset at OOTA.

Note that the example I was using is not the "full OOTA" example with r1.store(r2) , r2.store(r1) producing a value never introduced by the source, but does actually introduce 42. "Full OOTA" is definitely even worse, but the example I was looking at is producible just via the ARMv8 load;store reordering, as there is no data-dependency from C to D other than the sequenced-after relation, and is still a causal cycle to observe the results of a sequenced-after write.