TB: Refine protector end semantics #3732
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JoJoDeveloping
force-pushed
the
tree-borrows-protector-end-write
branch
from
62336b4 to
71f6c4f
Compare
RalfJung
reviewed
Jul 4, 2024
Comment on lines
12
to
18
| let funky_ref_lazy_on_fst_elem; | ||
| { | ||
| // this creates a reference that is Reserved Lazy on the first element (offset 0). | ||
| // It does so by doing a proper retag on the second element (offset 1), which is fine | ||
| // since nothing else happens at that offset, but the lazy init mechanism means it's | ||
| // also reserved at offset 0, but not initialized. | ||
| funky_ref_lazy_on_fst_elem = |
There was a problem hiding this comment.
Is there a reason you did not make this let funky_ref_lazy_on_fst_elem = ...?
There was a problem hiding this comment.
No reason, just being derpy. 🙂
| funky_ref_lazy_on_fst_elem = | ||
| unsafe { (&mut *(ptr_to_vec.wrapping_add(1))) as *mut i32 }.wrapping_sub(1); | ||
| } | ||
| return funky_ref_lazy_on_fst_elem; |
There was a problem hiding this comment.
Suggested change
| return funky_ref_lazy_on_fst_elem; | |
| // If we write to `ref_to_fst_elem` here, then any further access to `funky_ref_lazy_on_fst_elem` would | |
| // definitely be UB. Since the compiler ought to be able to reorder the write of `42` above down to | |
| // here, that means we want this program to also be UB. | |
| return funky_ref_lazy_on_fst_elem; |
RalfJung
reviewed
Jul 4, 2024
RalfJung
reviewed
Jul 4, 2024
| @@ -28,7 +28,7 @@ impl fmt::Display for AccessCause { | |||
| Self::Explicit(kind) => write!(f, "{kind}"), | |||
| Self::Reborrow => write!(f, "reborrow"), | |||
| Self::Dealloc => write!(f, "deallocation"), | |||
| Self::FnExit => write!(f, "protector release"), | |||
| Self::FnExit(kind) => write!(f, "protector release ({kind})"), | |||
There was a problem hiding this comment.
Suggested change
| Self::FnExit(kind) => write!(f, "protector release ({kind})"), | |
| // These are dead code, since the protector release access itself can never | |
| // cause UB (while the protector is active, if some other access invalidates | |
| // further use of the protected tag, that is immediate UB). | |
| // Describing the cause of UB is the only time this function is called. | |
| Self::FnExit(_) => unreachable!("protector accesses can never be the source of UB"), |
This way if someone out there happens to somehow trigger this, we'll know. :)
There was a problem hiding this comment.
I've added it, and all tests still passed.
JoJoDeveloping
force-pushed
the
tree-borrows-protector-end-write
branch
from
71f6c4f to
5d11037
Compare
|
Looks good, thanks. :) @bors r+ |
|
☀️ Test successful - checks-actions |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Tree Borrows has protector end tag semantics, namely that protectors ending cause a special implicit read on all locations protected by that protector that have actually been accessed. See also #3067.
While this is enough for ensuring protectors allow adding/reordering reads, it does not prove that one can reorder writes. For this, we need to make this stronger, by making this implicit read be a write in cases when there was a write to the location protected by that protector, i.e. if the permission is
Active.There is a test that shows why this behavior is necessary, see
tests/fail/tree_borrows/protector-write-lazy.rs.