[BEAM] Unsynchronized access to a shared static mut variable

[japaric]

Please read #111 first, if you haven't already.

Rendered discussion document

[RalfJung]

The crucial aliasing point here is: the moment INTERRUPT1 starts executing, any previously created pointer such as everything done in INTERRUPT0 gets invalidated.

So, safety relies on the assumption that the safe code cannot somehow leak the &'static mut that it got -- for example, through a static X: RefCell<Option<&'static mut u128>> or so. I assume that is possible for safe code even on BEAM, so this would not be a safe abstraction. But if you change it as follows, I think this hole is plugged:

#[no_mangle] unsafe fn INTERRUPT1() { let x: &mut u128 = unsafe { &mut X }; inner(x); // Crucially, inner is generic in the lifetime and hence // cannot leak the reference. fn inner(x: &mut u128) { // .. any safe code .. } }

Besides this point, I agree that the program is fine as far as Stacked Borrows is concerned. I can only hope LLVM agrees with that. ;) The compiler cannot know that the functions cooperate, but when it doubt it has to assume that they do.

[RalfJung]

Closing due to inactivity, see #169 for tracking.