Removing allocations is technically unsound in OOM (out-of-memory) situations

[RalfJung]

The following program might be considered to be guaranteed to run out of memory, but LLVM actually compiles it in a way that it does not:

int *x = malloc(SIZE_MAX);
int *y = malloc(SIZE_MAX);
if (x && y) {
  printf("This is unreachable. I could deref a NULL pointer and this program would still be fine.");
}

It is not clear how to formally justify this.

@JakobDegen also has an example for recursion exhausting memory via stack allocations and being similarly optimized away.

[JakobDegen]

I've since improved upon the example:

fn bad(limit: usize) {
    if limit == 0 {
        return;
    }
    let mut x: usize = limit;
    let r = &mut x;
    bad(limit - 1);
    if *r != limit {
        panic!();
    }
    return;
}

fn main() {
    bad(usize::MAX);
    println!("unreachable");
}

The interesting things about it are that 1) it never does anything to inspect the values of the pointers and 2) all of the values in the locals are genuinely live when the recursion bottoms out, so no amount of liveness analysis will get us out of this.

[JakobDegen]

My original idea for a way to solve this was to not require that addresses of memory in different allocations be unique in general, but to magically guarantee that this is indeed the case for any two allocations that have the property of both being live and having at least one exposed (via ptr.expose_addr()) item in their borrow stacks. That runs into this cursed example though:

let p1 = alloca(8);
let p2 = alloca(8);

if abs_diff(p1.addr(), p2.addr()) < 8 {
    // Dead code, but removing it is unsound
    p1.expose_addr();
    p2.expose_addr();
    println!("Unreachable");
}

if abs_diff(p1.addr(), p2.addr()) < 8 {
    println!("Unreachable");
}

dealloc(p1);
dealloc(p2);

This means that even if we are willing to give up unconditional address uniqueness (which I think we have to given the example above), it is still entirely unclear how to make this work

[JakobDegen]

I've written up a proposal for a fix here: https://hackmd.io/@2S4Crel_Q9OwC_vamlwXmw/HkQaMnB49

[RalfJung]

At a high level, it seems like that proposal moves the OOM to when expose_addr is done? That's when OOM errors occur, and hence removing an expose_addr now becomes impossible for the same reason that removing OOM-causing operations was impossible previously.

So, doesn't this example still have the same problem?

let x = malloc(isize::MAX);
let y = malloc(isize::MAX);
let z = malloc(isize::MAX);

if x.expose_addr() != 0 && y.expose_addr() != 0 && z.expose_addr() != 0 {
  unreachable!();
}

free(x);
free(y);
free(z);

It should be possible to remove this expose_addr, since we can see the allocation being removed, so no valid code can ever pick this provenance in a future from_exposed_addr.

[RalfJung]

(After talking with @JakobDegen on Zulip.)

Indeed this doesn't entirely solve the problem of removing dead allocations -- one can still not remove dead allocations that are being exposed. However, that sounds like a big step forwards! Most allocations are not being exposed so removing them can be justified by this model. (And if we keep something like AllocId, we don't need many different "domains" either, just a single per-allocation boolean indicating whether it is part of the "bottom" domain.)

Basically, if we can carry the AllocId around reliably, we don't need "non-overlapping addresses" to figure out which allocation an access is intended to access.

The downside is that expose_addr becomes even more of an optimization barrier. Previously there were some conditions where it could be removed, that seems a lot harder now.

What remains somewhat fuzzy to me is that the address gets picked when the allocation is created, but if it gets exposed then that address may later fail to be disjoint and the program is doomed for OOM. Basically, it seems impossible for a programmer to prove, under this model, that their program does not go OOM. However, these kinds of models usually have to allow any allocation to non-deterministically OOM anyway, so... that doesn't really make things any worse, I think? Certainly some use-cases do need to prove absence of OOM, but they need a different model to begin with. I wonder if there are good ways to relate the two...

---

Now I wonder: what goes wrong if we just remove the "addresses must be disjoint" part entirely, without replacing it by some condition on expose_addr like @JakobDegen proposed? In from_exposed_addr we just non-deterministically guess which allocation is meant, as before. Shouldn't that still work?

[JakobDegen]

My third example was intended to show that this is potentially problematic:

// May these get overlapping addresses?
let p = alloca(8); *p = 0;
let q = alloca(8); *q = 0;

let a = p.expose_addr();
q.expose_addr();

let x = a as *mut usize;
*x = 5;
dbg!((*p, *q));

Legal behaviors for this program that users definitely expect would seem to be for it to OOM, or for it to print (5, 0). I believe your suggestion also allows it to print (0, 5), which seems extremely surprising (or even (0, 0) if there is any other exposed pointer anywhere else in the AM)

[RalfJung]

That's a fair point. Basically this boils down to, the angelic choice that is magically made should only be allowed to affect UB, not observable behavior.

[RalfJung]

I think I just realized there is a problem with this scheme: it breaks code like PartialEq for slices that has a fast-path for when both slices have the same address and length. Basically that would have to use expose_addr rather than addr, which (a) nobody will get right, and (b) makes optimizations hard, somewhat defeating the point of the fast-path.

[JakobDegen]

I think there are even more problems than that. For example, how does this work with FFI: We don't guarantee that this code

extern "C" { fn foo(a: &u8, b: &u8) }

let x = 0;
let y = 0;
foo(&x, &y);

will pass distinct pointers to FFI. This was not a concern with other situations, since in those cases the compiler had to assume that FFI code does the worst crimes it possibly could, but here the compiler has no such concerns. This can be fixed by saying something akin to: On FFI calls, we find all the pointers reachable from the arguments/globals and .expose_addr() them; this ensures that OOMs happen before the call, and so if the call succeeds everything has disjoint allocations.

This is ugly though, and I would absolutely love to have a model that does it better. I just don't know one

[RalfJung]

I don't see why things would be any different for an FFI function than for a Rust function.

[JakobDegen]

Oh, yeah, nevermind. This probably doesn't work then, which means we probably have to scrap a lot of this model. Really I think the most important thing we need is some way to address the annoying circular reasoning you can do in Example 2. I don't know how to go about it though.

[JakobDegen]

I thought about this some more, and can make the issue somewhat more concrete. For slightly weird reasons, I do think this is actually an issue specifically with external functions (such as FFI). Consider

fn bar() {
    foo(&1);
}

#[inline(never)]
fn foo(a: &i32) {
    a.expose_addr();
}

A naive implementation of the Rust AM under my model would require us to include a check in foo to ensure that the addresses of a does not overlap with any other exposed allocation. Obviously this is borderline impossible to practically implement. However, a compiler could be smarter. It could instead do things in two stages:

1. In the first stage (roughly resembling MIR) that check is implicit as a part of the .expose_addr(). We don't worry about how to implement this in actual hardware, we just pretend we can. This allows us to do all the optimizations that are enabled by this memory model.
2. In the second stage (roughly corresponding to asm) that check is no longer implicit. However, now our IR instead includes a promise that all allocations are created in the exposed address domain. This means that when we lower to this IR, we no longer have any need to include the check - it would come back false anyway. Of course, by doing this, we now once more have only finite memory and in general removing allocations at this stage is unsound - but that's ok, we've already gotten a chance to do our optimizations.

This kind of model almost works, except when you go and make foo pub. Now you're in trouble, because you can't expect that whatever will call foo, which may be arbitrary Rust code, will uphold the expectation of the lowered IR. In other words, when all the code we cared about was still under the control of this compilation session, our compiler could do smart tricks to avoid having to implement the check. Now that that is no longer the case, we're in trouble.

I don't see a way to fix this. As I said above, at this point I'm mostly just trying to think of a brand new idea.

[digama0]

I think this is why I was saying that it needs to be a compiler obligation that the OOM case of expose_addr is never actually codegenned. In the case of foo, I believe this means that we would need to mark the function as potentially-exposing (or actually-exposing if the body is visible), and in general for FFI calls we can't know whether addresses are exposed and must assume that they are.

We can therefore lift the exposure into bar, i.e. replace it with let x = &1; x.expose_addr(); foo(x). This is pessimistic since we might be prematurely exposing x and also the exposure could be conditional in foo if it is opaque, but since we are permitted to spuriously OOM, this is a legal transformation.

You can therefore optimize bar using the same two-stage approach - it's just that all calls to previously optimized and opaque functions are treated as exposing everything that is reachable. In short, I don't think FFI causes any additional issues.