Open tavianator opened 4 years ago
The problem of surjective virtual addresses can be somewhat sidestepped by using proxy types that use ptr::volatile_{read,write}
to interact with the managed buffer, and Deref/Mut
to interact with user code. This has the downside of pessimizing optimization, by constructing proxy objects that have a destructor, rather than merely allowing ordinary load/store instructions.
It may also be possible to mark volatility by encoding the buffer as a [UnsafeCell<T>]
, rather than [T]
, in the container, and using pointer-casting in reference production to create &/mut T
references. I believe that LLVM is restricted from modifying accesses to an UnsafeCell
, regardless of the access site's Rust type, but I am not confident on this.
In this case, I would bias towards empirical proof, rather than theoretical: if the test suite indicates that runtime use of the structure shows that surjective pointers behave as expected, the library is "correct enough" going forward until a change to the environment (new behaviors in new LLVM or Rust versions) causes the test to misbehave according to the crate's assumptions.
I didn't see any discussion of this, so I figured I'd bring it up. I believe the "magic ring buffer" trick leads to undefined behaviour in C, for reasons discussed in this SO question which I just now realized you asked, so I suppose you're aware of the potential problem :). Still, for completeness I'll outline the potential problem from C's perspective:
I suspect this kind of assumption (p != q means they don't alias) is inherent in a lot of LLVM's optimizations, so I'm worried that Rust might have this problem as well, at least theoretically. I couldn't think of a way to demonstrate it with the API of
SliceDeque
.@myrrlyn points out here that the ownership system may make everything safe. It might be nice to have a more formal "proof" of that. I worry that sufficiently creative compiler optimizations could result in two different pointers to the same physical memory being live at the same time.