Nick Spinale

> A compiler barrier is not sufficient to prevent the compiler from fusing memory accesses. Ah, you're right, the mutable reference to the memory being accessed by the assembly fragment...

> Is there anything rust-sel4 can do to prevent this? If not, maybe a note should be added to the with_ipc_buffer functions saying that you should never do an IPC...

Good call, I've improved the relevant error messages here: https://github.com/seL4/rust-sel4/pull/259

> i don't think it's because of any compiler memory barrier, but rather because the with_ipc_buffer calls are separated, the ipc buffer mut borrow is shortened and so the compiler...

However, thanks to insight gleaned from this discussion, I now realize that the handling of the IPC buffer in the implementation of the IPC operations in the `sel4-sys` crate is...

Thanks for identifying this bug. I'd like to avoid unsafe except where absolutely necessary. The reason for not using the `sys::seL4_BootInfoHeader` directly for reading the header is because casting arbitrary...

Thanks for this feedback, you're right, the use of this term is confusing. My intent was to use it to mean literally the granule from the perspective of the seL4...

> Do you mean `seL4_PageBits`? Smallest memory seL4 deals with via UTs is `seL4_MinUntypedBits`, which is 4. Ah yes, sorry for being unclear, I meant the smallest unit on the...