Repository navigation
[soundness] P0: deferred call keeps a live reference, so moving the value into a task races #415
Description
The smallest .hy program that demonstrates it
// prog.hy
fn report(m map[string]int) int {
return m["task"]
}
fn worker(m map[string]int) {
m["task"]++
}
fn main() {
shared := map[string]int{}
defer report(shared)
task worker(move shared)
}$ hyb check prog.hy
prog.hy: OK (0 diagnostics)
Emitted Go, verbatim:
func main() {
shared := map[string]int{}
defer report(shared)
go worker(shared)
}defer report(shared) evaluates the argument now but calls report at function exit — after the spawn — while worker is writing the same map. go run reproduces it deterministically.
Environment: commit 8dd00028c7791813e56c586a3b77192bd57db2d8, hyb MVP-0, pinned go1.26.9 / rust 1.99.0, Windows 10.0.19045.
What the checker should say
REJECT with HYB-E3003 ("use/read after ownership was moved away").
A defer statement whose arguments capture a reference-bearing binding is a live use of that binding at function exit. move shared at the spawn transfers ownership before that use happens, so the deferred call reads a value that the sender no longer owns — the exact shape O5.2 forbids. The checker already reports this form when the deferred call is a closure capture:
// rejected today with HYB-E3003 "`shared` is read after ownership was moved away"
show := fn() { fmt.println("{shared[\"task\"]}") }
defer show()
task worker(move shared)The direct-argument form above is the same defect through a different path and is accepted.
What it actually said
$ hyb check prog.hy
prog.hy: OK (0 diagnostics)
exit code 0
Race evidence
Same shape with a real map access inside the deferred call (120000-iteration loops), hyb check still OK (0 diagnostics), emitted and run under go run (go1.26.9), 5 runs out of 5:
fatal error: concurrent map read and map write
fatal error: concurrent map read and map write
fatal error: concurrent map read and map write
fatal error: concurrent map read and map write
fatal error: concurrent map read and map write
Note for reproducers: len(m) inside the deferred call does not reproduce — len reads the map header, not the map, so the runtime detector stays quiet. The deferred call must actually index the map for the race to surface.
Claimed severity
P0 — data race reachable in the checked subset.
Anything else
Why this slips through. defer expr evaluates its arguments at the defer statement, which the checker treats as an ordinary read at that point — before the move. But the call is deferred to function exit, so the reference outlives the move. Tracking the argument as a use at the defer statement is not enough; the checker needs to keep it as a pending use at function exit, or emit HYB-E3003 at the spawn when a moved binding is captured by a live defer.
Interaction with scope_pop. Not related to #399: no block scope is involved here.
Suggested regression test. Register the minimal program as a corpus case with EXPECTED-VERDICT: REJECT (A1b/E3003), plus the closure form above as the already-rejecting twin and a control where the deferred call uses a different map and stays ACCEPT.
AI disclosure. Prepared by an AI agent, as permitted by BOUNTY.md. Every verdict and the runtime output above were produced by actually running hyb at the stated commit.
Activity
hy-check: corpus case and tests for the defer live-reference fix (lim…
hy-check: keep defer arguments live until function exit (fixes limitl…
hy-check: corpus case and tests for the defer live-reference fix (lim…
gelismarvel commentedon Oct 17, 2026
/claim #415
Fixes #415
Submitting verified fix PR for #415.
fix: reject moving a deferred binding into a task or consuming call (l…
Anekenonso commentedon Oct 17, 2026
Submitted a comprehensive fix in PR #422 covering task spawns, channel sends, local move rebinds, may-share peer aliasing, block scopes, and closures, backed by a hermetic regression test suite in compiler/crates/hy-check/tests/defer_move_soundness.rs (100% pass, 52/52 corpus agreement).
hy-check: guard the send arm too for defer live references (limitless…
fix: reject moving a deferred binding into a task or consuming call (l…
hy-check: guard the alias form of defer live references too (limitles…
G0st13 commentedon Oct 17, 2026
Thanks @exantiv and @Anekenonso — good to see three independent takes on this.
As the original reporter I have kept #418 updated while the competition arrived, and reading your test lists was useful: it surfaced the alias form (
defer report(alias)+task worker(move shared)), which my first cut missed because it keyed on the moved name rather than the alias/may-share component. That is now covered in #418 (deferred_conflict), so credit for the case goes to your suites.Current state of #418:
task worker(move shared)with a livedeferon it →HYB-E3003(A1b)ch <- move shared→HYB-E3003defer report(alias)+move shared→HYB-E3003(the case above)deferdeclared inside anifstill fires at function exit, so it is still guardedBacking: corpus
54-...-at-spawn.hy,55-...-at-send.hy,56-...-via-alias.hy, allREJECTwithHYB-E3003; corpus is 55/55 on verdict agreement; 6 unit tests inhy-check/tests/defer_live_ref.rsincluding two ACCEPT controls (deferred call reads a different map; no defer at all); 598 tests green; rebased onmain.One deliberate position, so it is explicit rather than accidental: I kept the check conservative — it fires at the transfer whether or not the
defercould be shown to run first. A path-sensitive variant would accept more programs, but the closure case makes "when does the deferred call run" genuinely hard to prove, and over-rejecting a rare safe shape seemed the better trade for this rule.@limitlessprojects — the three implementations differ in where the check lives (
loans/freezevsclosures.rs), so a comparison of false-positive behaviour on the ACCEPT controls may be the fastest way to pick one. Happy to adapt #418 to whatever shape you prefer.fix(hy-check): resolve closures.rs rebase and track pre-defer aliases (…
fix(hy-check): resolve closures.rs rebase and track pre-defer aliases (…
sonson0910 commentedon Oct 17, 2026
For maintainer triage cross-reference on the
STATUS.mddeferslot:2026-10-15T01:27:25Z) and PR fix(hy-check): enforce freeze and loan windows across defer and call-arg moves (#98) #99 (2026-10-15T01:28:53Z, triaged in wave-1, wave-2, andRecon (session-15/2-e)at fix(hy-check): enforce freeze and loan windows across defer and call-arg moves (#98) #99 (comment)) are the original wave-1 report and superset fix forStmt::DeferA1b/A7 freeze (HYB-E3003) and A2/A3 loan-window extension (HYB-E3101/HYB-E3102), opened 57 hours before [soundness] P0: deferred call keeps a live reference, so moving the value into a task races #415/hy-check: keep defer arguments live until function exit (fixes #415, #438) #418/fix(hy-check): reject moving a deferred binding or its pre-/post-defer aliases (#415, #438) #421/fix(hy-check): reject moves of bindings held by live deferred calls (fixes #415) #422/[soundness] P0: rebinding a name clears the freeze on storage a defer captured #438.94e4d79) is already rebased cleanly ontoorigin/main(07d63ec, post-fix(hy-check): preserve peer sharing/loans across shadows and rebinds and mark moves in statement expressions (fixes #393) #395/fix(emit): flush O8 slot loans at non-lexical last_use, on rebind, and in match some arms (#246) #247,mergeable=true,clean), rejects all [soundness] P0: deferred call keeps a live reference, so moving the value into a task races #415 and [soundness] P0: rebinding a name clears the freeze on storage a defer captured #438 shapes (spawn, send, alias, and pre-/post-defer alias across rebind), and also resolves thesession-15/2-a2calibration note (defer f(m); m = fresh; task g(move m)is accepted when moving the fresh value, while moving an alias of the deferred value is rejected).hy-check: fold the defer move-freeze into the single Stmt::Defer arm
Merge pr-421 (exantiv, fixes limitlessprojects#415 limitlessprojects#438
gelismarvel commentedon Oct 17, 2026
I am withdrawing my bounty claim for #415 (fixed by #421). As noted on #421, its regression tests and checker-corpus files came from @G0st13's earlier #418, so please do not pay this bounty out to me. How to allocate it, for example to @G0st13, is entirely up to the maintainers.