[DEV] autosetup: preprocessing watchdog — cancel cloud jobs stuck in prover preprocessing - #138
Merged
Conversation
Add a preprocessing watchdog to CloudProverRunner's wait loop. The prover's treeview carries an empty rules list for as long as the run is in preprocessing (scene construction, storage/pointer analyses, CVL typechecking); rules appear only once rule checking begins. A run whose preprocessing blows up therefore sits in RUNNING with no rules until the prover's global timeout, and autosetup burned its whole 150-minute per-job budget polling it. The watchdog piggy-backs on the existing 10s status poll: queue time is free, the clock starts on the first RUNNING observation, and after a grace period it probes the treeview at a bounded cadence. A non-empty rules list makes it dormant; probe transport errors self-disable it (restoring the old behavior); exceeding the budget cancels the job and classifies the result as a new distinct JobStatus.PREPROCESSING_TIMEOUT so that: - conf workarounds never retry an identical doomed job (on_job_problem guard) and the submission cache is dropped so a deliberate future run submits fresh, - sanity_summary.md shows a dedicated row instead of crashing on the missing job report of a cancelled job. Env knobs (0 budget disables): AUTOSETUP_PREPROCESSING_BUDGET_SECONDS (default 1800), AUTOSETUP_PREPROCESSING_GRACE_SECONDS (300), AUTOSETUP_PREPROCESSING_PROBE_SECONDS (90). Verified live against a production job stuck in preprocessing: cancelled and classified ~5.5 minutes after the budget window opened, with the job showing CANCELED on the cloud. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…y answered probe The probe interval already expresses "don't probe a job that just started running": seeding the last-probe timestamp when the clock starts puts the first probe one interval in, so the separate grace period bought nothing that a second time knob had to exist for. It also removes a misconfiguration trap, since grace and budget were tunable independently with no ordering check between them. _consecutive_probe_errors now resets after any probe the endpoint answers, not only after a JobNotFoundError. An endpoint that answers is not a broken endpoint, and the counter gates a permanent self-disable.
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
1 participant
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.
Mirror of #84 onto the
devbleeding-edge branch.Source branch:
shelly/preprocessing-watchdog. This branch is that head merged forward withdev; #84 itself is untouched and still targetsmaster.Per the
devbranch policy this merges without review oncepyrightandpytestare green.