allocations: document that they can be read-only

[RalfJung]

Miri currently tracks "read-only" as an explicit flag on allocations that exists independent of provenance. It essentially corresponds to a read-only mapping in the page table.

Let's make this officially part of our model.
Cc @rust-lang/lang @rust-lang/opsem

[rustbot]

r? @Mark-Simulacrum

rustbot has assigned @Mark-Simulacrum.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

Why was this reviewer chosen?

The reviewer was selected based on:

• Owners of files modified in this PR: libs
• libs expanded to 12 candidates
• Random selection from 6 candidates

[RalfJung]

@rfcbot merge opsem

[rust-rfcbot]

@RalfJung has proposed to merge this. The next step is review by the rest of the tagged team members:

• @CAD97
• @RalfJung
• @digama0
• @joshlf
• @saethlin

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[Mark-Simulacrum]

r=me with FCP complete, unless you think there's something to be done about the comment

View changes since this review

[rust-rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[joshlf]

Is there a reason we can't model this more simply as just only handing out read-only provenance pointers to these allocations without needing a separate notion of a read-only allocation?

Checking my box anyway – if there's a reason that a provenance-based approach isn't viable (or isn't genuinely simpler) then I'm happy to merge as-is.

[RalfJung]

Is there a reason we can't model this more simply as just only handing out read-only provenance pointers to these allocations without needing a separate notion of a read-only allocation?

I think with the restrictions we have on atomics, that does not work. Doing a load(Ordering::Acquire) with read-only provenance is entirely fine, but doing it on a read-only allocation is not.

[joshlf]

Our docs on atomic accesses to read-only memory say:

In general, all atomic accesses on read-only memory are undefined behavior. For instance, attempting to do a compare_exchange that will definitely fail (making it conceptually a read-only operation) can still cause a segmentation fault if the underlying memory page is mapped read-only. Since atomic loads might be implemented using compare-exchange operations, even a load can fault on read-only memory.

IIUC, this is a platform-level detail, not an opsem thing? In other words, the fact that an atomic load is implemented using compare-exchange isn't visible to opsem, and thus, as you said:

Doing a load(Ordering::Acquire) with read-only provenance is entirely fine

...because opsem doesn't "know" that the underlying atomic load is implemented via compare-exchange?

[RalfJung]

...because opsem doesn't "know" that the underlying atomic load is implemented via compare-exchange?

Correct. On the semantics / Abstract Machine level, a failing CAS and an atomic load are read-only operations, they don't change the contents of memory. (They do change some other state related to the concurrency memory model, but that's a separate question.)

In other words, this is sound, at least under Tree Borrows:

use std::sync::atomic::*;

fn main() { unsafe {
    let x = 0i32;
    let atomic_x = &*(&x as *const i32 as *const AtomicI32);
    // atomic_x is derived from &x, so it has read-only provenance.
    atomic_x.load(Ordering::SeqCst);
} }