Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[pointer][invariant] Remove AliasingMapping, Inaccessible #1942

Open
wants to merge 1 commit into
base: Ifc49755af0d90eeefe7822d755d508403c266bda
Choose a base branch
from
Open

[pointer][invariant] Remove AliasingMapping, Inaccessible #1942

wants to merge 1 commit into from

Commits on Nov 11, 2024

  1. [pointer][invariant] Remove AliasingMapping, Inaccessible 

    We previously used `AliasingMapping`s and `Inaccessible` to model
`UnsafeCell` agreement. This abuses the notion of a mapping since one
doesn't ever actually want to change the aliasing of a pointer (and
certainly not to `Inaccessible`) - really this was meant to model
pointer casts which should never be performed. In addition to being an
awkward fit, the presence of `Inaccessible` meant that code could not
assume that any `Aliasing` invariant permitted reading, and so we had to
add extra machinery to work around this.

Future commits will use a different, simpler model for denoting
`UnsafeCell` agreement or disagreement.

While we're here, make `Read` slightly more permissive, implemented for
`A: Aliasing, T: Immutable` rather than just `A: Reference, T:
Immutable`.

Makes progress on #1122, #1866

gherrit-pr-id: I1ac2ae177a235083e33b09fc848423220d3da042
    @joshlf
    joshlf committed Nov 11, 2024
    Configuration menu
    Copy the full SHA
    355531d View commit details
    Browse the repository at this point in the history