Repository navigation
fix(auto): register Base lock functions as non-consuming effects - #84
MilesCranmerBot wants to merge 3 commits into
Conversation
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cd58e82ffb
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
|
Replaced the approach in 4bd8bd5 — registering Base.lock/unlock/trylock/islocked as non-consuming effects is the wrong model: it blesses a lock as a memory-safety boundary and makes locked regions a diagnostic void where aliased writes and escapes are silently accepted. A lock serializes task access; it says nothing about borrow rules. Adversarial probe results (now pinned as tests): aliased write inside the lock block remains missed on both versions and is now pinned with a repro as @test_broken; escape into an outliving Ref is diagnosed on this branch via conservative consume-attribution of the unknown closure call; global array writes remain missed on both (globals untracked, pre-existing). Root cause of the remaining holes: the do-block lowers to a fresh closure object captured through slot-merged Core.Boxes; the checker never enters the callback body, and static recovery of the captured bindings from the call site is defeated by the box reuse. The proper fix is checking the callback body against caller state at check time (closure inlining), which is follow-up-sized work - attempted variants (callback-tt substitution; union-find capture linking via def-chain walks) were evaluated and rejected because they either still miss the case or corrupt unrelated cache entries. The memoryrefget ret-alias adjustment from the original commit is retained. |
|
Heads-up to whoever is shepherding this PR: do not re-apply 4bd8bd5 / d3f31ce. Pushing 3b798de next (force-push), which supersedes the revert-and-pin approach:
Per direct instruction from Miles to implement the fix rather than document the hole. |
1329a76 to
c4168aa
Compare
The lock-effect registry entries, the higher-order lock(f, l) model, and all four lock testsets are merged into MilesCranmer#88 (ported to the dissolved src/safe layout and verified green on 1.12 and 1.13-rc3). The src/auto module layout this branch was built on was dissolved by MilesCranmer#87, so the remaining rename is superseded upstream.
c4168aa to
a3424c7
Compare
Problem
@safemisflags locked regions as violations. Reproduces on v0.4.6, Julia 1.12.6:The callback functor and the
Lockableboth flow intolock, an unknown callee, so the conservative fallback treats the call as consuming/escaping its arguments.Fix
Register
Base.lock,Base.unlock,Base.trylock,Base.islockedin the builtin effect registry (_populate_registry!) with emptywrites/consumes/ret_aliases. Locks serialize access; they never consume or write through their arguments' contents, so the conservative treatment is always a false positive for them.A pleasant consequence:
Base.Lockable(immutable struct, 1.12+) now works as a checked shared-mutable carrier. The wrapper itself is untracked (immutable), and payload access through thelock(f, l)do-block form checks cleanly at:functionscope and under recursive scopes (:module/:user).Testing
:functionand:modulescope passes; ordinary aliasing violations near blessed calls still throw.Basefunctions.Known remaining gaps (not addressed here)
lock(l); ...; unlock(l)regions still false-positive when the payload is written through field access in the same function (l.value[2] += 1): the write throughgetfieldof the live immutable wrapper is flagged as an aliased write. Pre-existing, independent of locks; reads pass.Threads.@spawnboundaries are flagged as consumes regardless of whether the thunk reads or writes (thunk bodies are not summarized yet).