Stacked Borrows: An Aliasing Model For Rust

[glaebhoerl]

Question for my own edification: as far as I gather, this model does not deal very well with “transmutes”. What about the “types as contracts” model - is it any better at handling them?

[jpetkau]

You are creating a shared reference to a , and then mutating it. I think allowing this would inhibit most of the optimizations we want to do around shared references.

I thought your model was being careful work only in terms of actual loads and stores, and not say anything about data which was reachable through the type system but never actually reached. In this example the mutation to some data reachable from ‘a’ is never observed.

The launder does not affect the data behind the reference though – it launders the outer & in &'static Node , but it does not have any effect on the references stored inside that struct.

I guess I’m confused about the precise terminology in use here. Immediately after let p = some_address as *const (&'a i32, &'a i32); let r = &*p;, is there one reference or three? I was assuming the former–i.e. references that are part of some data structure sitting in memory aren’t part of the formal model until they’re loaded–but apparently that was wrong?

I think my first example had unnecessarily long ref lifetimes which confused the issue. Here is a cleaner version, where the work-in-progress nodes are stored in pointers instead of refs. Is there UB in this version?

Edit: yes, I was mixing up a half-baked model in my head with your model. I think your model does define what happens for all of my examples. Bits of the data-dependency-like model were stuck in my head because that’s the only way I can see to reasonably deal with transmutes. Cases like what to do with pointer * 0 fortunately aren’t actually a problem if you’re only tracking references.

[RalfJung]

Question for my own edification: as far as I gather, this model does not deal very well with “transmutes”. What about the “types as contracts” model - is it any better at handling them?

The trouble with transmutes comes from having extra data stored at pointers, so there is a representation difference between mutable references, shared references and raw pointers. “Types as Contracts” had the explicit goal to not do that, so it did not have this problem.

However, it made lifetimes matter. I am not sure which is worse…

I thought your model was being careful work only in terms of actual loads and stores, and not say anything about data which was reachable through the type system but never actually reached. In this example the mutation to some data reachable from ‘a’ is never observed.

Then you are misunderstanding. My model explicitly performs “activation” of all references that enter or leave a function – passed in as argument, passed out as argument, loaded from memory, stored to memory, passed in as return value, passed out via return. This gives us some nice invariants to work with – it is needed, for example, for the dereferencable annotation. Also we do retagging on references coming in, we can’t do that without looking at the data. The model is mostly access based, but not 100% so.

However, when doing “activation”, I propose to not recurse through references. So for example, when a function receives (as incoming argument, incoming return value or loaded from memory) a (&mut i32, &mut i32), then these references are both activated. However, when it receives a &mut &mut i32, the inner reference is not touched at all. IOW, we look at the data coming in (two references in case of the pair, one reference in the second example), but we do not go into memory to perform some recursive action.

Immediately after let p = some_address as *const (&'a i32, &'a i32); let r = &*p; , is there one reference or three?

I do not understand how you are counting references. The second line is a raw-ptr-to-shared-ref, so it will do the following to all locations “covered” by the ref – the ref has type &(&i32, &i32), so that would be 16 locations (with 8 bytes pointer size):

1. Activate a Raw (so some_address must be frozen or have a Raw in the stack)
2. Bump the clock and assign the newly created shared ref the current timestamp.
3. Initiate Frz(current_time), which will freeze the location.

The values stores in these locations (which happen to be references again in this case) do not matter at all here.

Here is a cleaner version, where the work-in-progress nodes are stored in pointers instead of refs. Is there UB in this version?

Yes. Let’s look at the most important steps happening:

    unsafe {
        (*a).next = &*b; // <--
        (*b).next = &*a;
        &*(a as *const Node)
    }

At the marked line, we create a shard ref covering whatever memory b is stored in. This follows the steps I described above, so in the end, that memory is frozen. In the next line, b.next is mutated again, which is okay because there is a Raw in the stack – but will end the freezing for that part of memory (the last 8 bytes of b), because you cannot mutate something frozen.
Finally, later a.next.next aka b.next is accessed. This will activate that shared reference, asserting that memory is still frozen – triggering UB because memory is in fact not frozen any more.

Taking a step back, at (*a).next = &*b; you are creating a shared reference. That is a promise that the memory pointed to by this reference will never be mutated while this reference is valid. The reference points at wherever b sits in memory. The next thing you do is mutate b. The only way now to maintain your promise is if we say that this invalidate the reference you just created. (With types as contracts, btw, this would already be UB – types as contracts takes lifetimes into account, so the moment you create an &'static pointing at something, that memory is marked as read-only forever. Which makes sense, because that’s literally what &'static is.)

We have to find a way to make this work without mutating memory pointed to by a shared reference. One way is to opt-out of the promise I mentioned above by using Cell or UnsafeCell. So if you replace &'static Node by Cell<&'static Node> or UnsafeCell<&'static Node>, you should be good. Would that be an acceptable solution? It changes the type throughout the program, but it also reflects better the fact that the memory here is being mutated while there is a shared ref pointing at it.

[jpetkau]

I thought your model was being careful work only in terms of actual loads and stores

… However, when it receives a &mut &mut i32 , the inner reference is not touched at all. IOW, we look at the data coming in (two references in case of the pair, one reference in the second example), but we do not go into memory to perform some recursive action.

That’s what I meant to say - the model is “shallow”, so reference-typed values that are just sitting out in some data structure in memory don’t have any special properties in this model until they’re loaded. (As opposed to the “types as contracts” model, where they do have special properties and my example is obviously UB.)

But your description of how the example would trigger UB doesn’t seem to be following this “shallow” model:

Finally, later a.next.next aka b.next is accessed. This will activate that shared reference, asserting that memory is still frozen – triggering UB because memory is in fact not frozen any more.

This will activate what shared reference? No reference is used more than once in the example, and all references are gone by the end of the unsafe block; a: *mut Node is the only live variable of any type at that point. New references are later derived from it (to access a.b.a), but those will have later timestamps. If that triggers UB, then so would let mut x = Box::new(5); &*x; *x = 6; *x. It’s the same sequence of steps: Start with a root raw pointer; derive a shared ref, freezing the memory; mutate the memory, unfreezing it; later, derive a new shared ref from the root pointer and use it to read the memory.

BTW I’m not arguing that my example should necessarily be legal; as long as there is some way to create cycles of references, and there seems to be general consensus that that’s desirable. But I think this model actually allows quite a lot of questionable stuff. E.g.:

    // of course lifetimes won't let this compile, but assume the same structure was created
    // by unsafe pointer casts or transmutes or whatever.
    let mut i = 0;
    let r1 = &mut &mut &mut i;
    let r2 = &mut &mut &mut i;
    ***r1 = 1;
    ***r2 = 2;
    println!("{}", ***r1);

This clearly should be UB. But it appears to be allowed by the stacked borrows model, because ***r1 loads a chain of new references from memory, so they get fresh timestamps and pushed onto the stack.

This is fixable for shared refs, by having the derived ref take its ancestor’s timestamp instead of a fresh timestamp (so the memory must have been immutable since the initial root shared ref was created), but I’m not sure how to fix it for unique refs without tracking the whole graph of which ref was created from which.

[RalfJung]

This will activate what shared reference?

b.next

The model is shallow, but when the code goes “down into the data”, the model follows along.

New references are later derived from it (to access a.b.a), but those will have later timestamps.

No, why would they? The timestamp is stored together with the reference in memory and fetched again when the reference is loaded from memory.

If that triggers UB, then so would let mut x = Box::new(5); &*x; *x = 6; *x .

No, this is fine. There is no shared reference that lives across the mutation. It is a very different sequence of steps.

Your code matches let mut x = Box::new(5); let ref = &*x; *x = 6; *ref. Or, slightly closer

let mut x = Box::new(5);
let shr = Box::new(&*Box::into_raw(x)); // put a shared ref into memory
*x = 6;
**shr // load the shard ref again and then deref it

That is UB.

This clearly should be UB. But it appears to be allowed by the stacked borrows model, because ***r1 loads a chain of new references from memory, so they get fresh timestamps and pushed onto the stack.

It is not allowed, and (I think I said this above but it seems that got missed ) you do not just get fresh timestamps when loading from memory. Instead, you first load the old timestamp, activate it – meaning make it the top of the stack, or cause UB if that does not work – and then retag (assign a fresh timestamp).

It was you who first talked about “just” assigning a fresh timestamp when loading. I replied that I find this dubious for &mut (search for “interesting suggestion” in this post). Thanks for providing an example

So, to repeat – reference identity, including the timestamp, is generally preserved by a memory round-trip. I did not say that explicitly in the post because I would never have thought of doing anything else.^^ Many steps in the model would not make any sense otherwise. Also we probably want to optimize a store immediately followed by a load into just re-using the value; if memory round-trips changed the value that would not be correct.

[gereeter]

Indeed, but as specified it is not a superset. LLVM will assume that alloca’ed variables whose addresses do not escape are not mutated externally

Ah. I see what you meant now. Sorry for the misunderstanding. As @RalfJung mentioned, this is justified on the LLVM side by citing the nondeterminism of allocation (in their Twin Memory Allocation paper). We could theoretically port this argument over directly to Rust, but it adds a line of reasoning that I thought we were trying to avoid. In essence (if I understand correctly), that paper argues that if there is a set of nondeterministic choices that result in undefined behaviour, then the code is undefined code, and so we can assume that this doesn’t happen. To quote the paper (section 3.2):

Since there is at least one execution where the program would trigger UB, the compiler can assume q cannot alias with p (or with any object at all).

This is an explicit departure from the notion that UB should be machine checkable, since we are declaring the code undefined even if the particular execution it takes is perfectly fine. Now, I might be willing to make this small concession, since the only type of nondeterminism relevant to this question is where allocations get located; things like I/O, pseudorandom number generation, etc. don’t have to count. However, it is a big leap from where we are today.

I think weak memory is of little concern here because all potentially racing accesses must happen through &UnsafeCell , so there is no freezing and no checking going on – everything is Raw .

That might simplify things? But that guarantee can only really be made with safe code, I think (yes, it is UB even outside of safe code, but since we’re trying to define UB, things feel like they get trickier). Besides, many of the problems show up when working purely immutably with data. The problem is that the freezes and such from creating references act as writes in the abstract, possibly creating (handle-able) races from something that isn’t writing at all.

Why do you think this is ruled out? The second reference would re-freeze, but that’s okay.

But if the two threads have incomparable timestamps, then thread 1 could freeze, have its freeze overwritten by thread 2’s freeze, and then try to access the data. The access would be undefined since thread 2’s freeze would not have come before the creation of thread 1’s reference. Perhaps for clarity I should have written the creation of the references and the access of the references as separate steps.

The return value would be activated, and then that would be UB because the location is not frozen.

Oof. That seems quite undesirable. I would instinctively want to say that since there is an implicit coercion that doesn’t even change the runtime representation of the references going from &mut to &, it should be perfectly safe.

Note that at least in my mind, the tag is just a timestamp, it does not know whether it is Uniq or Frz . So transmuting a &mut T to a &T actually “reinterprets” the tag. Maybe the tag should come with that extra information as you seem to assume it does, and maybe that helps – retagging would activate the Uniq , but then freeze. I think that solution sounds best, from the ones I have seen so far.

Yeah, I think this gets at why I wanted unique pointers to have an ID separate from the timestamp - it completely dodges all ugly questions about reinterpreting things. Also, yes, I think I was imagining that there was some sort of (abstract) runtime tagging of whether a pointer was unique or shared. As long as we have tags, we might as well add more information to them, I guess.

Spurious writes are only okay if the reference is never used again by anyone else in the future. Am I missing something?

The spurious writes I’m thinking about are writing the value that was already present, i.e.

*ptr = *ptr;

These definitely access the memory location, but there should be no problem if there are no aliasing/racing accesses and Uniq(ptr) is at the top of the memory’s stack. It does nothing to the value of memory and nothing to the stack.

However, this means that we can only add noalias when we can show that the corresponding reference is never dropped.

I don’t actually think this is a good direction to follow, but I don’t think the “never dropped” analysis would be that hard in most cases - mutable references passed to functions are reborrowed, generally, not moved, so they just aren’t dropped until the end of the function.

[jpetkau]

No, why would they? The timestamp is stored together with the reference in memory and fetched again when the reference is loaded from memory. […] So, to repeat – reference identity, including the timestamp, is generally preserved by a memory round-trip.

Yes, that’s where I was misunderstanding. I understood “shallow” to mean that references sitting out in memory had no special properties at all (in particular, no identity). The only per-memory-address metadata was your struct MemoryByte, with the stack of borrows / freeze state of that address, but no special metadata for a reference that might be stored there. So loading a value of type &i32 would have to get a new timestamp from somewhere. Hence my talk about “root pointers” - if all you have is an &&&i32, there is just one reference in the model until you start following the chain.

I’m pretty sure this model would actually work fine for shared references. But yeah, it’s not at all the same as your model. Thanks, now it makes much more sense.

This is a much stricter model, in some ways more strict than “types as contracts”, since transmuting or casting a pointer won’t let you change the restrictions on indirectly reachable references. So how the model handles transmutes is important.

(That’s another reason I was confused for so long–I assumed the model had to let you fill in a chunk of memory by some unspecified means, then declare “this a *mut T with lifetime starting now” and use it as such, as long as the bits in that memory are valid for a T.)

A slightly more interesting case is if you have a memory region that stores pointers, and is accessed by code that needs raw pointers (e.g., it’s a data structure shared with C code), but some other code wants to view the memory as containing references. However, in that scenario it seems acceptable to me to require that all code agrees that the memory contains raw pointers, and let the code that wants to deal with references explicitly cast between raw pointers and references when loading and storing (and place any lifetime parameters in PhantomData ).

I hope we can avoid such a limitation. Rust’s current support for transmutes and working with the with the bit representation of types is really useful, and a big selling point for low-level programming. (In contrast to the C/C++ model, where the standard effectively refuses to admit that objects are made of bits, and so makes things that should be trivial either UB or impossible unless you go the linux kernel route and tell the compiler to follow different rules for your codebase.)

[nikomatsakis]

If &&T can point to an invalid pointer, there would be some restrictions on that optimization:

I have wondered about this optimization too. It seems though that if we are analyzing to see whether the &&usize escapes the function, we could also analyze to see whether the usize value is actually used, no? In that case, we could do the optimization without caveats.

Well, I suppose the concern is that there would be cases where it is “maybe used”…? I suppose that without termination analysis that is eminently possible. So never mind perhaps. =)

[comex]

Making integers carry tags invalidates all sorts of arithmetic optimizations, so that is a no-go.

My first thought was – what if integers carry tags but arithmetic does not propagate them, so only straightforward copies were allowed?

But that’s not enough, since, as you know, there’s still the problematic optimization of "if we know that a == b, then replace b with a".

Still, at the risk of repeating myself, I really think that a model that doesn’t allow copying values through memcpy is unacceptably surprising.

I’m curious whether and how LLVM intends to fix the aforementioned issue for C, and whether the resulting model will be sane/predictable enough that it could be used here.

From the LLVM bug thread:

Nuno Lopes 2017-11-07 11:44:34 PST

Ralf is part of the memory model team btw. We will share a document + patches starting late next week.

Do you know if that document ever got shared, and if so do you have a link?

[RalfJung]

In essence (if I understand correctly), that paper argues that if there is a set of nondeterministic choices that result in undefined behaviour , then the code is undefined code , and so we can assume that this doesn’t happen.

There is no such thing as undefined code. Undefined behavior is a property of an execution. If a program has multiple executions because of non-determinism, then if any execution has UB, that is sufficient license for the compiler to optimize. This is the same for Rust, C and LLVM. I do not see any other way to define this – we cannot require all executions to exhibit UB, that would be prohibitive for optimizations. For example:

fn main() {
  let x = Box::into_raw(Box::new(0)) as usize;
  let y = 0x42440usize as *mut i32;
  println!("{}", unsafe { *y });
}

This could be defined behavior if x is really allocated at that address. Still we say the program has UB because it can have UB.

This is an explicit departure from the notion that UB should be machine checkable, since we are declaring the code undefined even if the particular execution it takes is perfectly fine.

Yes and no. It is, in principle, still checkable by exploring all executions. Again, this is not new – for example, once concurrency enters the picture, this is also the case even if you entirely ignore integer-pointer-casts.

Now, the question is whether this is still feasible to check. And if the number of executions is large, it is not. Which is why I am trying to reduce the extend to which we rely on non-determinism for this. However, for the kind of reasoning LLVM does around pointer-integer-casts, I do not see any alternative. You do not even have to go all the way to twin memory allocations to see this, the following example is sufficient:

fn main() {
  let x = Box::into_raw(Box::new(0)) as usize;
  let y = Box::into_raw(Box::new(1)) as usize;
  if x < y { /* cause UB */ }
}

Essentially, the moment the actual integer address of an allocation matters, you have a huge amount of non-determinism and no way to explore it exhaustively.

And, again, I do not follow your terminology. What is “undefined code”? UB is a per-execution property.

---

Oof. That seems quite undesirable. I would instinctively want to say that since there is an implicit coercion that doesn’t even change the runtime representation of the references going from &mut to & , it should be perfectly safe.

This was talking about a transmute from &mut to &. These do have different runtime representations in my model – and anyway coercions do not imply “same runtime representation”, consider e.g. unsizing.

Yeah, I think this gets at why I wanted unique pointers to have an ID separate from the timestamp - it completely dodges all ugly questions about reinterpreting things.

Oh then I misunderstood. What you are asking for is for the thing tagging & and the thing tagging &mut to be distinguishable. If one was a timestamp and one an ID they’d still both be 64bits of data. OTOH, if we sacrifice a bit or two to introduce a distinction, we can do that and still use timestamps for &mut.

Essentially, currently I plan to use the Borrow enum from my post as tag.

The spurious writes I’m thinking about are writing the value that was already present, i.e.

I see. Yes inserting those for &mut should be fine, not sure why you’d want to do that. (We’d have to take care that this does not require the value at that location to be valid, but that should be doable.)

---

The only per-memory-address metadata was your struct MemoryByte , with the stack of borrows / freeze state of that address , but no special metadata for a reference that might be stored there.

The reference metadata is part of that reference. There is no reference without the metadata. So this is not per-memory-address metadata, it is just part of the data that is stored in memory.

---

Still, at the risk of repeating myself, I really think that a model that doesn’t allow copying values through memcpy is unacceptably surprising.

I’m curious whether and how LLVM intends to fix the aforementioned issue for C, and whether the resulting model will be sane/predictable enough that it could be used here.

Oh sure, I think one should be able to copy through memcpy. What does not work – and is, in fact, broken in LLVM (though I do not know of a miscompilation) is doing that while using an integer type in memcpy. You want a type that can hold arbitrary data, including (part of) a pointer with its metadata – a type that you cannot do anything with, no arithmetic, no deref, just write it somewhere else. C intends to make char that type, but that does not actually work because C also allows arithmetic on char. Unfortunately, LLVM has no type suitable for this purpose either – and without a concrete miscompilation, it will be hard to convince them to change that.

Do you know if that document ever got shared, and if so do you have a link?

That document is the twin allocation paper that has been mentioned here multiple times

[gbutler]

then if any execution has UB, that is sufficient license for the compiler to optimize.

Could you explain briefly why freeing the compiler to optimize if there is UB is a desirable goal? I would think it would be better to simply abort/fail to compile for UB. Why is well-defining what UB is, then using that definition to allow for optimizations useful? If something is UB, and I optimize it, isn’t it still UB? How is a program with UB useful?

EDIT: As I think about this more, I think I understand: The “compiler” like LLVM can optimize UB in the LLIR presented to it because it can assume that the higher-level compiler has already ruled out the UB case and that it will never occur in practice, therefore, the LL compiler can optimize “knowing” that the UB will never actually occur even though it can’t statically prove that from the information (structured IR) presented to it. Is that roughly correct?

[Ixrec]

I’m sure Ralf will have a better answer here, but since I think I understand this stuff I’d like to double-check that I do understand it by writing down what I believe the answers are in case I need correction.

Could you explain briefly why freeing the compiler to optimize if there is UB is a desirable goal?

This is a bit of a strange question because license to optimize is the only reason why we want unspecified, implementation-defined and undefined behavior to exist in the first place. I’m not sure there’s a more direct/helpful answer than “if that optimization wasn’t desirable, then that code wouldn’t be UB.”

I would think it would be better to simply abort/fail to compile for UB.

I think what’s happened here is some confusion over the compiler knowing for sure that a program will exhibit UB, and the compiler making optimizations based on the assumption that UB will not be exhibited. When the compiler actually does know UB is going to happen, that absolutely should be a compiler error (afaik this is totally uncontroversial). But when we ask the compiler to optimize a function that takes two shared references, we don’t expect the compiler to go check all the call sites of that function and prove the references cannot possibly alias, which it likely can’t do in the presence of sufficiently complex unsafe code or external crates. Instead, we say it’s UB for shared references to alias, so it can go ahead and compile the function with the obvious optimizations you’d expect, and the presence of unsafe/external/etc code near one of its call sites does not magically deoptimize anything.

Why is well-defining what UB is, then using that definition to allow for optimizations useful?

Pretty much the same as the first question. If you have a desirable optimization that can’t be done without declaring something UB, then we can’t actually make that optimization work in practice with other people’s unsafe code unless the authors of that unsafe code know what is and isn’t UB.

If something is UB, and I optimize it, isn’t it still UB?

Well, yeah. Rust-level UB is different from LLVM IR-level UB is different from x86-level UB. I think we’re mostly talking about Rust-level UB, which is just a property of the Rust source code, not a property of the final executable. How much optimization was done by the Rust compiler has nothing to do with whether the Rust source code had Rust-level UB, unless the compiler is literally editing your source code for some reason. If you meant “does the x86 executable have x86-level UB if compiled from Rust source code with Rust-level UB?” then the answer is “it may or may not; Rust-level UB means the Rust compiler is allowed to do anything at all with it.”

How is a program with UB useful?

A program that actually exhibits UB is never useful in theory. In practice, it’s only useful if your compiler happens to be acting as if it wasn’t exhibiting UB, either because you configured it to do so or because it’s not fully exploiting that license to optimize yet.

EDIT: As I think about this more, I think I understand: The “compiler” like LLVM can optimize UB in the LLIR presented to it because it can assume that the higher-level compiler has already ruled out the UB case and that it will never occur in practice, therefore, the LL compiler can optimize “knowing” that the UB will never actually occur even though it can’t statically prove that from the information (structured IR) presented to it. Is that roughly correct?

I think this is the correct intuition for why LLVM IR has more complex (and harder to auto-check) rules for UB than we would like surface Rust to have. Though surface Rust still needs some notion of what UB is to justify all the optimizations we want around arbitrary unsafe code.

[arielb1]

I do not see any other way to define this – we cannot require all executions to exhibit UB, that would be prohibitive for optimizations.

Note that the “nondeterminism” here is not what a system programmer would call “nondeterminism”.

1. For a system programmer, nondeterminism generally refers to “environment nondeterminism” - which random value is read from /dev/urandom, which request arrives first on a socket, et cetera. The compiler is not allowed to make arbitrary choices here - if a code has a buffer overflow when it gets requests in the wrong order, the program should still be well-defined as long as requests arrive in the correct order.
2. For twinned allocation, nondeterminism is something that the compiler can choose - it can place stack arguments in which location it wants, and leave “traps” in arbitrary memory locations, to “catch” code that performs “random” memory accesses. This nondeterminism essentially only happens in theory - if code mangles memory, the compiler can retroactively claim that the address the mangling code accessed was a “trap”, and therefore UB happened. This has nothing to do with “environment” nondeterminism.

[arielb1]

I’m trying to differentiate this model from the ACA model (https://github.com/nikomatsakis/rust-memory-model/issues/26), to explore model space.

One significant difference is that ACA has lifetimes, while this model doesn’t. However, I don’t think this is such a big difference as it seems.

Axis 1 - lifetimes

I think the barrier + use semantics are fairly close to making a borrow’s lifetime last as long as it is either live or kept alive by a barrier. This is not necessarily a valid “Rust” assignment of lifetimes - it can violate “artificial” lifetime constraints (in ACA, you could fix a lifetime to anything you want by using lifetime constraints), and “interior borrow constraints”, and of course it is a dynamic, rather than a static, notion.

By “interior borrow constraints” I mean the following:

fn foo(x: &mut Option<&mut u32>) { unsafe {
    let x_ptr: *mut Option<&mut u32> = x;
    let t = &mut *x;
    let x_inner: &mut u32 = match t {
        &mut Some(ref mut x_inner) => &mut **x_inner,
        None => return
    };
    *x_ptr = None;
    use(x_inner);
}}

By ACA, this is UB - the reborrow in x_inner asserts ownership of x for the entire lifetime of x_inner, which conflicts with the write *x_ptr = None;. By the stacked borrow model, t is not live after the match statement, so there is no conflict.

Axis 2 - lifetimes of raw pointer

This is a bit similar to axis 1.

fn foo(x: &mut u32) -> u32 {
    let raw: *mut u32 = x;
    let t = &mut *x;
    *t = 0;
    unsafe { *raw } // is this UB?
}

In the stack-based model, if I understood it right (did I), creating t pops of the Raw from the stack, which makes further accesses from a raw pointer UB.

In the ACA model, this depends on how the lifetimes are assigned, so the situation is more vague. If the lifetime of the raw pointer is the same as x, this is OK, because as long as the raw pointer is alive, x does not protect the memory behind it.

The intent IIRC was that the compiler will be conservative and make it OK.

Axis 3 - stack vs. cactus stack

The ACA model is OK with creating a “cactus” of mutable references, as long as only 1 of them is used in the end. I think that this works less well with the “stacked borrow” model, but that this is orthogonal to the “strict liveness” restriction (i.e., it is possible to create a “cactusy” lifetimeless system).

I think the “cactus” behavior is essential for “unsafe mutability polymorphism”, as in https://github.com/nikomatsakis/rust-memory-model/issues/31

fn foo(a: bool, r: &mut u32) {
    let r1a = &mut *(r as *mut u32);
    let r2a = &mut *(r1a as *mut u32);
    let r1b = &mut *(r as *mut u32);
    let r2b = &mut *(r1b as *mut u32);
    if a {
        *r2a = 0;
// using r2b is now illegal
    } else {
        *r2b = 0;
// using r2a is now illegal
    }
}

[RalfJung]

Could you explain briefly why freeing the compiler to optimize if there is UB is a desirable goal? I would think it would be better to simply abort/fail to compile for UB. Why is well-defining what UB is, then using that definition to allow for optimizations useful? If something is UB, and I optimize it, isn’t it still UB? How is a program with UB useful?

In addition to what @Ixrec wrote, may I point you at this blog post of mine?

The short summary is that UB is a contract between the compiler and the user; it is a way for the compiler to make assumptions during optimizations that it would have a hard time determining with its own analyses, so it asks the user to prove them instead.

Why is well-defining what UB is, then using that definition to allow for optimizations useful?

The term “undefined behavior”, and indeed its treatment in C, seems to sometimes lead to the impression that undefined behavior is about not defining something. That’s not really true. It is important to have a precise definition of which programs have undefined behavior, because compiler authors need to know exactly what they can rely on and programmers need to know exactly what they have to prove! What is “undefined” about UB is what the program does when it exhibits UB. This is very different from defining whether a program exhibits UB.

---

For a system programmer, nondeterminism generally refers to “environment nondeterminism” - which random value is read from /dev/urandom , which request arrives first on a socket, et cetera. The compiler is not allowed to make arbitrary choices here - if a code has a buffer overflow when it gets requests in the wrong order, the program should still be well-defined as long as requests arrive in the correct order .

Good point. This is what I think is usually called “external non-determinism” in the literature.

For twinned allocation, nondeterminism is something that the compiler can choose - it can place stack arguments in which location it wants, and leave “traps” in arbitrary memory locations, to “catch” code that performs “random” memory accesses. This nondeterminism essentially only happens in theory - if code mangles memory, the compiler can retroactively claim that the address the mangling code accessed was a “trap”, and therefore UB happened. This has nothing to do with “environment” nondeterminism.

I agree that this “internal” non-determinism is different, but I disagree that it only happens in theory. It happens in practice, and is very observable, for example with concurrency: The following program may print either 0 or 1, and the compiler is free to optimize it to a program that always prints one of the two things:

fn main() {
  let x = AtomicUsize::new(0);
  rayon::join(
    || x.store(1, Ordering::Relaxed),
    || println!("{}", x.load(Ordering::Relaxed)
  )
}

This program inherently has several ways in which it can execute (independent of what the environment does). The compiler is at liberty to preserve this non-determinism or reduce it, ruling out some possible executions. Many optimizations the compiler performs around memory accesses have the effect of ruling out some executions.
If any of these branches has UB, the compiler can hence eliminate all branches except for the UB one, and then proceed assuming the program has UB.

---

By ACA, this is UB - the reborrow in x_inner asserts ownership of x for the entire lifetime of x_inner , which conflicts with the write *x_ptr = None; . By the stacked borrow model, t is not live after the match statement, so there is no conflict.

I am surprised that this is UB. x_inner has nothing to do any more with x, it is a copy (reborrow) of the inner reference, inside the Option. Does this happen because taking a borrow out of x means that x's lifetime has to outlive x_inner?

In the stack-based model, if I understood it right (did I), creating t pops of the Raw from the stack, which makes further accesses from a raw pointer UB.

Correct. This is needed, I think, do get the desired behavior from methods like split_at_mut that “reborrow” through a raw pointer: After let y = slice.split_at_mut(2).0, when slice is used again, y should become invalid just like it would if this was a normal reborrow.

the lifetime of the raw pointer

Come again? How are those defined, and how do they behave when casting from and to integers?

a “cactus” of mutable references

I think the “cactus” behavior is essential for “unsafe mutability polymorphism”, as in https://github.com/nikomatsakis/rust-memory-model/issues/31

Hm, so with Stacked Borrows something like this might work if initiating a reference happens on its first use, not on its creation. (No idea where there is a “cactus” here.^^) But that seems way too permissive to me.

What is the argument for making that code legal? I cannot see the connection to the example in the issue you linked. And I think allowing what you asked for in that issue is in direct contradiction to optimizations we might want to allow, like inserting spurious write to mutable references if we know that does not change the value (could introduce a data race if this is actually a shared reference).

“mutability polymorphism” should be solved on the type-system level, not by weakening what the reference types mean.

[arielb1]

Non-determinism

I agree that this “internal” non-determinism is different, but I disagree that it only happens in theory. It happens in practice, and is very observable, for example with concurrency: The following program may print either 0 or 1, and the compiler is free to optimize it to a program that always prints one of the two things:

The reason that I said that the determinism occurs “only in theory” is because it does not have to precisely match reality “at the lowest level”. For example, if you use your Special Environment Powers, for example a debugger, to find the “canonical” location the compiler used to store a variable, you still can’t reliably change the variable by writing to it (either via the debugger or via a “lackey” in the program).

Similarly, with timing, with a sufficiently smart compiler behind rayon::join, the real-world timing of operations (which might be measured by e.g. timing page faults) might not always match the PL “happens-before” relationship.

For a system programming POV, a program is always embedded in an environment, which satisfies its own interpretation of the “environment specification” (at least most of the time). The mapping between environment concepts and PL concepts is not always trivial.

ACA

Does this happen because taking a borrow out of x means that x 's lifetime has to outlive x_inner ?

Exactly because of this.

lifetimes of raw pointers

the lifetime of the raw pointer

Come again? How are those defined, and how do they behave when casting from and to integers?

That’s the problem with models that rely on lifetimes. The original idea was that the compiler couldn’t assume anything about the lifetimes in unsafe code, but could pick out whatever lifetimes it wanted in safe code, but then as_ptr_mut being safe ruined that idea.

However, if you can define the lifetime of a raw pointer, it doesn’t cause any problem when casting through an integer.

mutability polymorphism

“mutability polymorphism” should be solved on the type-system level, not by weakening what the reference types mean.

For that, we have to first solve it on the type-system level, then get all programmers to use the solution. If we want to define Rust of today, we have to support “implicit” mutability polymorphism.

[arielb1]

Correct. This is needed, I think, do get the desired behavior from methods like split_at_mut that “reborrow” through a raw pointer: After let y = slice.split_at_mut(2).0 , when slice is used again, y should become invalid just like it would if this was a normal reborrow.

The problem is that this would make implementations of split_at_mut that “implicitly” insert reborrows UB, e.g.

fn split_at_mut(&mut self, at: usize) -> (&mut Self, &mut Self) {
    let x: *mut Self = &mut self[..at];
    let y: *mut Self = &mut self[at..]; // this would pop `self[..at]`
    unsafe { (&mut *x, &mut *y) }
}

[RalfJung]

The reason that I said that the determinism occurs “only in theory” is because it does not have to precisely match reality “at the lowest level”. For example, if you use your Special Environment Powers, for example a debugger, to find the “canonical” location the compiler used to store a variable, you still can’t reliably change the variable by writing to it (either via the debugger or via a “lackey” in the program).

Similarly, with timing, with a sufficiently smart compiler behind rayon::join , the real-world timing of operations (which might be measured by e.g. timing page faults) might not always match the PL “happens-before” relationship.

For a system programming POV, a program is always embedded in an environment, which satisfies its own interpretation of the “environment specification” (at least most of the time). The mapping between environment concepts and PL concepts is not always trivial.

I agree to the high-level point that the “source” of non-determinism might look different in the mathematical model and in the “real thing”. However, the non-determinism itself – the fact that it occurs – is real, or else we wouldn’t bother modelling it.

It’s news to me that “happens-before” would contradict real-world timing. How can that happen?

For that, we have to first solve it on the type-system level, then get all programmers to use the solution. If we want to define Rust of today, we have to support “implicit” mutability polymorphism.

I am afraid this is in direct contradiction with some of the assumptions we want to make, e.g. about &mut really being unique pointers. I am not convinced we have to support “implicit” mutability polymorphism.

The problem is that this would make implementations of split_at_mut that “implicitly” insert reborrows UB

Yes, that is intentional. Using a &mut, including reborrowing from it, asserts that this &mut is currently live and hence unique.

It might be possible to weaken this, but this is the first time I hear that we want to allow such code.

[RalfJung]

Btw, if you want to follow along the implementation of this in miri, we have a topic on Zulip for that

[system]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.