Tree Borrows: Make tree root always be initialized #3415
Merged
Conversation
This file contains 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-initialized-root
branch
from
00adb65
to
8a6587e
Compare
RalfJung
reviewed
Mar 25, 2024
|
After some further thought, we decided to make the root note default |
JoJoDeveloping
force-pushed
the
tree-borrows-initialized-root
branch
2 times, most recently
from
8ab3543
to
63107f8
Compare
RalfJung
reviewed
Mar 26, 2024
Comment on lines
475
to
477
| // we manually set it to `Active` on all in-bounds positions. | ||
| // we also ensure that it is initalized, so that no `Active` but | ||
| // not yet initialized nodes exist. |
There was a problem hiding this comment.
Suggested change
| // we manually set it to `Active` on all in-bounds positions. | |
| // we also ensure that it is initalized, so that no `Active` but | |
| // not yet initialized nodes exist. | |
| // We manually set it to `Active` on all in-bounds positions. | |
| // We also ensure that it is initalized, so that no `Active` but | |
| // not yet initialized nodes exist. Essentially, we pretend there | |
| // was a write that initialized these to `Active`. |
There was a problem hiding this comment.
You dropped part of my diff, I had also fixed capitalization in the first two lines.
That's why using the github button is a good idea. ;) (You can than still pull, squash, force-push if you want to avoid the extra commit.)
There was a problem hiding this comment.
Ah, alternatively I could simply look more closely 🙈
I've also fixed capitalization in other places.
|
LGTM, just one comment nit. :) |
JoJoDeveloping
force-pushed
the
tree-borrows-initialized-root
branch
from
63107f8
to
07bbebb
Compare
There should never be an `Active` but not initialized node in the borrow tree. If such a node exists, and if it has a protector, then on a foreign read, it could become disabled. This leads to some problems when formally proving that read-reordering optimizations are sound. The root node is the only node for which this can happen, since all other nodes can only become `Active` when actually used. But special- casing the root node here is annoying to reason about, everything becomes much nicer if we can simply say that *all* `Active` nodes must be initialized. This requires making the root node default- initialized. This is also more intuitive, since the root arguably becomes ini- tialized during the allocation, which can be considered a write.
JoJoDeveloping
force-pushed
the
tree-borrows-initialized-root
branch
from
07bbebb
to
5b208c4
Compare
|
Thanks! |
|
☀️ 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.
This PR fixes a slight annoyance we discovered while formally proving that certain optimizations are sound with Tree Borrows. In particular... (copied from the commit message):
There should never be an
Activebut not initialized node in the borrow tree. If such a node exists, and if it has a protector, then on a foreign read, it could become disabled. This leads to some problems when formally proving that read moving optimizations are sound.The root node is the only node for which this can happen, since all other nodes can only become
Activewhen actually used. But special-casing the root node here is annoying to reason about, everything becomes much nicer if we can simply say that allActivenodes must be initialized. This requires making the root node default-initialized.This is also more intuitive, since the root arguably becomes initialized during the allocation, which can be considered a write.