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.

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

Is it sound to produce &[u8] and &UnsafeCell to the same memory so long as the latter isn't "used"? #455

Open
joshlf opened this issue Aug 29, 2023 · 6 comments

Comments

@joshlf
Copy link

joshlf commented Aug 29, 2023

Is it sound to produce a &[u8] and a &UnsafeCell which refer to the same region of memory and are live at the same time so long as no code performs mutation operations via the latter reference?

If this is sound, then it's possible to write a wrapper type which "disables" interior mutability by simply not exposing it, which is useful for caes such as google/zerocopy#5 (specifically, we are running into issues with how to define the MaybeValid type).

@RalfJung
Copy link
Member

This is intended to be sound but Stacked Borrows has issues with it, see #303.

@joshlf
Copy link
Author

joshlf commented Aug 29, 2023

Gotcha. Sounds like the current state of things is that:

  • It's desirable that this is sound
  • It's not currently guaranteed that this is sound
  • Under stacked borrows, this is not sound

Is it the case that, as is mentioned in the issue you linked, replacing &UnsafeCell with &MaybeUninit<UnsafeCell> makes it so that this is guaranteed to be sound? Or, as is speculated in the issue thread, is that just a limitation of Miri being able to see through MaybeUninit?

@RalfJung
Copy link
Member

RalfJung commented Aug 29, 2023

The issue mentions replacing UnsafeCell<T> with MaybeUninit<T>. That is unsound, &MaybeUninit<T> must be read-only like all shared references. I have no idea what the person in the issue meant when they said using MaybeUninit could help; it shouldn't make a difference (and we never got an example of it making a difference, so I think they were just confused and there are other things that changed at the same time).

@RalfJung
Copy link
Member

Gotcha. Sounds like the current state of things is that:

To add to the list: under Tree Borrows, this is sound.

@joshlf
Copy link
Author

joshlf commented Aug 29, 2023

The issue mentions replacing UnsafeCell<T> with MaybeUninit<T>. That is unsound, &MaybeUninit<T> must be read-only like all shared references. I have no idea what the person in the issue meant when they said using MaybeUninit could help; it shouldn't make a difference (and we never got an example of it making a difference, so I think they were just confused and there are other things that changed at the same time).

Ah gotcha. I'm asking a slightly different question, which is: Does stacked borrows consider it insta-UB to have &[u8] and &MaybeUninit<UnsafeCell> live at the same time? In other words, does MaybeUninit (or really any similarly-shaped union) serve as the hypothetical "disable interior mutability" type I was referring to in the original comment?

Unfortunately, I answered my own question in the negative (that code is adapted from the code in #303).

@RalfJung
Copy link
Member

RalfJung commented Aug 29, 2023 via email

joshlf added a commit to google/zerocopy that referenced this issue May 9, 2024
Previously, we required there to always be "`UnsafeCell` agreement"
between any `Ptr`s or references referencing a given region of memory.
This was based on an overly-strict interpretation of the semantics of
`UnsafeCell`.

In this commit, we relax `Ptr` to only require "`UnsafeCell` agreement"
when the aliasing model is `Shared`. All of the places that our internal
invariants are "consumed" - ie, where we use them as safety
preconditions for calling unsafe functions defined outside our crate -
this relaxation is sufficient.

This is based on what we (@jswrenn and I) believe to be a more accurate
model of the semantics of `UnsafeCell`s. In particular, `UnsafeCell`s do
not affect the semantics of loads or stores in Rust. All they do is
affect the semantics of shared references. In particular, Rust assumes
that the referent of a shared reference will not be stored to during the
lifetime of any shared reference, but this assumption is not made for
bytes which are covered by an `UnsafeCell`.

This is entirely a runtime property. If two references refer to the same
memory, but disagree on whether that memory is covered by an
`UnsafeCell`, this results in UB if the `UnsafeCell` is used to store to
the memory, violating the expectations of the non-`UnsafeCell` shared
reference. This commit is consistent with the runtime nature of this
property, but is inconsistent with Stacked Borrows
(rust-lang/unsafe-code-guidelines#455). However, this is considered to
be a bug in Stacked Borrows.
github-merge-queue bot pushed a commit to google/zerocopy that referenced this issue May 9, 2024
Previously, we required there to always be "`UnsafeCell` agreement"
between any `Ptr`s or references referencing a given region of memory.
This was based on an overly-strict interpretation of the semantics of
`UnsafeCell`.

In this commit, we relax `Ptr` to only require "`UnsafeCell` agreement"
when the aliasing model is `Shared`. All of the places that our internal
invariants are "consumed" - ie, where we use them as safety
preconditions for calling unsafe functions defined outside our crate -
this relaxation is sufficient.

This is based on what we (@jswrenn and I) believe to be a more accurate
model of the semantics of `UnsafeCell`s. In particular, `UnsafeCell`s do
not affect the semantics of loads or stores in Rust. All they do is
affect the semantics of shared references. In particular, Rust assumes
that the referent of a shared reference will not be stored to during the
lifetime of any shared reference, but this assumption is not made for
bytes which are covered by an `UnsafeCell`.

This is entirely a runtime property. If two references refer to the same
memory, but disagree on whether that memory is covered by an
`UnsafeCell`, this results in UB if the `UnsafeCell` is used to store to
the memory, violating the expectations of the non-`UnsafeCell` shared
reference. This commit is consistent with the runtime nature of this
property, but is inconsistent with Stacked Borrows
(rust-lang/unsafe-code-guidelines#455). However, this is considered to
be a bug in Stacked Borrows.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants