Skip to content

fix(core): drain effects registered during unload - #91

Open
Termina1 wants to merge 1 commit into
cordiverse:mainfrom
Termina1:fix/late-registration-during-unload
Open

fix(core): drain effects registered during unload#91
Termina1 wants to merge 1 commit into
cordiverse:mainfrom
Termina1:fix/late-registration-during-unload

Conversation

@Termina1

Copy link
Copy Markdown

While a fiber is unloading, a late async effect can still call ctx.plugin() — and it succeeds. But _unload has already grabbed and cleared the disposable list, so the new child's disposer is never called. After the parent is fully disposed, the child is still ACTIVE in the registry and its listeners keep firing. Nothing will ever clean it up.

This is easy to hit with HMR or config reconciliation: a plugin awaits something, its dependency goes away mid-await, the plugin wakes up during unload and registers a child.

Why it happens:

  • assertActive only checks uid, so it lets an UNLOADING fiber register new effects;
  • _unload calls this._disposables.clear() once and awaits that snapshot — anything added during those awaits goes into the now-empty list, and nobody ever reads it again.

The fix: keep draining. Instead of one pass over the snapshot, _unload loops until _disposables is empty, so anything registered mid-unload gets torn down too. I chose to tear down late children rather than reject late ctx.plugin() calls, so legitimate async effects that resolve mid-reload keep working — they just get disposed like everything else.

The loop is capped at 16 rounds, so a disposer that keeps registering new effects forever can't hang unload: it gets a ctx.logger.error and the leftovers are dropped. There's a test for that case too.

The new regression test fails on current main (child.uid is 2 instead of null, the orphan's listener still fires after dispose) and passes with the fix. Full suite: 165/165.

How I found this: I've been mechanizing the Cordis paper in Idris 2, mostly with AI agents doing the proof work under adversarial review: https://github.com/Termina1/dgamma. The paper's proof of Lemma 68 assumes every child registration is tied to a live step of the parent's activation, but the operational rules don't actually enforce that. So I had the agents check whether the real implementation has the same hole — and this race is it. The repo's README has the details and executable countermodels.

Side note: the same audit confirmed that name reuse is handled correctly here (callback identity + monotonic fiber uids), even though the paper's single raw-name renaming would conflate two components that share a freed name.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant