Repository navigation
fix(pi): seal the wakeup slot only against a run in flight - #237
Merged
Merged
Conversation
/loop treated any non-idle session as a run in flight. Pi is also not idle during a manual compaction, and it emits agent_settled only when a run ends, so a /loop typed during a compaction left the slot sealed and the next run was refused every wakeup. The scheduler now tracks a run from agent_start to agent_settled and seals only then. The TLA+ model of the scheduler comes with the change; two of its runs still fail by design and record narrower findings this does not fix.
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
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.
Why
A
/loopcommand typed while Pi compacts the session left the scheduler refusing wakeups for a run the command never interrupted. A self-paced loop started during/compactran one iteration and stopped, and/loop stopduring/compactmade the next run unable to schedule a wakeup. The command read "not idle" as "a run is in flight", but Pi is also not idle during a compaction, and it emitsagent_settledonly when a run ends.What changed
agent_starttoagent_settledand seals the wakeup slot only while one is in flight. A/loopduring a compaction still waits for idle before its first prompt.tla/holds a TLA+ model of the scheduler with its TLC matrix and mutations file.Scope
This PR fixes the compaction case. The model records two narrower findings that it leaves open, and its matrix exits 1 because of them: a
/loop stopthat lands between a prompt being sent and its run starting, and a new run that replaces a queued loop start within a second of the previous run ending. It bumps no version, so the fix reaches installs with the next release. No CI job runs the model yet.Blast Radius
Only the Pi extension changes. If Pi ever skipped
agent_start, a/loopduring that run would not seal, and the stopped loop could return for one iteration. Pi emitsagent_settledfrom afinallyblock, so the flag cannot stay set after a run.Verification
tests/pi/interaction.test.mjsfailed on the old code with "Not scheduled" where "Wakeup scheduled" is required, and pass on the new code.bun test tests/reports 1180 pass, 36 skip, 0 fail.bun tools/typecheck-pi.mjsexits 0.