Stop blaming the guest id when two spine workers race - #231
Merged
Conversation
A lost race and a guest mismatch produced the same message, and the message
described the wrong one. From the v0.20.0 cutover:
extend-spine failed for block 2:
Build a host that matches the proof's guest (reproduce/Dockerfile), then retry.
Underlying verifier error: claim digest does not match the expected digest c08d5e0f…
There was no guest mismatch. Both workers ran the same binary, both had
asserted `binary and board agree` at startup, and the very next attempt
succeeded — which a genuine mismatch cannot do, because it is deterministic.
The real cause is the shape of the loop: fetch the head, wait on the GPU lock,
then fold. Another worker advances the spine inside that window, so the fold is
computed against a head that no longer exists and its claim digest cannot
match.
The caller is the only place that can tell the two apart, because only it knows
which head the fold was computed against. On failure it now re-reads
`/api/spine` and compares:
* head moved -> "the spine advanced under us … refolding from the new head",
at info level, and the loop continues. Not an error: the
other worker did the work we were about to do.
* head unchanged -> the existing advice, which is now actually the likely cause.
Also states the operator half in `run-workers.sh`, where the trap is set.
`MODE=spine` says "only ever needs ONE" — that is **fleet-wide, not per box**,
and `MODE=mixed` allocates one spine worker per box, so `mixed` on N boxes
gives N spine workers racing one spine. The header now says so, and says to run
`mixed` on one box and `prove` on the rest.
⚠ Only the message and the recovery change. A seam failure with an unmoved head
still exits loudly, because that one really is information.
Verified: `python3 -m ast` parses, `hazync --help` runs, `bash -n` on
run-workers.sh, and all eight repo check scripts REAL_EXIT=0.
Claude-Session: https://claude.ai/code/session_01BGBba1FtGQjp2focJGWtjU
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.
Closes #220.
The two cases looked identical, and the message picked the wrong one
From the v0.20.0 cutover:
There was no guest mismatch. Both workers ran the same binary, both had asserted
binary and board agreeat startup, and the next attempt succeeded — which a real mismatch cannot do, being deterministic.The cause is the shape of the loop: fetch the head → wait on the GPU lock → fold. Another worker advances the spine inside that window, so the fold is computed against a head that no longer exists and the claim digest cannot match.
The fix goes in the caller, because only it knows
The host sees a claim-digest mismatch and nothing else; it cannot know which head the fold was computed against. The CLI can. On failure it now re-reads
/api/spine:the spine advanced under us ([1..N] -> [1..M]) — refolding from the new head, at info level, and the loop continues. Not an error — the other worker did the work we were about to do.Only the message and the recovery change. A seam failure with an unmoved head still exits loudly, because that one really is information.
The operator half, stated where the trap is set
MODE=spinealready says "only ever needs ONE". That is fleet-wide, not per box — andMODE=mixedallocates one spine worker per box, somixedon N boxes gives N spine workers racing one spine. Nothing said so.run-workers.sh's header now does, and says to runmixedon one box andproveon the rest.Verified:
python3 -m astparses,hazync --helpruns,bash -nclean, all eight repo check scripts REAL_EXIT=0.⚠ Independent of #230 — branched off
main, not stacked on it, so both get their own CI.