diff --git a/plugins/pstack/pi/schedule.ts b/plugins/pstack/pi/schedule.ts index fa0d2567..86a471ee 100644 --- a/plugins/pstack/pi/schedule.ts +++ b/plugins/pstack/pi/schedule.ts @@ -31,6 +31,9 @@ export class Scheduler { // nothing tells that run's re-arm of the old loop from any other wakeup. It // is refused them all, or the loop the user just ended would come back. sealed = false; + // A run is in flight: set by agent_start, cleared by agent_settled. Not + // ctx.isIdle(), which is also false during a manual compaction. + running = false; constructor(private readonly pi: ExtensionAPI) {} @@ -163,7 +166,11 @@ export function registerSchedule(pi: ExtensionAPI, scheduler: Scheduler, oneShot }, }); + pi.on("agent_start", () => { + scheduler.running = true; + }); pi.on("agent_settled", () => { + scheduler.running = false; scheduler.sealed = false; }); @@ -171,6 +178,8 @@ export function registerSchedule(pi: ExtensionAPI, scheduler: Scheduler, oneShot description: "Run a prompt on an interval (/loop 5m ), self-paced (/loop ), or stop (/loop stop)", async handler(args, ctx) { const cmd = parseLoop(args); + // Also true during a manual compaction, which no run is behind: the first + // prompt then waits for idle, but only a run in flight seals the slot. const midRun = !ctx.isIdle(); // sendUserMessage only starts the run, and a one-shot run disposes the // session as soon as the command returns, so there the command waits it out. @@ -180,7 +189,7 @@ export function registerSchedule(pi: ExtensionAPI, scheduler: Scheduler, oneShot // re-arm then comes from a later run and is not refused. if (midRun) { scheduler.scheduleWakeup(0, prompt, ctx); - ctx.ui.notify("The loop starts when the current run ends.", "info"); + ctx.ui.notify("The loop starts once the session is idle.", "info"); return; } if (!oneShot.exits(ctx)) { @@ -197,18 +206,18 @@ export function registerSchedule(pi: ExtensionAPI, scheduler: Scheduler, oneShot ctx.ui.notify(`${cmd.reason ? `${cmd.reason} ` : ""}Usage: /loop [interval like 5m or 1h] , or /loop stop`, "info"); return; case "stop": - ctx.ui.notify(scheduler.stopAll(midRun) ? "Loop stopped." : "No loop was running.", "info"); + ctx.ui.notify(scheduler.stopAll(scheduler.running) ? "Loop stopped." : "No loop was running.", "info"); return; case "fixed": { const seconds = Math.max(MIN_DELAY_S, cmd.seconds); - scheduler.stopAll(midRun); + scheduler.stopAll(scheduler.running); scheduler.startLoop(seconds, cmd.prompt, ctx); ctx.ui.notify(`Looping every ${seconds}s. /loop stop ends it.`, "info"); await fire(cmd.prompt); return; } case "dynamic": - scheduler.stopAll(midRun); + scheduler.stopAll(scheduler.running); scheduler.startSelfPaced(); await fire(dynamicPrompt(cmd.prompt)); } diff --git a/tests/pi/interaction.test.mjs b/tests/pi/interaction.test.mjs index a6fa79d6..09ff7368 100644 --- a/tests/pi/interaction.test.mjs +++ b/tests/pi/interaction.test.mjs @@ -357,6 +357,7 @@ describe("/loop", () => { const { pi, ctx, run, ui } = loop({ idle: () => idle }); await run("watch PR 42"); idle = false; + await pi.emit("agent_start", {}, ctx); await run("stop"); expect(ui.calls.at(-1).message).toBe("Loop stopped."); const refused = await pi.call("schedule_wakeup", { delaySeconds: 60, prompt: rearm }, { ...ctx, ui }); @@ -373,6 +374,7 @@ describe("/loop", () => { let idle = false; const { pi, ctx, run, ui } = loop({ idle: () => idle }); const wake = () => pi.call("schedule_wakeup", { delaySeconds: 60, prompt: "later" }, { ...ctx, ui }); + await pi.emit("agent_start", {}, ctx); await run("stop"); expect(ui.calls.at(-1).message).toBe("No loop was running."); expect((await wake()).details).toEqual({ refused: true }); @@ -389,8 +391,9 @@ describe("/loop", () => { const wake = (params) => pi.call("schedule_wakeup", params, { ...ctx, ui }); await run("watch old"); idle = false; + await pi.emit("agent_start", {}, ctx); await run("watch new"); - expect(ui.calls.at(-1).message).toBe("The loop starts when the current run ends."); + expect(ui.calls.at(-1).message).toBe("The loop starts once the session is idle."); expect((await wake({ delaySeconds: 60, prompt: "/loop watch old" })).details).toEqual({ refused: true }); expect((await wake({ stop: true })).details).toEqual({ cancelled: false }); jest.advanceTimersByTime(60_000); @@ -412,6 +415,7 @@ describe("/loop", () => { test("a fixed loop asked for during a run sends its first prompt once that run settles", async () => { let idle = false; const { pi, ctx, run } = loop({ idle: () => idle }); + await pi.emit("agent_start", {}, ctx); await run("5m check the deploy"); jest.advanceTimersByTime(30_000); expect(pi.userMessages).toEqual([]); @@ -421,6 +425,31 @@ describe("/loop", () => { expect(pi.userMessages.map((m) => m.content)).toEqual(["check the deploy"]); }); + // During a manual compaction isIdle() is false with no run in flight, and + // no agent_settled follows when it ends. + test("a self-paced loop started during a manual compaction waits for idle, then re-arms after its first iteration", async () => { + let idle = false; + const { pi, ctx, run, ui } = loop({ idle: () => idle }); + await run("watch the deploy"); + expect(ui.calls.at(-1).message).toBe("The loop starts once the session is idle."); + idle = true; + jest.advanceTimersByTime(1_000); + expect(pi.userMessages).toHaveLength(1); + idle = false; + await pi.emit("agent_start", {}, ctx); + const rearm = await pi.call("schedule_wakeup", { delaySeconds: 60, prompt: "/loop watch the deploy" }, { ...ctx, ui }); + expect(resultText(rearm)).toContain("Wakeup scheduled"); + }); + + test("/loop stop during a manual compaction does not refuse the next run's wakeup", async () => { + let idle = false; + const { pi, ctx, run, ui } = loop({ idle: () => idle }); + await run("stop"); + await pi.emit("agent_start", {}, ctx); + const wake = await pi.call("schedule_wakeup", { delaySeconds: 60, prompt: "later" }, { ...ctx, ui }); + expect(resultText(wake)).toContain("Wakeup scheduled"); + }); + for (const [what, started, prompt] of [ ["a live loop's re-arm in other words than its prompt", "watch PR 42", "/loop Watch PR 42."], ["a /loop prompt with no loop started", null, "/loop babysit PR 42"], diff --git a/tla/PiScheduler.matrix b/tla/PiScheduler.matrix new file mode 100644 index 00000000..45d787da --- /dev/null +++ b/tla/PiScheduler.matrix @@ -0,0 +1,70 @@ +# Matrix for tlc-matrix.sh. w is MaxWakeups (scheduleWakeup calls), l is +# MaxLoops (startLoop calls). The code has exactly one wakeup slot and one +# event loop, so there is no slot count or worker count to vary. +# +# "strict" is the host the comments in schedule.ts assume: not idle means a +# run is in flight, a fired prompt is a run at once, and nothing else starts a +# run while a /loop start waits in the slot. Every property holds there. + +spec PiScheduler.tla +check INVARIANTS TypeOK OneWakeup TimersOwned NoCancelledDelivery NoRearmByCutRun SealedOnlyAgainstCutRun FreshRunNotRefused StartSurvivesRuns OneLoopKind StoppedIsTerminal +check PROPERTIES IdleDelivery NothingFiresAfterStop +reach ParkedWakeup | strict w=2 +reach DueWhileIdle | strict w=2 +reach TickWhileBusy | strict w=2 +reach StartBehindCutRun | strict w=2 +reach LoopAndWakeup | strict w=2 +reach SelfPacedRearm | strict w=2 +reach StoppedAfterDelivery | strict w=2 +reach ShutdownCancelled | strict w=2 +reach AllDelivered | strict w=2 +run strict w=0 l=1 | MaxWakeups=0 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=1 l=0 | MaxWakeups=1 MaxLoops=0 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=1 l=1 | MaxWakeups=1 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=2 l=1 | MaxWakeups=2 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=3 l=2 | MaxWakeups=3 MaxLoops=2 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=5 l=2 | MaxWakeups=5 MaxLoops=2 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE + +# Liveness, under the fairness in Spec. It holds on every host: a /loop start +# that a run replaces counts as cancelled. +spec PiScheduler.tla +check PROPERTIES WakeupDelivered +run strict w=1 l=1 liveness | MaxWakeups=1 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run strict w=2 l=1 liveness | MaxWakeups=2 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=FALSE +run host=all w=2 l=1 liveness | MaxWakeups=2 MaxLoops=1 CompactCmd=TRUE StartGap=TRUE StartRace=TRUE + +# All three host behaviours on. The timer, delivery, stop and sealed +# properties do not depend on the host. +spec PiScheduler.tla +check INVARIANTS TypeOK OneWakeup TimersOwned NoCancelledDelivery SealedOnlyAgainstCutRun FreshRunNotRefused OneLoopKind StoppedIsTerminal +check PROPERTIES IdleDelivery NothingFiresAfterStop +run host=all w=3 l=2 | MaxWakeups=3 MaxLoops=2 CompactCmd=TRUE StartGap=TRUE StartRace=TRUE + +# One host behaviour at a time. First the sealed properties that still hold +# with it on, then the ones that fail. The failing runs are the record of each +# finding and are expected to FAIL; do not weaken the property. + +# /loop during a manual compaction. Every property holds: the seal follows the +# extension's own run flag, not isIdle(), so a loop started during a +# compaction runs and re-arms. +spec PiScheduler.tla +check INVARIANTS TypeOK NoRearmByCutRun SealedOnlyAgainstCutRun FreshRunNotRefused StartSurvivesRuns +reach CompactionLoopRearmed | host=compact +run host=compact holds w=3 l=2 | MaxWakeups=3 MaxLoops=2 CompactCmd=TRUE StartGap=FALSE StartRace=FALSE + +# A gap between fire() and the run becoming active. +spec PiScheduler.tla +check INVARIANTS TypeOK SealedOnlyAgainstCutRun FreshRunNotRefused StartSurvivesRuns +reach StoppedLoopRearmed | host=gap +run host=gap holds w=3 l=2 | MaxWakeups=3 MaxLoops=2 CompactCmd=FALSE StartGap=TRUE StartRace=FALSE +spec PiScheduler.tla +check INVARIANTS NoRearmByCutRun +run finding rearm-after-stop-in-gap w=2 l=1 | MaxWakeups=2 MaxLoops=1 CompactCmd=FALSE StartGap=TRUE StartRace=FALSE + +# Another run starts while a /loop start waits in the slot. +spec PiScheduler.tla +check INVARIANTS TypeOK NoRearmByCutRun SealedOnlyAgainstCutRun FreshRunNotRefused +run host=race holds w=3 l=2 | MaxWakeups=3 MaxLoops=2 CompactCmd=FALSE StartGap=FALSE StartRace=TRUE +spec PiScheduler.tla +check INVARIANTS StartSurvivesRuns +run finding loop-start-replaced w=2 l=1 | MaxWakeups=2 MaxLoops=1 CompactCmd=FALSE StartGap=FALSE StartRace=TRUE diff --git a/tla/PiScheduler.mutations b/tla/PiScheduler.mutations new file mode 100644 index 00000000..9f244df4 --- /dev/null +++ b/tla/PiScheduler.mutations @@ -0,0 +1,127 @@ +# Mutations for mutate.py. Each one swaps a piece of PiScheduler.tla for a +# plausible bug in schedule.ts and names the one property that must fail on +# it. Each mutation runs on one host where the unmutated spec passes every +# property it checks, strict unless the bug needs CompactCmd, so a DETECTED +# line is the mutation's doing. + +mutation scheduleWakeup does not cancel the pending wakeup first +detects OneWakeup +only strict w=2 +- /\ wtimer' = [Cleared EXCEPT ![nextW] = "armed"] ++ /\ wtimer' = [wtimer EXCEPT ![nextW] = "armed"] + +mutation the idle retry does not keep its new timer handle +detects TimersOwned +only strict w=2 +- /\ slot' = w ++ /\ slot' = None + +mutation cancel does not stop a timer whose delay has already passed +detects NoCancelledDelivery +only strict w=2 +- Cleared == [w \in W |-> IF w = slot THEN "off" ELSE wtimer[w]] ++ Cleared == [w \in W |-> IF w = slot /\ wtimer[w] = "armed" THEN "off" ELSE wtimer[w]] + +mutation schedule_wakeup ignores sealed +detects NoRearmByCutRun +only strict w=2 +- LET refused == sealed IN ++ LET refused == FALSE IN + +mutation agent_settled does not clear sealed +detects SealedOnlyAgainstCutRun +only strict w=2 +- /\ sealed' = FALSE ++ /\ sealed' = sealed + +mutation stopAll seals whether or not a run is in flight +detects FreshRunNotRefused +only strict w=2 +- /\ sealed' = (sealed \/ running) ++ /\ sealed' = TRUE + +# The bug before the fix: a /loop during a manual compaction sealed the slot +# against a run that was not there, and the next run was refused. +mutation /loop seals whenever the session is not idle, compaction included +detects FreshRunNotRefused +only host=compact +- /\ sealed' = (sealed \/ running) ++ /\ sealed' = (sealed \/ midRun) + +mutation /loop seals during a compaction, so the loop it starts cannot re-arm +detects reach:CompactionLoopRearmed +only host=compact +- /\ sealed' = (sealed \/ running) ++ /\ sealed' = (sealed \/ midRun) + +mutation agent_settled does not clear the running flag +detects SealedOnlyAgainstCutRun +only host=compact +- /\ running' = FALSE ++ /\ running' = running + +mutation stop: true cancels a sealed slot +detects StartSurvivesRuns +only strict w=2 +- LET guarded == sealed IN ++ LET guarded == FALSE IN + +mutation a fixed /loop does not end the self-paced loop +detects OneLoopKind +only strict w=2 +- /\ selfPaced' = (c = "dynamic") ++ /\ selfPaced' = (c = "dynamic" \/ (c = "fixed" /\ selfPaced)) + +mutation session_shutdown leaves the interval running +detects StoppedIsTerminal +only strict w=2 +- /\ Cancel /\ StopLoop ++ /\ Cancel /\ UNCHANGED loopVars + +mutation deliver does not check that the session is idle +detects IdleDelivery +only strict w=2 +- /\ ~down /\ wtimer[w] = "due" /\ Idle ++ /\ ~down /\ wtimer[w] = "due" + +mutation stopLoop clears the field but not the interval +detects NothingFiresAfterStop +only strict w=2 +- StoppedLoop == [l \in L |-> IF l = loop THEN "off" ELSE ltimer[l]] ++ StoppedLoop == ltimer + +mutation a wakeup that finds the session busy is dropped, not re-armed +detects WakeupDelivered +only strict w=2 +- /\ wtimer' = [wtimer EXCEPT ![w] = "armed"] ++ /\ wtimer' = [wtimer EXCEPT ![w] = "off"] + +# The next two are not code bugs. They weaken assumption A8 and show that +# each strong-fairness conjunct is needed: with weak fairness a session that +# is busy at every expiry, or that turns busy before every callback, starves +# the wakeup. +mutation only weak fairness on delivery +detects WakeupDelivered +only strict w=2 +- /\ SF_vars(DeliverFire(w)) ++ /\ WF_vars(DeliverFire(w)) + +mutation only weak fairness on expiry while idle +detects WakeupDelivered +only strict w=2 +- /\ SF_vars(Idle /\ Expire(w)) ++ /\ WF_vars(Idle /\ Expire(w)) + +# Not a code bug: it removes the model's bound on scheduleWakeup calls, to +# show that TypeOK constrains the state. +mutation the bound on wakeup ids is not enforced +detects TypeOK +only strict w=2 +- /\ nextW <= MaxWakeups ++ /\ TRUE + +mutation /loop during a run fires at once and does not take the slot +detects reach:StartBehindCutRun +only strict w=2 +- /\ IF c # "stop" /\ midRun THEN Arm(IF running THEN "cmd" ELSE "compact", "plain") ELSE Cancel ++ /\ IF FALSE THEN Arm("cmd", "plain") ELSE Cancel diff --git a/tla/PiScheduler.tla b/tla/PiScheduler.tla new file mode 100644 index 00000000..0fb0a601 --- /dev/null +++ b/tla/PiScheduler.tla @@ -0,0 +1,343 @@ +---- MODULE PiScheduler ---- +(* The Pi wakeup and /loop scheduler: one pending wakeup, one fixed-interval + loop and one self-paced loop per session, and the `sealed` flag that stops + a run the user cut off from re-arming the loop. + + Source followed: + plugins/pstack/pi/schedule.ts:23-93 class Scheduler + plugins/pstack/pi/schedule.ts:131-226 registerSchedule: the + schedule_wakeup tool, the + agent_start and agent_settled + handlers, /loop + plugins/pstack/pi/index.ts:29-34 session_shutdown calls stopAll() + + One Node.js event loop runs every task to completion, so each action below + is one task: a timer callback, a tool call, a command handler, an event + handler. There is no lock and no program counter per thread. The state a + thread model would keep in a pc is in `run` (the session's run) and in the + timer tables. + + A wakeup that finds the session busy re-arms itself (schedule.ts:49-52). + It waits in `wtimer` as "armed" or "due" and only its own timer wakes it. + The user can always type another command, so a wakeup that is dropped while + it waits never shows as a TLC deadlock. It shows as a violation of the + liveness property WakeupDelivered. + + Assumptions. The code does not guarantee these; the Pi host or Node does. + A1 clearTimeout and clearInterval stop a timer whose delay has passed but + whose callback has not started (Node's timer lists). + A2 schedule_wakeup runs only while a run is active, and the active run is + the only caller. + A3 ctx.isIdle() is false exactly while a run is active or a manual + compaction is in progress (Pi 1.0.0, agent-session.js:1038-1039). + A4 Every active run ends, and Pi then clears the run and calls the + agent_settled handler with no timer or input task between the two + (agent-session.js:671-677, 1369-1377). + A5 Not one-shot mode: oneShot.exits(ctx) is false, so schedule.ts:155-157 + and 199-202 are not modelled. + A6 A wakeup or loop prompt is plain text or "/loop ". A prompt + that is itself "/loop stop" or "/loop 5m ..." is not modelled. + A7 No scheduler call follows session_shutdown. + A8 Strong fairness, for WakeupDelivered only: the session is idle at some + expiry of the wakeup's timer, and the callback then runs before a new + run starts. In real time: the session stays idle for IDLE_RETRY_MS. + Weak fairness is not enough. The mutation "only weak fairness" in + PiScheduler.mutations gives the starvation trace. + A9 Pi emits agent_start to extensions in the same task chain that sets + its run-active flag (agent-session.js:1352, then pi-agent-core + agent-loop.js:50 before any model call), and agent_settled follows + every run, aborted or failed (the finally at agent-session.js:1369- + 1377). So the extension's `running` flag is TRUE exactly while + run = "active", and no schedule_wakeup call precedes agent_start. + + Three constants switch on host behaviour that the comments in schedule.ts + assume away. With all three FALSE every property holds. + CompactCmd the user can run /loop while a manual compaction is in + progress (Pi interactive-mode.js:2652-2658 does this). + StartGap a prompt that fire() sends becomes an active run in a later + task, so isIdle() stays true in between (Pi's prompt() awaits + hooks before agent-session.js:1352). + StartRace another run can start while a /loop start waits in the slot: + the user types a prompt, or an interval tick lands, before the + wakeup's next retry. *) +EXTENDS Naturals, FiniteSets + +CONSTANTS MaxWakeups, MaxLoops, CompactCmd, StartGap, StartRace + +None == 0 +W == 1..MaxWakeups \* one id per scheduleWakeup call, which is one deliver closure +L == 1..MaxLoops \* one id per startLoop call + +VARIABLES + slot, loop, selfPaced, sealed, \* Scheduler fields, schedule.ts:24-36 + running, \* Scheduler.running: a run is in flight, schedule.ts:36 + wtimer, ltimer, \* Node's timers: "off", "armed", or "due" (delay passed, callback not yet run) + run, compacting, down, \* the Pi session + startedBy, \* the wakeup whose prompt started the current run, else None + nextW, nextL, wby, wkind, \* next free id; who scheduled each wakeup ("cmd": /loop during a run, + \* "compact": /loop during a compaction) and what its prompt is + fired, cancelled, \* history: wakeups delivered; wakeups cancelled or replaced + cut, \* history: the user ran /loop while the current run was in flight + quiet, \* history: the last /loop was "stop" and no run was in flight + refusedFresh, startStolen \* history: a run that was not cut was refused; a run cancelled a /loop start + +slotVars == <> +loopVars == <> +session == <> +history == <> +vars == <> + +Init == /\ slot = None /\ loop = None /\ selfPaced = FALSE /\ sealed = FALSE /\ running = FALSE + /\ wtimer = [w \in W |-> "off"] /\ ltimer = [l \in L |-> "off"] + /\ run = "none" /\ compacting = FALSE /\ down = FALSE /\ startedBy = None + /\ nextW = 1 /\ nextL = 1 + /\ wby = [w \in W |-> "tool"] /\ wkind = [w \in W |-> "plain"] + /\ fired = {} /\ cancelled = {} + /\ cut = FALSE /\ quiet = FALSE /\ refusedFresh = FALSE /\ startStolen = FALSE + +Idle == run # "active" /\ ~compacting \* ctx.isIdle() +Started == IF StartGap THEN "transit" ELSE "active" \* the run state after fire() on an idle session +Pending == IF slot = None THEN {} ELSE {slot} +StartPending == slot # None /\ wby[slot] # "tool" \* a /loop start waits in the slot +LiveW == {w \in W : wtimer[w] # "off"} +LiveL == {l \in L : ltimer[l] # "off"} + +\* clearTimeout(this.wakeup), schedule.ts:62, and clearInterval(this.loop), :75. +Cleared == [w \in W |-> IF w = slot THEN "off" ELSE wtimer[w]] +StoppedLoop == [l \in L |-> IF l = loop THEN "off" ELSE ltimer[l]] + +\* cancelWakeup, schedule.ts:60-65. +Cancel == /\ wtimer' = Cleared /\ slot' = None + /\ cancelled' = cancelled \cup Pending + /\ UNCHANGED <> + +\* scheduleWakeup, schedule.ts:44-58: cancel, arm a new timer, keep its handle. +Arm(by, kind) == + /\ nextW <= MaxWakeups + /\ wtimer' = [Cleared EXCEPT ![nextW] = "armed"] + /\ slot' = nextW /\ nextW' = nextW + 1 + /\ wby' = [wby EXCEPT ![nextW] = by] /\ wkind' = [wkind EXCEPT ![nextW] = kind] + /\ cancelled' = cancelled \cup Pending + +\* stopLoop, schedule.ts:73-78, and startLoop after it, :67-71. +StopLoop == ltimer' = StoppedLoop /\ loop' = None /\ UNCHANGED nextL +StartLoop == /\ nextL <= MaxLoops + /\ ltimer' = [StoppedLoop EXCEPT ![nextL] = "armed"] + /\ loop' = nextL /\ nextL' = nextL + 1 + +\* fire, schedule.ts:40-42, on an idle session. With no gap the run is active +\* at once and Pi emits agent_start (A9), schedule.ts:169-171. +Fire(by) == run' = Started /\ running' = (Started = "active") /\ startedBy' = by + +\* The user types /loop stop, /loop ("fixed") or +\* /loop ("dynamic"): schedule.ts:181-224. The first prompt waits +\* whenever the session is not idle; the seal needs a run in flight. +Cmd(c) == + LET midRun == ~Idle IN \* :183 + /\ ~down + /\ compacting => CompactCmd + /\ sealed' = (sealed \/ running) \* :90, :209 + /\ selfPaced' = (c = "dynamic") \* :89, :81 + /\ IF c = "fixed" THEN StartLoop ELSE StopLoop \* :91, :214 + /\ IF c # "stop" /\ midRun THEN Arm(IF running THEN "cmd" ELSE "compact", "plain") ELSE Cancel \* :87, :190-191 + /\ IF c # "stop" /\ ~midRun THEN Fire(None) ELSE UNCHANGED <> \* :195-197 + \* A start that lands in the StartGap window sends its first prompt into the + \* run in transit. That run's re-arm may then be the new loop's own, so only + \* a stop marks the run in transit as cut. + /\ cut' = (cut \/ run = "active" \/ (run = "transit" /\ c = "stop")) + /\ quiet' = (c = "stop" /\ run = "none") + /\ UNCHANGED <> + +\* The active run calls schedule_wakeup with a delay and a prompt: schedule.ts:145-165. +ToolSchedule(kind) == + LET refused == sealed IN \* :148 + /\ run = "active" /\ ~down + /\ IF refused + THEN /\ refusedFresh' = (refusedFresh \/ ~cut) + /\ UNCHANGED <> + ELSE /\ Arm("tool", kind) \* :159 + /\ startStolen' = (startStolen \/ StartPending) + /\ UNCHANGED refusedFresh + /\ UNCHANGED <> + +\* The active run calls schedule_wakeup with stop: true: schedule.ts:139-144. +ToolStop == + LET guarded == sealed IN \* :141 + /\ run = "active" /\ ~down + /\ IF guarded + THEN /\ refusedFresh' = (refusedFresh \/ (~cut /\ slot # None)) + /\ UNCHANGED <> + ELSE /\ Cancel + /\ startStolen' = (startStolen \/ StartPending) + /\ UNCHANGED refusedFresh + /\ UNCHANGED <> + +\* Node: the wakeup timer's delay passes and its callback is queued. +Expire(w) == + /\ ~down /\ wtimer[w] = "armed" + /\ wtimer' = [wtimer EXCEPT ![w] = "due"] + /\ UNCHANGED <> + +\* deliver on a busy session, schedule.ts:49-52: re-arm and keep the new handle. +Retry(w) == + /\ ~down /\ wtimer[w] = "due" /\ ~Idle + /\ wtimer' = [wtimer EXCEPT ![w] = "armed"] + /\ slot' = w + /\ UNCHANGED <> + +\* deliver on an idle session, schedule.ts:53-54. A "/loop " prompt is +\* the self-paced re-arm: Pi runs the /loop handler in place, :219-222. +DeliverFire(w) == + /\ ~down /\ wtimer[w] = "due" /\ Idle + /\ wtimer' = [wtimer EXCEPT ![w] = "off"] + /\ slot' = None + /\ fired' = fired \cup {w} + /\ Fire(w) + /\ IF wkind[w] = "loop" THEN selfPaced' = TRUE /\ StopLoop + ELSE UNCHANGED <> + /\ quiet' = FALSE + /\ UNCHANGED <> + +\* Node: the interval's delay passes; then its callback, schedule.ts:69, which +\* fires on an idle session and drops the tick on a busy one. +LExpire(l) == + /\ ~down /\ ltimer[l] = "armed" + /\ ltimer' = [ltimer EXCEPT ![l] = "due"] + /\ UNCHANGED <> + +TickFire(l) == + /\ ~down /\ ltimer[l] = "due" /\ Idle + /\ StartRace \/ ~StartPending + /\ ltimer' = [ltimer EXCEPT ![l] = "armed"] + /\ Fire(None) + /\ quiet' = FALSE + /\ UNCHANGED <> + +TickDrop(l) == + /\ ~down /\ ltimer[l] = "due" /\ ~Idle + /\ ltimer' = [ltimer EXCEPT ![l] = "armed"] + /\ UNCHANGED <> + +\* The user types a prompt on an idle session. +UserPrompt == + /\ ~down /\ run = "none" /\ ~compacting + /\ StartRace \/ ~StartPending + /\ Fire(None) + /\ quiet' = FALSE + /\ UNCHANGED <> + +\* With StartGap: the prompt in transit becomes the active run and Pi emits +\* agent_start: schedule.ts:169-171. +RunStart == + /\ ~down /\ run = "transit" + /\ run' = "active" + /\ running' = TRUE + /\ UNCHANGED <> + +\* The run settles and Pi emits agent_settled: schedule.ts:172-175. +RunSettle == + /\ ~down /\ run = "active" + /\ run' = "none" /\ startedBy' = None + /\ running' = FALSE + /\ sealed' = FALSE + /\ cut' = FALSE + /\ UNCHANGED <> + +\* Manual compaction. Pi aborts the run first, so none is in flight. +CompactStart == + /\ ~down /\ run = "none" /\ ~compacting + /\ compacting' = TRUE + /\ UNCHANGED <> + +CompactEnd == + /\ ~down /\ compacting + /\ compacting' = FALSE + /\ UNCHANGED <> + +\* session_shutdown: stopAll() with midRun false, index.ts:29-34. +Shutdown == + /\ ~down + /\ down' = TRUE + /\ Cancel /\ StopLoop + /\ selfPaced' = FALSE + /\ UNCHANGED <> + +\* Stutter after shutdown so that the end is not reported as a deadlock. +Done == down /\ UNCHANGED vars + +Next == \/ \E c \in {"stop", "fixed", "dynamic"} : Cmd(c) + \/ \E k \in {"plain", "loop"} : ToolSchedule(k) + \/ ToolStop + \/ \E w \in W : Expire(w) \/ Retry(w) \/ DeliverFire(w) + \/ \E l \in L : LExpire(l) \/ TickFire(l) \/ TickDrop(l) + \/ UserPrompt \/ RunStart \/ RunSettle + \/ CompactStart \/ CompactEnd \/ Shutdown \/ Done + +\* Runs start and end and compaction ends. No fairness on anything the user or +\* the agent chooses to do. The two strong conjuncts are assumption A8. +Fairness == /\ WF_vars(RunStart) /\ WF_vars(RunSettle) /\ WF_vars(CompactEnd) + /\ \A w \in W : /\ WF_vars(Retry(w)) + /\ SF_vars(Idle /\ Expire(w)) + /\ SF_vars(DeliverFire(w)) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ slot \in W \cup {None} /\ loop \in L \cup {None} + /\ selfPaced \in BOOLEAN /\ sealed \in BOOLEAN /\ running \in BOOLEAN + /\ wtimer \in [W -> {"off", "armed", "due"}] /\ ltimer \in [L -> {"off", "armed", "due"}] + /\ run \in {"none", "transit", "active"} /\ (run = "transit" => StartGap) + /\ running = (run = "active") \* A9 + /\ compacting \in BOOLEAN /\ down \in BOOLEAN + /\ startedBy \in W \cup {None} /\ (run = "none" => startedBy = None) + /\ nextW \in 1..(MaxWakeups + 1) /\ nextL \in 1..(MaxLoops + 1) + /\ wby \in [W -> {"tool", "cmd", "compact"}] /\ wkind \in [W -> {"plain", "loop"}] + /\ fired \subseteq W /\ cancelled \subseteq W + /\ cut \in BOOLEAN /\ quiet \in BOOLEAN + /\ refusedFresh \in BOOLEAN /\ startStolen \in BOOLEAN + +\* (1) At most one wakeup timer is alive. +OneWakeup == Cardinality(LiveW) <= 1 +\* Ownership: a timer is alive exactly when the Scheduler field holds its handle. +TimersOwned == LiveW = Pending /\ LiveL = (IF loop = None THEN {} ELSE {loop}) +\* (2) A wakeup that was cancelled or replaced never delivers its prompt. +NoCancelledDelivery == fired \cap cancelled = {} +\* (3) A run the user cut off with /loop never has a wakeup of its own pending. +NoRearmByCutRun == cut => (slot = None \/ wby[slot] = "cmd") +\* (3) sealed is set only against a run that /loop cut off, and is clear once that run settles... +SealedOnlyAgainstCutRun == sealed => (run = "active" /\ cut) +\* ...so a run that started after the /loop command is never refused. +FreshRunNotRefused == ~refusedFresh +\* The /loop start that waits in the slot is cancelled only by /loop or shutdown, never by a run. +StartSurvivesRuns == ~startStolen +\* The fixed loop and the self-paced loop are never both live. +OneLoopKind == ~(loop # None /\ selfPaced) +\* (5), terminal state: after /loop stop with no run in flight, and after +\* shutdown, no timer is pending and no loop is live. +Terminal == slot = None /\ loop = None /\ ~selfPaced /\ LiveW = {} /\ LiveL = {} +StoppedIsTerminal == (quiet \/ down) => Terminal +\* (4) The wakeup path delivers only to an idle session. +IdleDelivery == [][fired' # fired => Idle]_vars +\* (5) After /loop stop with no run in flight, nothing fires again. +Fires == fired' # fired \/ \E l \in L : TickFire(l) +NothingFiresAfterStop == [][quiet => ~Fires]_vars +\* (6) A pending wakeup is delivered unless it is cancelled or replaced. +WakeupDelivered == \A w \in W : (wtimer[w] # "off") ~> (w \in fired \/ w \in cancelled) + +\* Reachable states the properties depend on (reach lines in PiScheduler.matrix). +ParkedWakeup == \E w \in W : wtimer[w] = "due" /\ ~Idle \* a due wakeup waits for idle +DueWhileIdle == \E w \in W : wtimer[w] = "due" /\ Idle \* a stop can land before the callback +TickWhileBusy == \E l \in L : ltimer[l] = "due" /\ ~Idle \* a tick about to be dropped +StartBehindCutRun == sealed /\ cut /\ StartPending \* a /loop start waits behind the run it cut +LoopAndWakeup == loop # None /\ slot # None \* the interval and a wakeup both alive +SelfPacedRearm == selfPaced /\ slot # None /\ wkind[slot] = "loop" \* the self-paced loop's own re-arm pending +StoppedAfterDelivery == quiet /\ fired # {} \* /loop stop on an idle session that had fired +ShutdownCancelled == down /\ cancelled # {} \* shutdown cancelled a pending wakeup +AllDelivered == W # {} /\ fired = W \* every wakeup the bound allows was delivered +\* The consequence of each finding on the host that allows it. +\* CompactCmd: a self-paced loop started during a compaction is in its first +\* iteration and that run's own re-arm is pending. +CompactionLoopRearmed == SelfPacedRearm /\ startedBy # None /\ wby[startedBy] = "compact" +\* StartGap: a wakeup fired, the user stopped the loop, and the run re-armed it. +StoppedLoopRearmed == cut /\ fired # {} /\ slot # None /\ wby[slot] = "tool" /\ wkind[slot] = "loop" +====