Track lent-through references as ShallowExclusive and announce all value drops - #175
Open
JonasAlaif wants to merge 3 commits into
Open
Track lent-through references as ShallowExclusive and announce all value drops#175JonasAlaif wants to merge 3 commits into
ShallowExclusive and announce all value drops#175JonasAlaif wants to merge 3 commits into
Conversation
Contributor
Author
|
I decided that reusing the |
…bility A collapse to write capability (an overwrite, or a StorageDead of e.g. a partially-moved local) packs up leaves that may still hold exclusive capability. Announce the capability drop with an explicit weaken for each such leaf, so that Collapse meets its guarantee that all packed-up places hold exactly the given capability. Related to #137. Owned weakens are now constructed through checked helpers (RepackOp::weaken / RepackOp::weaken_for_storage_dead) that assert the capability strictly decreases, and existing emission sites are routed through them. Also expose place_capability, local_is_expanded and the RegainedCapability accessors for consumers.
JonasAlaif
force-pushed
the
shallow-exclusive-refs
branch
from
August 13, 2026 12:19
9768fec to
d719f5b
Compare
A reference whose pointee is reborrowed still holds its own value: the pointer itself stays readable and overwritable; only the permission through the dereference is given up. That is exactly ShallowExclusive, so use it instead of silently dropping the reference to Write. All transitions out of ShallowExclusive are announced: overwrites and storage-deads weaken e -> W, and loan expiry restores from e. This also resolves the todo!() in the ShallowExclusive join arms: joining with a moved-out (Write) side labels the place and announces the value drop.
A place that was lent for reading reaches a join in a stale Read state (restore_place deliberately skips Read places when a read expansion dies), while the other side moved the value out. The joined state can only be Write, so the value still held on the read side is dropped by the join. Announce this as a restoration to Exclusive (the lending has ended) followed by an ordinary strictly-decreasing weaken to Write, after labelling the place so old-value references resolve to the join point.
JonasAlaif
force-pushed
the
shallow-exclusive-refs
branch
from
August 13, 2026 12:24
d719f5b to
039081d
Compare
Collaborator
|
@JonasAlaif This looks good to me at a high level, could you add a regression test (perhaps the motivating example)? |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Consumers that do exact resource accounting need two guarantees from the PCG's output that previously did not hold:
Writecapability must unambiguously mean "the place holds no value", and every transition intoWritemust be announced as an op on the statement or edge where it happens.Changes
Weaken still-exclusive leaves when collapsing to write capability (
obtainstep 2): a collapse-to-W(an overwrite, orStorageDeadof e.g. a partially-moved local) now emitsWeaken(E→W)for each leaf that still holds its value, so the emittedCollapsemeets its guarantee that all packed-up places hold exactly the given capability. Related to Unsound restoration to E capability after expiry of conditional borrow #137.Downgrade a mutably-derefed reference to
ShallowExclusive, notWrite: a reference whose pointee is reborrowed still holds its own value (the pointer stays readable and overwritable); only the permission through the dereference is given up, which is exactlyShallowExclusive. All transitions out ofeare announced: overwrites and storage-deads weakene→W, and loan expiry restores frome. This also resolves the previoustodo!()in the(e, _)join arms.Announce value drops at CFG joins: joining a lent-through (
e) or read (R) place with a side that moved the value out now labels the place (so labelled reads resolve to the join point) and announces the drop instead of performing it silently: theeside emitsWeaken(e→W), and theRside emits a restore toEfollowed by an ordinaryWeaken(E→W). Owned weakens are now constructed through checked helpers that assert the capability strictly decreases, upholdingRepackOp::Weaken's_.1 > _.2guarantee.