708722b7ff
El SDK CI - dev / build-and-test (pull_request) Has started running
Cancellation-token control channel checked at every step boundary lets a coordinator PAUSE/RESUME/REDIRECT/KILL a running worker mid-task instead of waiting for the whole (possibly wrong) plan to finish. Bounded purviews mean no half-committed state to unwind on interrupt. Includes a proof harness (proof.el, run.sh) comparing a broken non-interruptible worker against the new one under identical kill/redirect/pause timing. Distinct from the already-preserved swarm-ccr orchestrator (fan-out/ converge dispatch): this is single-worker interruptibility, a complementary mechanism, not a duplicate.
181 lines
8.8 KiB
EmacsLisp
181 lines
8.8 KiB
EmacsLisp
// proof.el — Proof of native interruptibility for Neuron-dispatched agents.
|
|
//
|
|
// Concatenated after runtime/swarm.el (see run.sh). Demonstrates, with raw
|
|
// before/after counts, that a dispatched worker interrupted MID-TASK stops
|
|
// instantly (not after finishing the wrong workflow), absorbs a redirect
|
|
// (re-plans, keeping progress), or terminates cleanly.
|
|
//
|
|
// Three scenarios on the SAME 12-step plan, SAME per-step cost, SAME signal
|
|
// timing (sent ~50ms in ≈ after step 3):
|
|
// A. BASELINE — the broken Claude-style worker: no mid-loop signal check.
|
|
// A kill sent at step ~3 is ignored until the whole plan finishes → all 12
|
|
// steps run = wasted work on a known-wrong task.
|
|
// B. INTERRUPTIBLE KILL — swarm_worker_run: the kill is absorbed within one
|
|
// step → stops at ~3, status=killed, ~9 steps of waste AVOIDED.
|
|
// C. INTERRUPTIBLE REDIRECT — mirrors the live incident (build-python-synth →
|
|
// native-fetch-render): the correction is absorbed mid-task; the 3 done
|
|
// steps are kept; the worker re-plans onto the new goal and finishes it.
|
|
|
|
// ── per-step work — one bounded unit (~15ms) ──────────────────────────────────
|
|
fn demo_step(arg: String) -> String {
|
|
let goal: String = json_get(arg, "goal")
|
|
let idx: String = json_get(arg, "idx")
|
|
let step: String = json_get(arg, "step")
|
|
sleep_ms(15)
|
|
return "did[" + goal + "] step#" + idx + " (" + step + ")"
|
|
}
|
|
|
|
// ── BASELINE: the broken, non-interruptible worker (Claude-style) ─────────────
|
|
// Same shape as swarm_worker_run BUT it never polls the token during the loop.
|
|
// It "finishes the workflow" and only notices the signal at the very end — the
|
|
// exact pattern Will called out. Reports how many steps it wasted post-signal.
|
|
fn broken_worker_run(arg: String) -> String {
|
|
let tok: Int = str_to_int(json_get(arg, "tok"))
|
|
let out_ch: Int = str_to_int(json_get(arg, "out"))
|
|
let step_fn: String = json_get(arg, "step_fn")
|
|
let purview: String = json_get_raw(arg, "purview")
|
|
let goal: String = json_get(purview, "goal")
|
|
let steps: String = json_get_raw(purview, "steps")
|
|
let n: Int = json_array_len(steps)
|
|
let idx: Int = 0
|
|
// NO token check inside the loop — this is the bug.
|
|
while idx < n {
|
|
let step: String = json_array_get(steps, idx)
|
|
let step_arg: String = "{\"goal\":\"" + goal + "\",\"idx\":" +
|
|
int_to_str(idx) + ",\"step\":" + step + "}"
|
|
let tid: Int = __thread_create(step_fn, step_arg)
|
|
let result: String = __thread_join(tid)
|
|
__channel_send(out_ch, result)
|
|
let idx = idx + 1
|
|
}
|
|
// Only NOW does it look at the control signal — too late.
|
|
let late: String = token_check(tok)
|
|
if str_eq(late, "") {
|
|
__channel_send(out_ch, "[no signal]")
|
|
} else {
|
|
__channel_send(out_ch, "[TOO LATE: absorbed " + json_get(late, "sig") +
|
|
" only after running ALL " + int_to_str(n) +
|
|
" steps — wasted work]")
|
|
}
|
|
return "{\"status\":\"ran-to-completion\",\"completed\":" + int_to_str(idx) + "}"
|
|
}
|
|
|
|
// ── helpers ───────────────────────────────────────────────────────────────────
|
|
|
|
// drain_count — drain out_ch, print each line, return count of real step outputs
|
|
// (lines beginning with "did").
|
|
fn drain_and_report(out_ch: Int) -> Int {
|
|
let done: Int = 0
|
|
let did: Int = 0
|
|
while done == 0 {
|
|
let m: String = __channel_try_recv(out_ch)
|
|
if str_eq(m, "") {
|
|
let done = 1
|
|
} else {
|
|
println(" | " + m)
|
|
if str_starts_with(m, "did") {
|
|
let did = did + 1
|
|
}
|
|
}
|
|
}
|
|
return did
|
|
}
|
|
|
|
fn twelve_steps() -> String {
|
|
return "[\"s0\",\"s1\",\"s2\",\"s3\",\"s4\",\"s5\",\"s6\",\"s7\",\"s8\",\"s9\",\"s10\",\"s11\"]"
|
|
}
|
|
|
|
fn main() -> Void {
|
|
println("=====================================================================")
|
|
println(" NATIVE INTERRUPTIBILITY — PROOF (canon 1ca4d3e9)")
|
|
println(" plan: 12 bounded steps @ ~15ms; signal sent ~50ms in (≈ after step 3)")
|
|
println("=====================================================================")
|
|
|
|
// ── A. BASELINE — broken, non-interruptible ──
|
|
println("")
|
|
println("[A] BASELINE broken worker (no mid-loop signal check) — Claude-style")
|
|
let tokA: Int = token_new()
|
|
let outA: Int = __channel_new(0)
|
|
let pvA: String = purview_new("A", "build-wrong-thing", twelve_steps())
|
|
let argA: String = "{\"tok\":" + int_to_str(tokA) + ",\"out\":" + int_to_str(outA) +
|
|
",\"step_fn\":\"demo_step\",\"purview\":" + pvA + "}"
|
|
let t0A: Int = time_now()
|
|
let tidA: Int = __thread_create("broken_worker_run", argA)
|
|
sleep_ms(50)
|
|
println(" -> coordinator sends KILL at +" + int_to_str(time_now() - t0A) + "ms (≈step 3)")
|
|
token_kill(tokA)
|
|
let finA: String = __thread_join(tidA)
|
|
let elapA: Int = time_now() - t0A
|
|
let didA: Int = drain_and_report(outA)
|
|
println(" RESULT: executed " + int_to_str(didA) + "/12 steps, wall=" +
|
|
int_to_str(elapA) + "ms, final=" + finA)
|
|
println(" >> ignored the kill, RAN ALL 12 — ~9 steps of KNOWN-WRONG waste")
|
|
|
|
// ── B. INTERRUPTIBLE KILL ──
|
|
println("")
|
|
println("[B] INTERRUPTIBLE swarm_worker_run + token_kill")
|
|
let pvB: String = purview_new("B", "build-wrong-thing", twelve_steps())
|
|
let hB: String = swarm_dispatch("demo_step", pvB)
|
|
let tokB: Int = str_to_int(json_get(hB, "tok"))
|
|
let outB: Int = str_to_int(json_get(hB, "out"))
|
|
let tidB: Int = str_to_int(json_get(hB, "tid"))
|
|
let t0B: Int = time_now()
|
|
sleep_ms(50)
|
|
println(" -> coordinator sends KILL at +" + int_to_str(time_now() - t0B) + "ms (≈step 3)")
|
|
token_kill(tokB)
|
|
let finB: String = __thread_join(tidB)
|
|
let elapB: Int = time_now() - t0B
|
|
let didB: Int = drain_and_report(outB)
|
|
println(" RESULT: executed " + int_to_str(didB) + "/12 steps, wall=" +
|
|
int_to_str(elapB) + "ms, final=" + finB)
|
|
println(" >> STOPPED within one step of the signal — no wasted continuation")
|
|
|
|
// ── C. INTERRUPTIBLE REDIRECT (the live incident) ──
|
|
println("")
|
|
println("[C] INTERRUPTIBLE redirect mid-task: build-python-synth -> native-fetch-render")
|
|
let pvC: String = purview_new("C", "build-python-synth-renderer", twelve_steps())
|
|
let hC: String = swarm_dispatch("demo_step", pvC)
|
|
let tokC: Int = str_to_int(json_get(hC, "tok"))
|
|
let outC: Int = str_to_int(json_get(hC, "out"))
|
|
let tidC: Int = str_to_int(json_get(hC, "tid"))
|
|
let t0C: Int = time_now()
|
|
sleep_ms(50)
|
|
println(" -> coordinator REDIRECTS at +" + int_to_str(time_now() - t0C) + "ms (≈step 3)")
|
|
token_redirect(tokC, "native-fetch-render", "[\"fetch\",\"realize\",\"cohere\"]")
|
|
let finC: String = __thread_join(tidC)
|
|
let elapC: Int = time_now() - t0C
|
|
let didC: Int = drain_and_report(outC)
|
|
println(" RESULT: executed " + int_to_str(didC) + " steps total, wall=" +
|
|
int_to_str(elapC) + "ms, final=" + finC)
|
|
println(" >> absorbed the correction mid-task: kept early progress,")
|
|
println(" re-planned onto native-fetch-render, finished the RIGHT plan")
|
|
|
|
// ── D. INTERRUPTIBLE PAUSE -> RESUME (hold state, then continue) ──
|
|
println("")
|
|
println("[D] INTERRUPTIBLE pause mid-task, hold state, then resume to finish")
|
|
let pvD: String = purview_new("D", "long-render", twelve_steps())
|
|
let hD: String = swarm_dispatch("demo_step", pvD)
|
|
let tokD: Int = str_to_int(json_get(hD, "tok"))
|
|
let outD: Int = str_to_int(json_get(hD, "out"))
|
|
let tidD: Int = str_to_int(json_get(hD, "tid"))
|
|
let t0D: Int = time_now()
|
|
sleep_ms(50)
|
|
println(" -> coordinator PAUSES at +" + int_to_str(time_now() - t0D) + "ms (≈step 3)")
|
|
token_pause(tokD)
|
|
sleep_ms(60)
|
|
println(" -> worker held idle for ~60ms; coordinator RESUMES at +" +
|
|
int_to_str(time_now() - t0D) + "ms")
|
|
token_resume(tokD)
|
|
let finD: String = __thread_join(tidD)
|
|
let didD: Int = drain_and_report(outD)
|
|
println(" RESULT: executed " + int_to_str(didD) + "/12 steps, final=" + finD)
|
|
println(" >> paused on the spot, held its plan, resumed and finished it")
|
|
|
|
println("")
|
|
println("=====================================================================")
|
|
println(" A ran all 12 wrong steps. B stopped at ~3. C re-planned at ~3.")
|
|
println(" Same plan, same timing, same signal — only the interruptible worker")
|
|
println(" stops the instant it's told, like a human. QED.")
|
|
println("=====================================================================")
|
|
}
|