From 0687f052a30c3aacdd936b4674c402aa110a7732 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Wed, 11 Nov 2026 18:50:38 -0800 Subject: [PATCH 01/18] feat(formal): TLA+ model of the repo run cell lifecycle; fix two bugs it found formal/repo_batch/RepoBatch.tla models one batch directory of `repo run`: worker threads, resume and --force reruns, crashes between the artifacts and result.json, Ctrl-C, and what `repo report` counts. run.sh checks 13 TLC configs against their expected result (the fixed code passes; the code before the fixes, two mutations, no fairness and four vacuity witnesses each fail as expected). Fixes, each with a test replaying the TLC trace: - run_batch refuses a plan naming one cell twice (a repeated --task or --model, or two --model strings with one slug); with --jobs 2 both runs shared one directory and mixed their files. - load_cells refuses an arm/model whose finished cells ran under two execution ids, left by a --force run that stopped part way; report and compare pooled them in one row. EVALUATOR.md proposes a model-checking grader for agent tasks. Signed-off-by: Nikolay Petrov --- ...11_180000_napetrov_repo-batch-lifecycle.md | 16 ++ dokimi/docs/repo-evaluation-contract.md | 8 +- dokimi/dokimi/repos/report.py | 14 + dokimi/dokimi/repos/runner.py | 11 + dokimi/formal/repo_batch/.gitignore | 2 + dokimi/formal/repo_batch/EVALUATOR.md | 46 ++++ dokimi/formal/repo_batch/README.md | 136 ++++++++++ dokimi/formal/repo_batch/RepoBatch.tla | 243 ++++++++++++++++++ .../repo_batch/cfg/code_main_dup_plan.cfg | 18 ++ .../cfg/code_main_dup_plan_files.cfg | 18 ++ .../repo_batch/cfg/code_main_force_crash.cfg | 18 ++ dokimi/formal/repo_batch/cfg/fixed.cfg | 19 ++ .../repo_batch/cfg/mut_accept_stale.cfg | 18 ++ .../repo_batch/cfg/mut_count_every_commit.cfg | 18 ++ .../repo_batch/cfg/mut_no_cancel_guard.cfg | 18 ++ dokimi/formal/repo_batch/cfg/mut_no_lock.cfg | 18 ++ dokimi/formal/repo_batch/cfg/no_fairness.cfg | 18 ++ .../repo_batch/cfg/witness_NoCancel.cfg | 18 ++ .../cfg/witness_NoCrashAfterArtifacts.cfg | 18 ++ .../cfg/witness_NoResumeAfterCrash.cfg | 18 ++ .../repo_batch/cfg/witness_NoRetryHappens.cfg | 18 ++ dokimi/formal/repo_batch/run.sh | 43 ++++ dokimi/tests/test_repo_batch_lifecycle.py | 148 +++++++++++ 23 files changed, 901 insertions(+), 1 deletion(-) create mode 100644 dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md create mode 100644 dokimi/formal/repo_batch/.gitignore create mode 100644 dokimi/formal/repo_batch/EVALUATOR.md create mode 100644 dokimi/formal/repo_batch/README.md create mode 100644 dokimi/formal/repo_batch/RepoBatch.tla create mode 100644 dokimi/formal/repo_batch/cfg/code_main_dup_plan.cfg create mode 100644 dokimi/formal/repo_batch/cfg/code_main_dup_plan_files.cfg create mode 100644 dokimi/formal/repo_batch/cfg/code_main_force_crash.cfg create mode 100644 dokimi/formal/repo_batch/cfg/fixed.cfg create mode 100644 dokimi/formal/repo_batch/cfg/mut_accept_stale.cfg create mode 100644 dokimi/formal/repo_batch/cfg/mut_count_every_commit.cfg create mode 100644 dokimi/formal/repo_batch/cfg/mut_no_cancel_guard.cfg create mode 100644 dokimi/formal/repo_batch/cfg/mut_no_lock.cfg create mode 100644 dokimi/formal/repo_batch/cfg/no_fairness.cfg create mode 100644 dokimi/formal/repo_batch/cfg/witness_NoCancel.cfg create mode 100644 dokimi/formal/repo_batch/cfg/witness_NoCrashAfterArtifacts.cfg create mode 100644 dokimi/formal/repo_batch/cfg/witness_NoResumeAfterCrash.cfg create mode 100644 dokimi/formal/repo_batch/cfg/witness_NoRetryHappens.cfg create mode 100755 dokimi/formal/repo_batch/run.sh create mode 100644 dokimi/tests/test_repo_batch_lifecycle.py diff --git a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md new file mode 100644 index 000000000..f458221a5 --- /dev/null +++ b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md @@ -0,0 +1,16 @@ +### Fixed + +- **`repo run` refuses a plan that names one cell twice** — a repeated `--task` or `--model`, or two + `--model` strings with one directory name (`a/b` and `a:b`), put two runs in one cell directory; + with `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's + `meta.json` and answer. The run now stops before any agent starts, naming the cell. +- **`repo report` and `repo compare` refuse a batch whose arm and model hold two executions** — a + `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell) left + some cells on the old execution and was pooled with them in one row. The refusal names both ids; + a `--force` run that finishes the batch clears it. + +### Added + +- **`formal/repo_batch`: a TLA+ model of the `repo run` cell lifecycle** — retries, crashes, + resume, `--force`, Ctrl-C and what the report counts, with TLC configs for the code, the fixes + and two mutations; `run.sh` checks each against its expected result. diff --git a/dokimi/docs/repo-evaluation-contract.md b/dokimi/docs/repo-evaluation-contract.md index c152e0938..5c3805f1d 100644 --- a/dokimi/docs/repo-evaluation-contract.md +++ b/dokimi/docs/repo-evaluation-contract.md @@ -2303,7 +2303,13 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric still run; the file is left in place, and removing it or `--force` runs the cell again. The same holds for a finished cell of a task this host cannot run, except that `--force` keeps it: once its file is removed, the cell runs - on a host that meets the task's requirements. A batch stays on the eval tree it + on a host that meets the task's requirements. A `--force` run that stops part + way (Ctrl-C, a crash, a failed cell) can leave finished cells of two `id`s in + one arm and model; `repo report` and `repo compare` refuse such a batch, naming + both `id`s, until a `--force` run finishes it. A plan naming one cell twice (a + repeated `--task` or `--model`, or two `--model` strings with one directory + name, `a/b` and `a:b`) is refused before any agent starts. Ctrl-C lets the + running cells finish and starts no queued one. A batch stays on the eval tree it started with: its revision, or for a working tree the digests of its `eval_dir` and of the image build context. A batch with a task that names a `dokimi:` grader (or a task directory that cannot be read) also stays on the built-in graders' sources. diff --git a/dokimi/dokimi/repos/report.py b/dokimi/dokimi/repos/report.py index e9901dfec..f5b9a8fb7 100644 --- a/dokimi/dokimi/repos/report.py +++ b/dokimi/dokimi/repos/report.py @@ -63,6 +63,7 @@ from dokimi.utils import same_model from .grading import SCORE_BOUND, read_grade_json +from .batch_ledger import recorded_execution from .process_counts import process_line, process_means from .runner import UNSUPPORTED_FILE, slug from .useful import useful_line, useful_summary @@ -193,11 +194,24 @@ def load_cells(batch_dir: Path) -> tuple[list[dict[str, Any]], list[str]]: with reading_cells([str(path)]): rec["score_task"] = bool(rec["score_task"] if "score_task" in rec else rec["grade"]["score_only"]) finished.append(rec) + _refuse_mixed_executions(batch_dir, finished) done = {r["cell"] for r in finished} unsupported = {p.parent.name for p in batch_dir.glob(f"*/{UNSUPPORTED_FILE}")} return finished, sorted((planned | started) - done - unsupported) +def _refuse_mixed_executions(batch_dir: Path, finished: list[dict[str, Any]]) -> None: + """One (arm, model) of a batch ran with one execution: a --force run that stopped part way leaves two.""" + seen: dict[tuple[str, str], set[str]] = defaultdict(set) + for rec in finished: + ran = recorded_execution(rec).get("id") + seen[(rec["arm"], rec["model"])].add(ran if isinstance(ran, str) else "unrecorded") + for (arm, model), ids in sorted(seen.items()): + if len(ids) > 1: + raise CellFileError(f"{batch_dir}: the cells of arm {arm}, model {model} ran with executions " + f"{', '.join(sorted(ids))}; rerun the batch with --force to finish it, or use another --batch") + + def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]: """Cells the runner did not run on a host that missed their task's ``host`` requirements.""" out = [] diff --git a/dokimi/dokimi/repos/runner.py b/dokimi/dokimi/repos/runner.py index a5809f29a..10ad689a8 100644 --- a/dokimi/dokimi/repos/runner.py +++ b/dokimi/dokimi/repos/runner.py @@ -40,6 +40,7 @@ import sys import threading import uuid +from collections import Counter from collections.abc import Iterator from concurrent.futures import ThreadPoolExecutor from dataclasses import dataclass @@ -372,6 +373,7 @@ def run_batch(ctx: EvalContext, tasks: list[Task], arms: list[str], options: lis that cell's error.""" validate_tasks(tasks) cells = [(t, a, o, r) for t in tasks for a in arms for o in options for r in range(1, reps + 1)] + _refuse_shared_cells(cells) check_batch_executions(batch_dir, options, {cell_name(t.id, a, o.model, r) for t, a, o, r in cells} if force else None) host = probe_host(ctx, batch_dir / "_eval") _write_json(batch_dir / "_eval" / "host.json", host) @@ -436,6 +438,15 @@ def one(cell: tuple[Task, str, AgentOptions, int]) -> None: "spent_usd": round(state["spent"], 6)} +def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> None: + """Refuse a plan naming one cell directory twice: with --jobs 2 both would run in it and mix their files.""" + names = Counter(cell_name(t.id, a, o.model, r) for t, a, o, r in cells) + shared = sorted(name for name, n in names.items() if n > 1) + if shared: + raise ValueError(f"cell {shared[0]} is planned {names[shared[0]]} times (a repeated --task or --model, or " + "two --model strings with one name on disk); give each once") + + UNSUPPORTED_FILE = "unsupported.json" KEPT_HINT = ("this host cannot run the task, so --force keeps the file; remove it, and the cell runs on a host " "that meets the task's requirements") diff --git a/dokimi/formal/repo_batch/.gitignore b/dokimi/formal/repo_batch/.gitignore new file mode 100644 index 000000000..0c1bb46b7 --- /dev/null +++ b/dokimi/formal/repo_batch/.gitignore @@ -0,0 +1,2 @@ +out/ +RepoBatch_TTrace_* diff --git a/dokimi/formal/repo_batch/EVALUATOR.md b/dokimi/formal/repo_batch/EVALUATOR.md new file mode 100644 index 000000000..a572d6faa --- /dev/null +++ b/dokimi/formal/repo_batch/EVALUATOR.md @@ -0,0 +1,46 @@ + + +# Proposal: a model-checking grader for agent tasks + +Status: proposal, not implemented. It would be a `dokimi:` grader (like the built-in ones in +`dokimi/repos/`) for tasks whose answer is a change to a system with a fixed formal spec. + +## Shape + +- **Input**: the task's fixed spec (a `.tla` module with the properties, plus one or more `.cfg` + files and their `EXPECT` lines), pinned by the task; and the agent's change — either the model + of the implementation the agent edited, or the code that a task-owned extractor maps to the + model's constants. +- **Output**, one of four, in `grade.json`: + - `pass` — TLC finished every config and each matched its `EXPECT`; + - `counterexample` — a property was violated: the property name and the trace; + - `timeout` — the state space was not exhausted within the task's limit; + - `tool_error` — TLC or the parser failed (syntax error, unknown operator, Java missing). + +## Rules + +1. **The agent cannot weaken the spec.** The grader reads the spec, configs and `EXPECT` lines from + the task's eval tree (pinned in the batch ledger like other grader sources), never from the + agent's workspace. A change to those paths in the workspace is reported and ignored. +2. **The agent cannot swap the checker.** `tla2tools.jar` and the JRE are pinned by SHA-256 in the + grader and mounted read-only; TLC runs outside the agent's container. The command line + (`-workers`, `-deadlock`, `-config`) is the grader's, not the task's or the agent's. +3. **A timeout is not a proof.** `timeout` and `tool_error` score as not passed and are reported + apart from `counterexample`, so a slow model is not read as a correct one, and a broken tool is + not read as an agent failure. +4. **Vacuity.** Each task ships witness configs that must be violated; if a witness passes after the + agent's change (the change made the scenario unreachable), the grade is `counterexample` with + the witness named. +5. **A pass is not a quality score.** It means: in this bounded instance, under the stated fairness + assumptions, the listed properties hold. The report shows it as its own measure next to tests and + any judge, never folded into one number, and names the instance bounds. + +## Limits + +- Bounded: only the constants in the configs are checked. +- The model-to-code link is as good as the extractor or the human mapping (the README's action → + code table); a correct model of wrong code passes. +- Liveness holds only under the fairness the spec assumes. diff --git a/dokimi/formal/repo_batch/README.md b/dokimi/formal/repo_batch/README.md new file mode 100644 index 000000000..a4f224c25 --- /dev/null +++ b/dokimi/formal/repo_batch/README.md @@ -0,0 +1,136 @@ + + +# TLA+ model of the `repo run` cell lifecycle + +`RepoBatch.tla` models one batch directory of `dokimi repo run` (`dokimi/repos/runner.py`, +`dokimi/repos/batch_ledger.py`) and what `repo report` / `repo compare` count from it +(`dokimi/repos/report.py`). It asks one question: can retries, crashes, resumes, `--force` +reruns, worker threads, Ctrl-C and late results change which cells the report counts, or how +often? TLC answers it for a small, explicit instance. It says nothing about whether a grader, +an LLM judge or a task measures the right thing. + +## Run + +```sh +# pinned tools: tla2tools.jar v1.8.0 (sha256 e1f11b75c4b5bc4478ba0ac5cb6ae28e40a01b0016bc33e0aa97da22dfdbcd7f), +# any Java 11+ (checked with Temurin JRE 21.0.5+11) +TLA2TOOLS_JAR=/path/to/tla2tools.jar JAVA=/path/to/java ./run.sh # every cfg/*.cfg +TLA2TOOLS_JAR=... ./run.sh cfg/mut_accept_stale.cfg # one config +``` + +Each config carries an `\* EXPECT:` line (`pass` or `violation `); `run.sh` writes +`out/summary.tsv` and one log per config (with TLC's counterexample trace), and exits 1 when a +result differs from its expectation. `out/` is not committed. + +## What exists in the code, and what does not + +| Mechanism | In the code | In the model | +|---|---|---| +| Run = batch dir `--batch`; cell = `cell_name(task, arm, model, rep)` dir | yes | `Tasks` (one arm, model, rep) | +| Repetition | `--reps N`: cells `__r1..__rN`, independent samples | not needed: one rep per cell | +| Retry of a cell | only a later `repo run` on the batch (resume or `--force`), same cell name, replaces the dir | `Take` by a later invocation | +| In-process retry, redelivery, reassignment, leases, heartbeats | **none** | not modelled (would be an imagined architecture) | +| Workers | `ThreadPoolExecutor(jobs)` + `pool.map` | `Workers` threads | +| Timeout | agent killed, the cell is graded (an outcome, not a retry) | inside `Work` | +| Crash | process dies; no `result.json` → cell is *missing*, the next run fills it | `Crash` | +| Late result of an old attempt | impossible in-process: threads die with the process | `LateCommit`, mutation only | +| Cancel | Ctrl-C: `KeyboardInterrupt`; `pool.map` cancels queued futures, running cells finish | `Cancel`, `CancelGuard` | +| Exclusion of concurrent runs on one batch | `batch_lock` (flock on `_eval/lock`) | `Locked` | +| Execution pinning | `execution.id` in `meta.json`/`result.json`; `check_batch_executions` before any cell | `Configs`, `StartCheck` | +| Commit | `_write_json(rd / "result.json")`: mkstemp + `os.replace` (atomic) | `Commit` | +| Aggregation | `load_cells`: one `result.json` per dir; missing = planned − done | `Done`, `Counted`, `Missing` | +| Dataset/task, skill, evaluator pins | eval tree revision or digests, `_eval/skills.json`, grader sources in the batch ledger | folded into `Configs` | +| Caps (timeout, max turns, budget) pinned | **no**: recorded per cell in `agent.caps`, not in `execution.id` | not modelled (open question 3) | + +## Actions → code + +| Action | Code | +|---|---| +| `Start(g, f, p)` | `cmd_repo_run` → `batch_lock`, `run_batch` → `_refuse_shared_cells`, `check_batch_executions` (`--force` skips its own plan) | +| `Take(w, i)` | `pool.map` → `one` → `run_cell`: `reused_result` keeps a done cell unless `--force`; else `_rmtree` + mkdir of the cell dir | +| `Work(w)` | agent run, then `meta.json`, `events.jsonl`, `answer.txt`, `task.json`, grade, written by path | +| `Commit(w)` | `_write_json(rd / "result.json", record)` | +| `Crash(i)` | SIGKILL / OOM / reboot: flock released, threads gone | +| `Cancel(i)`, `Finish(i)` | Ctrl-C; pool join and the exit code of `cmd_repo_run` (1 on errors, interrupt, budget stop, probe failure) | +| `LateCommit(a)` | mutation `AcceptStale` only | + +## Properties + +| | Property (TLA+) | Meaning | Where the code holds it | +|---|---|---|---| +| P1 | `RetryNotRepetition` | a cell is one sample at most, however often it ran | `load_cells` reads one `result.json` per dir; the retry reuses the cell name | +| P2 | `OnlyValidAttempts` | a counted result is a finished attempt of that cell, beside that attempt's files only | `run_cell` rmtree's before an attempt; `result.json` written last; `_refuse_shared_cells` | +| P3 | `NoStaleOverwrite` | no `result.json` from an attempt that no longer owns the dir | `batch_lock`; threads die with the process; `_refuse_shared_cells` | +| P4 | `OneConfig` | the cells of one report row ran under one `execution.id` | `check_batch_executions`; `_refuse_mixed_executions` in `load_cells` | +| P5 | `PartialNotComplete` | exit 0 only with every planned cell done; the rest are *missing* | exit logic of `cmd_repo_run`; `record_plan` + `load_cells` | +| P6 | `CancelContract` | no attempt starts after Ctrl-C; the run does not exit 0 | `pool.map` cancels pending futures when the main thread raises | +| P7 | `InvocationEnds` (liveness) | every invocation ends | under `Fairness` only | + +Assumptions (stated in the model, not proven): + +- **Fairness**: weak fairness on `Work`, `Commit`, `Take`, `Finish` — a live thread keeps + working, an agent run ends (its timeout), the pool joins. Nothing forces a resume after a crash, + so "every planned cell eventually has a result" is *not* claimed: it needs a human or a + scheduler to rerun the batch. +- `os.replace` is atomic and a dead process writes nothing; a container that outlives the + process writes into the deleted dir's inode (`_rmtree` removed it), not into the new one. +- The batch dir is on a local file system where `flock` works. +- Not modelled: the batch budget (`--max-batch-usd`), unsupported tasks, multiple arms/models, + report reads racing a writer (they read whole files written atomically). + +Vacuity: `witness_*.cfg` each assert that a scenario never happens (no retry, no crash after the +artifacts, no Ctrl-C, no resume after a crash) and must be violated; they show `fixed.cfg` passes +with those scenarios reachable. + +## Results + +Instance: `Tasks = {t1, t2}`, `Workers = {w1, w2}`, `Configs = {cA, cB}`, `MaxInv = 3`; +tla2tools v1.8.0 (TLC2 Version 2026.11.06.222357, rev d8fb231), 4 TLC workers, Temurin 21.0.5+11, +224-core shared host; seconds are wall time. + +| cfg | expect | got | ok | generated | distinct | depth | seconds | +|---|---|---|---|---|---|---|---| +| code_main_dup_plan | violation NoStaleOverwrite | violation NoStaleOverwrite | yes | 3746 | 3474 | 7 | 0.8 | +| code_main_dup_plan_files | violation OnlyValidAttempts | violation OnlyValidAttempts | yes | 3673 | 3407 | 7 | 0.8 | +| code_main_force_crash | violation OneConfig | violation OneConfig | yes | 344636 | 266056 | 11 | 2.4 | +| fixed | pass | pass | yes | 10304813 | 5750785 | 28 | 431.9 | +| mut_accept_stale | violation NoStaleOverwrite | violation NoStaleOverwrite | yes | 4686 | 4172 | 8 | 0.9 | +| mut_count_every_commit | violation RetryNotRepetition | violation RetryNotRepetition | yes | 49055 | 42396 | 10 | 1.2 | +| mut_no_cancel_guard | violation CancelContract | violation CancelContract | yes | 124 | 119 | 5 | 0.7 | +| mut_no_lock | violation NoStaleOverwrite | violation NoStaleOverwrite | yes | 53078 | 27928 | 7 | 1.4 | +| no_fairness | violation InvocationEnds | violation InvocationEnds | yes | 217120 | 173024 | 11 | 4.0 | +| witness_NoCancel | violation NoCancel | violation NoCancel | yes | 25 | 25 | 3 | 0.7 | +| witness_NoCrashAfterArtifacts | violation NoCrashAfterArtifacts | violation NoCrashAfterArtifacts | yes | 260 | 234 | 5 | 0.7 | +| witness_NoResumeAfterCrash | violation NoResumeAfterCrash | violation NoResumeAfterCrash | yes | 10889 | 9747 | 8 | 1.0 | +| witness_NoRetryHappens | violation NoRetryHappens | violation NoRetryHappens | yes | 55492 | 47963 | 10 | 1.2 | + +- `code_main_*` model the code as it was before this change; their traces were replayed as tests in + `tests/test_repo_batch_lifecycle.py` (red before, green after). +- `mut_*` are mutations: TLC must find each. + +## Findings + +1. **One cell planned twice** (`code_main_dup_plan*`): `--task a --task a`, `--model m --model m`, + or `--model org/m --model org:m` (one `slug`) put two runs in one dir. With `--jobs 2` the second + rmtree'd the first's dir while its agent ran, and `result.json` landed beside the other + attempt's `meta.json`/answer. Fixed: `_refuse_shared_cells`. +2. **A part-way `--force` with another execution pools two executions** (`code_main_force_crash`, + found by TLC on its first run of `fixed`): `--force` replaced r1, then the run stopped; r2 kept + the old execution and `repo report` pooled both in one row. Fixed: `_refuse_mixed_executions`. +3. **Ctrl-C** (`mut_no_cancel_guard`): a probe with `_thread.interrupt_main()` started queued cells, + but a real SIGINT wakes the main thread and `pool.map` cancels them. Not a bug; the test pins it. + +Open questions (left as they are): + +1. `--force` with `--max-batch-usd`: the budget stop skips only cells that are not done, so a forced + rerun still reruns done cells after the budget is spent. +2. A grader with write access to the run dir could leave a `result.json` when the host fails to + write its own (`CellCrash`); a resume would reuse it. +3. Caps (timeout, max turns, per-cell budget) are not in `execution.id`, so one row can mix caps. + +## A formal-verification evaluator for agent tasks (proposal) + +See [`EVALUATOR.md`](EVALUATOR.md). diff --git a/dokimi/formal/repo_batch/RepoBatch.tla b/dokimi/formal/repo_batch/RepoBatch.tla new file mode 100644 index 000000000..0984967a8 --- /dev/null +++ b/dokimi/formal/repo_batch/RepoBatch.tla @@ -0,0 +1,243 @@ +------------------------------ MODULE RepoBatch ------------------------------ +(***************************************************************************) +(* Copyright (C) 2026 Intel Corporation *) +(* SPDX-License-Identifier: Apache-2.0 *) +(* *) +(* The cell lifecycle of `repo run` (dokimi/repos/runner.py, *) +(* dokimi/repos/batch_ledger.py) and what `repo report` *) +(* (dokimi/repos/report.py) aggregates from a batch directory. *) +(* *) +(* One batch directory, two tasks (one arm, one model, one rep: a cell per *) +(* task), two worker threads per invocation, up to MaxInv invocations of *) +(* `repo run` on the batch (a resume, a --force rerun, a crashed one). *) +(* An "attempt" is one run_cell call that prepared the cell's directory; *) +(* retries of a cell are later attempts on the same cell name, never a *) +(* new rep. See README.md for the mapping of every action to the code. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + Tasks, \* cell names (task ids; arm/model/rep fixed) + Workers, \* ThreadPoolExecutor(jobs) threads + Configs, \* execution ids (batch_ledger.execution_id) + MaxInv, \* bound on invocations of `repo run` on the batch + \* Switches for the code as it is, the fix, and the mutations: + Locked, \* batch_lock(): flock on _eval/lock held per invocation + StartCheck, \* check_batch_executions() before any cell runs + UniquePlan, \* the plan never names one cell twice (the fix, #1) + CancelGuard, \* Ctrl-C starts no queued cell (pool.map cancels them) + ReportCheck, \* the report refuses a row of two execution ids (the fix, #2) + AcceptStale, \* MUTATION: a dead attempt's result can still be committed + CountLog \* MUTATION: the report counts every commit, not one per cell + +ASSUME Locked \in BOOLEAN /\ StartCheck \in BOOLEAN /\ UniquePlan \in BOOLEAN +ASSUME CancelGuard \in BOOLEAN /\ ReportCheck \in BOOLEAN /\ AcceptStale \in BOOLEAN /\ CountLog \in BOOLEAN +ASSUME MaxInv \in Nat \ {0} + +None == 0 +Range(s) == {s[k] : k \in DOMAIN s} + +\* The plans run_batch builds: every cell, a --task subset, and, until the fix, +\* a plan naming one cell twice (`--task a --task a`, `--model m --model m`, or +\* two model strings with one slug, `a/b` and `a:b`). +Plans == + LET t1 == CHOOSE t \in Tasks : TRUE + all == CHOOSE s \in [1..Cardinality(Tasks) -> Tasks] : Range(s) = Tasks + IN {all, <>} \cup (IF UniquePlan THEN {} ELSE {<>}) + +VARIABLES + inv, \* invocations started so far + live, \* invocations whose process is alive + cfg, force, plan, queue, cancelled, errs, exit, \* per invocation + wk, \* per worker: [st, inv, att] + atts, \* attempt id -> [inv, cell, cfg] + owner, \* cell -> attempt that last prepared (rmtree+mkdir) its dir + result, \* cell -> attempt whose record result.json holds (None: no file) + art, \* cell -> attempts whose meta/answer/grade files the dir holds + commits, \* history: every write of a result.json, <> + ghosts, \* history: attempts of a crashed process past their artifacts + stale, \* history: a result.json was written by a non-owner attempt + lateStart, \* history: an attempt started after its invocation was cancelled + badOk \* history: an invocation exited 0 with a planned cell unfinished + +vars == <> + +Inv == 1..MaxInv +Idle == [st |-> "idle", inv |-> 0, att |-> 0] + +Init == + /\ inv = 0 /\ live = {} + /\ cfg = [i \in Inv |-> CHOOSE g \in Configs : TRUE] + /\ force = [i \in Inv |-> FALSE] + /\ plan = [i \in Inv |-> <<>>] /\ queue = [i \in Inv |-> <<>>] + /\ cancelled = [i \in Inv |-> FALSE] /\ errs = [i \in Inv |-> FALSE] + /\ exit = [i \in Inv |-> "none"] + /\ wk = [w \in Workers |-> Idle] + /\ atts = <<>> + /\ owner = [c \in Tasks |-> None] /\ result = [c \in Tasks |-> None] + /\ art = [c \in Tasks |-> {}] + /\ commits = <<>> /\ ghosts = {} + /\ stale = FALSE /\ lateStart = FALSE /\ badOk = FALSE + +CfgOf(a) == atts[a].cfg + +\* cmd_repo_run: batch_lock, then run_batch's check_batch_executions over the +\* finished cells (a --force run skips the cells of its own plan). +Start(g, f, p) == + /\ inv < MaxInv + /\ Locked => live = {} + /\ StartCheck => + \A c \in Tasks : result[c] # None => + (f /\ c \in Range(p)) \/ CfgOf(result[c]) = g + /\ LET i == inv + 1 IN + /\ inv' = i /\ live' = live \cup {i} + /\ cfg' = [cfg EXCEPT ![i] = g] /\ force' = [force EXCEPT ![i] = f] + /\ plan' = [plan EXCEPT ![i] = p] /\ queue' = [queue EXCEPT ![i] = p] + /\ UNCHANGED <> + +\* pool.map hands the next planned cell to an idle thread; one() calls run_cell. +\* reused_result: a finished cell is kept unless --force (another execution: error). +\* Otherwise run_cell rmtree's and recreates the dir, which drops result.json. +Take(w, i) == + /\ i \in live /\ wk[w].st = "idle" /\ queue[i] # <<>> + /\ CancelGuard => ~cancelled[i] + /\ LET c == Head(queue[i]) IN + /\ queue' = [queue EXCEPT ![i] = Tail(queue[i])] + /\ IF result[c] # None /\ ~force[i] + THEN /\ errs' = [errs EXCEPT ![i] = errs[i] \/ CfgOf(result[c]) # cfg[i]] + /\ UNCHANGED <> + ELSE LET a == Len(atts) + 1 IN + /\ atts' = Append(atts, [inv |-> i, cell |-> c, cfg |-> cfg[i]]) + /\ owner' = [owner EXCEPT ![c] = a] + /\ result' = [result EXCEPT ![c] = None] + /\ art' = [art EXCEPT ![c] = {}] + /\ wk' = [wk EXCEPT ![w] = [st |-> "run", inv |-> i, att |-> a]] + /\ lateStart' = (lateStart \/ cancelled[i]) + /\ UNCHANGED errs + /\ UNCHANGED <> + +\* The agent runs (it may time out: that is an outcome, the cell is graded), +\* then meta.json, events.jsonl, answer.txt, task.json and the grade are written +\* by path into the cell's directory, whatever attempt owns it now. +Work(w) == + /\ wk[w].st = "run" + /\ LET c == atts[wk[w].att].cell IN + art' = [art EXCEPT ![c] = art[c] \cup {wk[w].att}] + /\ wk' = [wk EXCEPT ![w].st = "art"] + /\ UNCHANGED <> + +\* _write_json(rd / "result.json"): mkstemp + os.replace into the path. +WriteResult(c, a) == + /\ result' = [result EXCEPT ![c] = a] + /\ commits' = Append(commits, <>) + /\ stale' = (stale \/ owner[c] # a) + +Commit(w) == + /\ wk[w].st = "art" + /\ WriteResult(atts[wk[w].att].cell, wk[w].att) + /\ wk' = [wk EXCEPT ![w] = Idle] + /\ UNCHANGED <> + +\* The process dies (SIGKILL, OOM, host reboot): its threads die with it, the +\* flock is released, a cell past its artifacts has no result.json (missing). +Crash(i) == + /\ i \in live + /\ live' = live \ {i} + /\ exit' = [exit EXCEPT ![i] = "fail"] + /\ ghosts' = ghosts \cup {wk[w].att : w \in {v \in Workers : wk[v].inv = i /\ wk[v].st = "art"}} + /\ wk' = [w \in Workers |-> IF wk[w].inv = i THEN Idle ELSE wk[w]] + /\ UNCHANGED <> + +\* MUTATION AcceptStale: the late result of a dead attempt is still written. +LateCommit(a) == + /\ AcceptStale /\ a \in ghosts + /\ WriteResult(atts[a].cell, a) + /\ ghosts' = ghosts \ {a} + /\ UNCHANGED <> + +\* Ctrl-C: KeyboardInterrupt in the main thread, inside pool.map. +Cancel(i) == + /\ i \in live /\ ~cancelled[i] + /\ cancelled' = [cancelled EXCEPT ![i] = TRUE] + /\ UNCHANGED <> + +\* The pool joins its threads; cmd_repo_run exits 0 only without errors and +\* without an interrupt. With CancelGuard the queued cells are dropped. +Finish(i) == + /\ i \in live + /\ queue[i] = <<>> \/ (CancelGuard /\ cancelled[i]) + /\ \A w \in Workers : wk[w].inv # i + /\ live' = live \ {i} + /\ LET ok == ~cancelled[i] /\ ~errs[i] IN + /\ exit' = [exit EXCEPT ![i] = IF ok THEN "ok" ELSE "fail"] + /\ badOk' = (badOk \/ (ok /\ \E c \in Range(plan[i]) : result[c] = None)) + /\ UNCHANGED <> + +Next == + \/ \E g \in Configs, f \in BOOLEAN, p \in Plans : Start(g, f, p) + \/ \E w \in Workers, i \in Inv : Take(w, i) + \/ \E w \in Workers : Work(w) \/ Commit(w) + \/ \E i \in Inv : Crash(i) \/ Cancel(i) \/ Finish(i) + \/ \E a \in ghosts : LateCommit(a) + +\* Progress: a live thread keeps working and the pool joins. Nothing forces a +\* new invocation, a crash or a Ctrl-C. +Fairness == + /\ \A w \in Workers : WF_vars(Work(w)) /\ WF_vars(Commit(w)) + /\ \A w \in Workers, i \in Inv : WF_vars(Take(w, i)) + /\ \A i \in Inv : WF_vars(Finish(i)) + +Spec == Init /\ [][Next]_vars +FairSpec == Spec /\ Fairness + +----------------------------------------------------------------------------- +(* What `repo report` reads: one result.json per cell directory. *) +Done == {c \in Tasks : result[c] # None} +Samples(c) == + IF CountLog THEN Cardinality({k \in DOMAIN commits : commits[k][1] = c}) + ELSE IF c \in Done THEN 1 ELSE 0 +Planned == UNION {Range(plan[i]) : i \in 1..inv} +Missing == Planned \ Done +Mixed == \E c, d \in Done : CfgOf(result[c]) # CfgOf(result[d]) +\* The cells a report counts: with ReportCheck a mixed row is refused (exit 1). +Counted == IF ReportCheck /\ Mixed THEN {} ELSE Done + +TypeOK == + /\ inv \in 0..MaxInv /\ live \subseteq Inv + /\ \A w \in Workers : wk[w].st \in {"idle", "run", "art"} + +\* P1 A retry of a cell is not another sample: a cell is one sample at most. +RetryNotRepetition == \A c \in Tasks : Samples(c) <= 1 +\* P2 A counted result is a finished attempt of that very cell, and the files +\* beside it (meta, answer, grade) are that attempt's and no other's. +OnlyValidAttempts == + \A c \in Done : atts[result[c]].cell = c /\ art[c] = {result[c]} +\* P3 No result.json is written by an attempt that no longer owns the dir. +NoStaleOverwrite == ~stale +\* P4 The results a report counts in one row ran under one execution id. +OneConfig == \A c, d \in Counted : CfgOf(result[c]) = CfgOf(result[d]) +\* P5 `repo run` exits 0 only when every planned cell has a result; the +\* report's missing list is exactly the planned cells without one. +PartialNotComplete == ~badOk +\* P6 Ctrl-C: no attempt starts after it, and the run does not exit 0. +CancelContract == + /\ ~lateStart + /\ \A i \in Inv : cancelled[i] => exit[i] # "ok" +\* P7 (liveness, under Fairness) every invocation ends. +InvocationEnds == \A i \in Inv : (i \in live) ~> (i \notin live) + +\* Vacuity witnesses: each must be VIOLATED, showing the scenario is reachable. +NoRetryHappens == \A c \in Tasks : Cardinality({k \in DOMAIN commits : commits[k][1] = c}) <= 1 +NoCrashAfterArtifacts == ghosts = {} +NoCancel == \A i \in Inv : ~cancelled[i] +NoResumeAfterCrash == ~(\E i, j \in 1..inv : i < j /\ exit[i] = "fail" /\ exit[j] = "ok") +============================================================================= diff --git a/dokimi/formal/repo_batch/cfg/code_main_dup_plan.cfg b/dokimi/formal/repo_batch/cfg/code_main_dup_plan.cfg new file mode 100644 index 000000000..66a96876a --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/code_main_dup_plan.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoStaleOverwrite +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = FALSE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoStaleOverwrite diff --git a/dokimi/formal/repo_batch/cfg/code_main_dup_plan_files.cfg b/dokimi/formal/repo_batch/cfg/code_main_dup_plan_files.cfg new file mode 100644 index 000000000..53c5388a3 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/code_main_dup_plan_files.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation OnlyValidAttempts +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = FALSE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT OnlyValidAttempts diff --git a/dokimi/formal/repo_batch/cfg/code_main_force_crash.cfg b/dokimi/formal/repo_batch/cfg/code_main_force_crash.cfg new file mode 100644 index 000000000..69de6217c --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/code_main_force_crash.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation OneConfig +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = FALSE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT OneConfig diff --git a/dokimi/formal/repo_batch/cfg/fixed.cfg b/dokimi/formal/repo_batch/cfg/fixed.cfg new file mode 100644 index 000000000..b94f9d924 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/fixed.cfg @@ -0,0 +1,19 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: pass +SPECIFICATION FairSpec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANTS TypeOK RetryNotRepetition OnlyValidAttempts NoStaleOverwrite OneConfig PartialNotComplete CancelContract +PROPERTY InvocationEnds diff --git a/dokimi/formal/repo_batch/cfg/mut_accept_stale.cfg b/dokimi/formal/repo_batch/cfg/mut_accept_stale.cfg new file mode 100644 index 000000000..9ee1c03f2 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/mut_accept_stale.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoStaleOverwrite +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = TRUE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoStaleOverwrite diff --git a/dokimi/formal/repo_batch/cfg/mut_count_every_commit.cfg b/dokimi/formal/repo_batch/cfg/mut_count_every_commit.cfg new file mode 100644 index 000000000..41d78b896 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/mut_count_every_commit.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation RetryNotRepetition +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = TRUE +CHECK_DEADLOCK FALSE +INVARIANT RetryNotRepetition diff --git a/dokimi/formal/repo_batch/cfg/mut_no_cancel_guard.cfg b/dokimi/formal/repo_batch/cfg/mut_no_cancel_guard.cfg new file mode 100644 index 000000000..5b4733bce --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/mut_no_cancel_guard.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation CancelContract +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = FALSE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT CancelContract diff --git a/dokimi/formal/repo_batch/cfg/mut_no_lock.cfg b/dokimi/formal/repo_batch/cfg/mut_no_lock.cfg new file mode 100644 index 000000000..84b4eb20a --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/mut_no_lock.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoStaleOverwrite +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = FALSE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoStaleOverwrite diff --git a/dokimi/formal/repo_batch/cfg/no_fairness.cfg b/dokimi/formal/repo_batch/cfg/no_fairness.cfg new file mode 100644 index 000000000..fa558e53f --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/no_fairness.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation InvocationEnds +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +PROPERTY InvocationEnds diff --git a/dokimi/formal/repo_batch/cfg/witness_NoCancel.cfg b/dokimi/formal/repo_batch/cfg/witness_NoCancel.cfg new file mode 100644 index 000000000..2c70c8571 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/witness_NoCancel.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoCancel +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoCancel diff --git a/dokimi/formal/repo_batch/cfg/witness_NoCrashAfterArtifacts.cfg b/dokimi/formal/repo_batch/cfg/witness_NoCrashAfterArtifacts.cfg new file mode 100644 index 000000000..17b2b05b3 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/witness_NoCrashAfterArtifacts.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoCrashAfterArtifacts +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoCrashAfterArtifacts diff --git a/dokimi/formal/repo_batch/cfg/witness_NoResumeAfterCrash.cfg b/dokimi/formal/repo_batch/cfg/witness_NoResumeAfterCrash.cfg new file mode 100644 index 000000000..33e18fc72 --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/witness_NoResumeAfterCrash.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoResumeAfterCrash +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoResumeAfterCrash diff --git a/dokimi/formal/repo_batch/cfg/witness_NoRetryHappens.cfg b/dokimi/formal/repo_batch/cfg/witness_NoRetryHappens.cfg new file mode 100644 index 000000000..f8f84640b --- /dev/null +++ b/dokimi/formal/repo_batch/cfg/witness_NoRetryHappens.cfg @@ -0,0 +1,18 @@ +\* Copyright (C) 2026 Intel Corporation +\* SPDX-License-Identifier: Apache-2.0 +\* EXPECT: violation NoRetryHappens +SPECIFICATION Spec +CONSTANTS + Tasks = {t1, t2} + Workers = {w1, w2} + Configs = {cA, cB} + MaxInv = 3 + Locked = TRUE + StartCheck = TRUE + UniquePlan = TRUE + CancelGuard = TRUE + ReportCheck = TRUE + AcceptStale = FALSE + CountLog = FALSE +CHECK_DEADLOCK FALSE +INVARIANT NoRetryHappens diff --git a/dokimi/formal/repo_batch/run.sh b/dokimi/formal/repo_batch/run.sh new file mode 100755 index 000000000..7b920f480 --- /dev/null +++ b/dokimi/formal/repo_batch/run.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# Copyright (C) 2026 Intel Corporation +# SPDX-License-Identifier: Apache-2.0 +# Run TLC on the given cfgs (default every cfg/*.cfg) and check each against its "EXPECT:" line; see README.md. +set -euo pipefail +here=$(cd "$(dirname "$0")" && pwd) +jar=${TLA2TOOLS_JAR:?set TLA2TOOLS_JAR to tla2tools.jar (v1.8.0)} +java=${JAVA:-java} +out=${OUT:-$here/out} +workers=${TLC_WORKERS:-4} +mkdir -p "$out" +summary="$out/summary.tsv" +printf 'cfg\texpect\tgot\tok\tgenerated\tdistinct\tdepth\tseconds\n' > "$summary" +fail=0 +[ $# -gt 0 ] || set -- "$here"/cfg/*.cfg +for cfg in "$@"; do + name=$(basename "$cfg" .cfg) + expect=$(sed -n 's/^\\\* EXPECT: //p' "$cfg") + log="$out/$name.log" + start=$(date +%s.%N) + set +e + (cd "$here" && "$java" -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers "$workers" -deadlock -noGenerateSpecTE \ + -metadir "$out/states/$name" -config "$cfg" RepoBatch.tla) > "$log" 2>&1 + rc=$? + set -e + secs=$(echo "$(date +%s.%N) - $start" | bc) + if grep -q '^Model checking completed. No error has been found.' "$log"; then + got=pass + elif name_v=$(grep -oP '^Error: Invariant \K\S+(?= is violated)' "$log"); then + got="violation $name_v" + elif name_v=$(grep -oP '^Error: Temporal property \K\S+(?= was violated)' "$log"); then + got="violation $name_v" + else + got="error rc=$rc" + fi + gen=$(grep -oP '^\d+ states generated, \K\d+(?= distinct)' "$log" | tail -1 || true) + all=$(grep -oP '^\K\d+(?= states generated)' "$log" | tail -1 || true) + depth=$(grep -oP 'depth of the complete state graph search is \K\d+' "$log" || true) + ok=yes; [ "$got" = "$expect" ] || { ok=NO; fail=1; } + printf '%s\t%s\t%s\t%s\t%s\t%s\t%s\t%.1f\n' "$name" "$expect" "$got" "$ok" "${all:-}" "${gen:-}" "${depth:-}" "$secs" >> "$summary" +done +column -t -s $'\t' "$summary" +exit $fail diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py new file mode 100644 index 000000000..457adc076 --- /dev/null +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -0,0 +1,148 @@ +# Copyright (C) 2026 Intel Corporation +# SPDX-License-Identifier: Apache-2.0 + +"""`repo run` cell lifecycle: the counterexamples TLC found in formal/repo_batch/RepoBatch.tla, replayed. + +Each test names the TLC config whose trace it follows. No docker, no LLM. +""" + +from __future__ import annotations + +import json +import os +import signal +import threading +import time + +import pytest +import yaml + +from dokimi.cli import build_parser +from dokimi.repos import runner as repo_runner +from dokimi.repos.report import CellFileError, summarize +from repo_eval_fixture import FakeRunner, fake_harness, make_repo + + +@pytest.fixture +def setup(tmp_path, monkeypatch): + root, _ = make_repo(tmp_path) + exe, profile = fake_harness(tmp_path) + runner = FakeRunner() + monkeypatch.setattr("dokimi.repos.container.DockerRunner", lambda *a, **k: runner) + monkeypatch.setenv("FAKE_ACTION", "fix") + return {"root": root, "exe": exe, "profile": profile, "runner": runner, "out": tmp_path / "runs"} + + +def _run(s, *extra, models=("m-1",)): + argv = ["repo", "run", f"{s['root']}@HEAD", "--manifest", ".agent-eval/repo-eval.yaml", "--harness", + str(s["profile"]), "--bin", str(s["exe"]), *[a for m in models for a in ("--model", m)], + "--batch", "b1", "--out", str(s["out"]), "--cache-root", str(s["out"] / "caches"), + "--agent-network", "host", "--arm", "guidance:raw", *extra] + args = build_parser().parse_args(argv) + args.func(args) + + +def _agents(s): + return [spec for spec in s["runner"].specs if "-p" in spec.argv] + + +@pytest.mark.parametrize("extra, models", [ + (("--task", "fix_add", "--task", "fix_add"), ("m-1",)), + (("--task", "fix_add"), ("m-1", "m-1")), + (("--task", "fix_add"), ("org/m-1", "org:m-1")), # one slug, one directory +]) +def test_a_plan_naming_one_cell_twice_is_refused_before_any_agent(setup, capsys, extra, models): + # cfg/code_main_dup_plan.cfg: two threads took one cell; the second rmtree'd the first one's directory while + # its agent ran, and the first then wrote result.json next to the second one's meta.json and answer.txt. + with pytest.raises(SystemExit) as exc: + _run(setup, *extra, "--jobs", "2", models=models) + assert exc.value.code == 1 + assert "is planned 2 times" in capsys.readouterr().err + assert not _agents(setup) + assert not list((setup["out"] / "b1").glob("*/result.json")) + + +def test_ctrl_c_starts_no_queued_cell(setup, monkeypatch): + # CancelContract of cfg/fixed.cfg (cfg/mut_no_cancel_guard.cfg breaks it): SIGINT wakes the main thread and + # pool.map cancels the queued cells; _thread.interrupt_main() sends no signal and would let them start. + started = [] + both = threading.Barrier(2) + real = repo_runner.run_cell + + def run_cell(ctx, task, arm, rep, *args, **kwargs): + started.append(rep) + if rep <= 2: + both.wait(5) # both threads busy, every cell already submitted to the pool + if rep == 1: + os.kill(os.getpid(), signal.SIGINT) # what Ctrl-C sends + time.sleep(0.3) # the main thread takes the interrupt while these cells still run + return real(ctx, task, arm, rep, *args, **kwargs) + + monkeypatch.setattr(repo_runner, "run_cell", run_cell) + with pytest.raises(KeyboardInterrupt): + _run(setup, "--task", "fix_add", "--reps", "5", "--jobs", "2") + batch = setup["out"] / "b1" + for _ in range(100): # the running cells are not joined; they end on their own + if len(list(batch.glob("*/result.json"))) == 2: + break + time.sleep(0.05) + time.sleep(0.3) # a thread that would start another cell has had the time to + assert sorted(started) == [1, 2] + summary = summarize(batch) # the running cells finished; the queued ones are missing, not failed + assert summary["cells"] == 2 + assert summary["missing"] == [f"fix_add__guidance-raw__m-1__r{r}" for r in (3, 4, 5)] + + +def test_a_force_run_stopped_part_way_does_not_pool_two_executions(setup, monkeypatch, capsys): + # cfg/code_main_force_crash.cfg: --force with another execution replaced r1, then stopped; r2 kept the old + # execution and `repo report` pooled both in one row. + _run(setup, "--task", "fix_add", "--reps", "2") + raw = yaml.safe_load(setup["profile"].read_text()) + raw["delegation"] = {"none": {"all": [*raw["tools"]["all"], "--no-agents"]}} + setup["profile"].write_text(yaml.safe_dump(raw)) + real = repo_runner.run_cell + + def run_cell(ctx, task, arm, rep, *args, **kwargs): + if rep == 2: + raise KeyboardInterrupt + return real(ctx, task, arm, rep, *args, **kwargs) + + monkeypatch.setattr(repo_runner, "run_cell", run_cell) + with pytest.raises(KeyboardInterrupt): + _run(setup, "--task", "fix_add", "--reps", "2", "--delegation", "none", "--force") + batch = setup["out"] / "b1" + ids = {json.loads((batch / f"fix_add__guidance-raw__m-1__r{r}/result.json").read_text())["execution"]["id"] + for r in (1, 2)} + assert len(ids) == 2 + with pytest.raises(CellFileError, match="ran with executions") as exc: + summarize(batch) + assert all(i in str(exc.value) for i in ids) + + monkeypatch.setattr(repo_runner, "run_cell", real) # finishing the forced run makes the batch one execution + _run(setup, "--task", "fix_add", "--reps", "2", "--delegation", "none", "--force") + assert summarize(batch)["rows"][0]["n"] == 2 + + +def test_a_resume_after_a_crash_between_the_artifacts_and_result_json_reruns_the_cell_once(setup, monkeypatch): + # cfg/witness_NoCrashAfterArtifacts.cfg, then P1/P2 of cfg/fixed.cfg: the crashed cell is missing, the resume + # replaces its directory, and the report counts it once, with the files of the attempt that finished. + def crash(path, data): + if path.name == "result.json": + raise SystemExit("killed") # the process dies after meta.json, answer.txt and grade.json + return real_write(path, data) + + real_write = repo_runner._write_json + monkeypatch.setattr(repo_runner, "_write_json", crash) + with pytest.raises(SystemExit): + _run(setup, "--task", "fix_add") + rd = setup["out"] / "b1/fix_add__guidance-raw__m-1__r1" + assert (rd / "answer.txt").is_file() and not (rd / "result.json").exists() + assert summarize(setup["out"] / "b1")["missing"] == [rd.name] + first = json.loads((rd / "meta.json").read_text())["start_sha"] + + monkeypatch.setattr(repo_runner, "_write_json", real_write) + _run(setup, "--task", "fix_add") + summary = summarize(setup["out"] / "b1") + assert summary["missing"] == [] and summary["rows"][0]["n"] == 1 + assert json.loads((rd / "meta.json").read_text())["start_sha"] == first + assert len(_agents(setup)) == 2 # the retry is a second attempt at r1, not an r2 From 475b47e2e4e0befdc8fd55470634cb89735b6876 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Wed, 11 Nov 2026 19:08:26 -0800 Subject: [PATCH 02/18] fix(report): check executions per compared row, not in load_cells; review fixes Self-review: the refusal in load_cells also blocked hits and a compare of clean arms beside a mixed one; it now runs in summarize and on the rows compare pools. Docs name the harness-binary cause; the Ctrl-C test sets its own SIGINT handler; README lists the gaps the review found. Signed-off-by: Nikolay Petrov --- ...11_180000_napetrov_repo-batch-lifecycle.md | 14 ++++---- dokimi/docs/repo-evaluation-contract.md | 7 ++-- dokimi/dokimi/repos/compare.py | 3 +- dokimi/dokimi/repos/report.py | 20 ++++++------ dokimi/dokimi/repos/runner.py | 2 +- dokimi/formal/repo_batch/README.md | 14 +++++--- dokimi/tests/test_repo_batch_lifecycle.py | 32 +++++++++++++------ 7 files changed, 59 insertions(+), 33 deletions(-) diff --git a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md index f458221a5..85f591926 100644 --- a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md +++ b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md @@ -4,13 +4,15 @@ `--model` strings with one directory name (`a/b` and `a:b`), put two runs in one cell directory; with `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's `meta.json` and answer. The run now stops before any agent starts, naming the cell. -- **`repo report` and `repo compare` refuse a batch whose arm and model hold two executions** — a - `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell) left - some cells on the old execution and was pooled with them in one row. The refusal names both ids; - a `--force` run that finishes the batch clears it. +- **`repo report` and `repo compare` refuse an arm and model whose cells hold two executions** — a + `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell), or a + harness binary replaced while the batch ran, left cells of two executions that were pooled in one + row. A batch that reported before can now be refused; the message names both ids, and `--force` + on the cells of the older one clears it. `repo compare` checks only the rows it compares. ### Added - **`formal/repo_batch`: a TLA+ model of the `repo run` cell lifecycle** — retries, crashes, - resume, `--force`, Ctrl-C and what the report counts, with TLC configs for the code, the fixes - and two mutations; `run.sh` checks each against its expected result. + resume, `--force`, Ctrl-C and what the report counts, with TLC configs for the code before the + fixes, the fixed code, four mutations, a run without fairness and four vacuity witnesses; + `run.sh` checks each against its expected result. diff --git a/dokimi/docs/repo-evaluation-contract.md b/dokimi/docs/repo-evaluation-contract.md index 5c3805f1d..802cc335f 100644 --- a/dokimi/docs/repo-evaluation-contract.md +++ b/dokimi/docs/repo-evaluation-contract.md @@ -2304,9 +2304,10 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric cell again. The same holds for a finished cell of a task this host cannot run, except that `--force` keeps it: once its file is removed, the cell runs on a host that meets the task's requirements. A `--force` run that stops part - way (Ctrl-C, a crash, a failed cell) can leave finished cells of two `id`s in - one arm and model; `repo report` and `repo compare` refuse such a batch, naming - both `id`s, until a `--force` run finishes it. A plan naming one cell twice (a + way (Ctrl-C, a crash, a failed cell), or a harness binary replaced while the + batch runs, can leave finished cells of two `id`s in one arm and model; `repo + report` refuses such a batch and `repo compare` such a compared row, naming + both `id`s, until `--force` reruns the cells of the older one. A plan naming one cell twice (a repeated `--task` or `--model`, or two `--model` strings with one directory name, `a/b` and `a:b`) is refused before any agent starts. Ctrl-C lets the running cells finish and starts no queued one. A batch stays on the eval tree it diff --git a/dokimi/dokimi/repos/compare.py b/dokimi/dokimi/repos/compare.py index 7d08f27b9..465786cfd 100644 --- a/dokimi/dokimi/repos/compare.py +++ b/dokimi/dokimi/repos/compare.py @@ -123,7 +123,7 @@ from .compare_tasks import CompareError, select_tasks from .compare_values import finite_values, task_values from .process_counts import as_measure, process_order, process_values -from .report import (load_cells, mismatch_warnings, model_mismatch, resolved_models, +from .report import (load_cells, mismatch_warnings, model_mismatch, refuse_mixed_executions, resolved_models, unmeasured_note, uptake_counts) from .useful import USEFUL_MEASURES, useful_arms_line, useful_counts @@ -203,6 +203,7 @@ def compare(batch_dirs: list[Path], baseline: str, treatments: list[str] | None treatments = _treatments(cells, baseline, base_sel, treatments, scope) compared = _in_models([c for c in cells if any(selector_matches(parse_selector(t), c) for t in [baseline, *treatments])], models) # a judged-recall file of an excluded arm or model does not count + refuse_mixed_executions(compared, "batch") # only the rows compared: a mixed arm left out does not block check_reported(metrics, compared, scope) measures = ["gate", "score", *([f"pass^{pass_k}"] if pass_k else []), *(["path_distance"] if path_stability else []), "cost_usd", "turns", "first_prompt_tokens", diff --git a/dokimi/dokimi/repos/report.py b/dokimi/dokimi/repos/report.py index f5b9a8fb7..c59c03d07 100644 --- a/dokimi/dokimi/repos/report.py +++ b/dokimi/dokimi/repos/report.py @@ -194,22 +194,23 @@ def load_cells(batch_dir: Path) -> tuple[list[dict[str, Any]], list[str]]: with reading_cells([str(path)]): rec["score_task"] = bool(rec["score_task"] if "score_task" in rec else rec["grade"]["score_only"]) finished.append(rec) - _refuse_mixed_executions(batch_dir, finished) done = {r["cell"] for r in finished} unsupported = {p.parent.name for p in batch_dir.glob(f"*/{UNSUPPORTED_FILE}")} return finished, sorted((planned | started) - done - unsupported) -def _refuse_mixed_executions(batch_dir: Path, finished: list[dict[str, Any]]) -> None: - """One (arm, model) of a batch ran with one execution: a --force run that stopped part way leaves two.""" - seen: dict[tuple[str, str], set[str]] = defaultdict(set) - for rec in finished: +def refuse_mixed_executions(cells: list[dict[str, Any]], where: str) -> None: + """One (batch, arm, model) ran with one execution: a ``--force`` run that stopped part way, or a harness + binary replaced mid-batch, leaves two, and pooling them would blend two setups in one row.""" + seen: dict[tuple[str, str, str], set[str]] = defaultdict(set) + for rec in cells: ran = recorded_execution(rec).get("id") - seen[(rec["arm"], rec["model"])].add(ran if isinstance(ran, str) else "unrecorded") - for (arm, model), ids in sorted(seen.items()): + seen[(rec.get("batch", ""), rec["arm"], rec["model"])].add(ran if isinstance(ran, str) else "unrecorded") + for (batch, arm, model), ids in sorted(seen.items()): if len(ids) > 1: - raise CellFileError(f"{batch_dir}: the cells of arm {arm}, model {model} ran with executions " - f"{', '.join(sorted(ids))}; rerun the batch with --force to finish it, or use another --batch") + raise CellFileError(f"{batch or where}: the cells of arm {arm}, model {model} ran with executions " + f"{', '.join(sorted(ids))}; rerun the cells of the older ones with --force " + "(--task, --arm, --model) to finish them, or use another --batch") def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]: @@ -226,6 +227,7 @@ def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]: def summarize(batch_dir: Path) -> dict[str, Any]: cells, missing = load_cells(batch_dir) + refuse_mixed_executions(cells, str(batch_dir)) groups: dict[tuple[str, str, str], list[dict[str, Any]]] = defaultdict(list) for rec in cells: groups[(rec["task"], rec["arm"], rec["model"])].append(rec) diff --git a/dokimi/dokimi/repos/runner.py b/dokimi/dokimi/repos/runner.py index 10ad689a8..44311a6cc 100644 --- a/dokimi/dokimi/repos/runner.py +++ b/dokimi/dokimi/repos/runner.py @@ -444,7 +444,7 @@ def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> No shared = sorted(name for name, n in names.items() if n > 1) if shared: raise ValueError(f"cell {shared[0]} is planned {names[shared[0]]} times (a repeated --task or --model, or " - "two --model strings with one name on disk); give each once") + "two --model strings with one name on disk, or a repeated --arm); give each once") UNSUPPORTED_FILE = "unsupported.json" diff --git a/dokimi/formal/repo_batch/README.md b/dokimi/formal/repo_batch/README.md index a4f224c25..a123edc59 100644 --- a/dokimi/formal/repo_batch/README.md +++ b/dokimi/formal/repo_batch/README.md @@ -36,7 +36,7 @@ result differs from its expectation. `out/` is not committed. | Workers | `ThreadPoolExecutor(jobs)` + `pool.map` | `Workers` threads | | Timeout | agent killed, the cell is graded (an outcome, not a retry) | inside `Work` | | Crash | process dies; no `result.json` → cell is *missing*, the next run fills it | `Crash` | -| Late result of an old attempt | impossible in-process: threads die with the process | `LateCommit`, mutation only | +| Late result of an old attempt | none after SIGKILL: threads die with the process (a second Ctrl-C is not modelled, open question 4) | `LateCommit`, mutation only | | Cancel | Ctrl-C: `KeyboardInterrupt`; `pool.map` cancels queued futures, running cells finish | `Cancel`, `CancelGuard` | | Exclusion of concurrent runs on one batch | `batch_lock` (flock on `_eval/lock`) | `Locked` | | Execution pinning | `execution.id` in `meta.json`/`result.json`; `check_batch_executions` before any cell | `Configs`, `StartCheck` | @@ -54,7 +54,7 @@ result differs from its expectation. `out/` is not committed. | `Work(w)` | agent run, then `meta.json`, `events.jsonl`, `answer.txt`, `task.json`, grade, written by path | | `Commit(w)` | `_write_json(rd / "result.json", record)` | | `Crash(i)` | SIGKILL / OOM / reboot: flock released, threads gone | -| `Cancel(i)`, `Finish(i)` | Ctrl-C; pool join and the exit code of `cmd_repo_run` (1 on errors, interrupt, budget stop, probe failure) | +| `Cancel(i)`, `Finish(i)` | Ctrl-C; pool join and the exit code of `cmd_repo_run` (1 on errors, budget stop, probe failure; an interrupt exits by `KeyboardInterrupt`, 130) | | `LateCommit(a)` | mutation `AcceptStale` only | ## Properties @@ -64,7 +64,7 @@ result differs from its expectation. `out/` is not committed. | P1 | `RetryNotRepetition` | a cell is one sample at most, however often it ran | `load_cells` reads one `result.json` per dir; the retry reuses the cell name | | P2 | `OnlyValidAttempts` | a counted result is a finished attempt of that cell, beside that attempt's files only | `run_cell` rmtree's before an attempt; `result.json` written last; `_refuse_shared_cells` | | P3 | `NoStaleOverwrite` | no `result.json` from an attempt that no longer owns the dir | `batch_lock`; threads die with the process; `_refuse_shared_cells` | -| P4 | `OneConfig` | the cells of one report row ran under one `execution.id` | `check_batch_executions`; `_refuse_mixed_executions` in `load_cells` | +| P4 | `OneConfig` | the cells of one report row ran under one `execution.id` | `check_batch_executions`; `refuse_mixed_executions` in `summarize` and `compare` | | P5 | `PartialNotComplete` | exit 0 only with every planned cell done; the rest are *missing* | exit logic of `cmd_repo_run`; `record_plan` + `load_cells` | | P6 | `CancelContract` | no attempt starts after Ctrl-C; the run does not exit 0 | `pool.map` cancels pending futures when the main thread raises | | P7 | `InvocationEnds` (liveness) | every invocation ends | under `Fairness` only | @@ -119,7 +119,7 @@ tla2tools v1.8.0 (TLC2 Version 2026.11.06.222357, rev d8fb231), 4 TLC workers, T attempt's `meta.json`/answer. Fixed: `_refuse_shared_cells`. 2. **A part-way `--force` with another execution pools two executions** (`code_main_force_crash`, found by TLC on its first run of `fixed`): `--force` replaced r1, then the run stopped; r2 kept - the old execution and `repo report` pooled both in one row. Fixed: `_refuse_mixed_executions`. + the old execution and `repo report` pooled both in one row. Fixed: `refuse_mixed_executions`. The same refusal catches a harness binary replaced mid-batch, which the model does not have (one execution per invocation, while the code hashes `--bin` per cell). 3. **Ctrl-C** (`mut_no_cancel_guard`): a probe with `_thread.interrupt_main()` started queued cells, but a real SIGINT wakes the main thread and `pool.map` cancels them. Not a bug; the test pins it. @@ -130,6 +130,12 @@ Open questions (left as they are): 2. A grader with write access to the run dir could leave a `result.json` when the host fails to write its own (`CellCrash`); a resume would reuse it. 3. Caps (timeout, max turns, per-cell budget) are not in `execution.id`, so one row can mix caps. +4. A second Ctrl-C leaves `batch_lock` while the pool's threads still finish their cells, so another + `repo run` can take the batch meanwhile (pre-existing; the model has no second interrupt). +5. Not modelled: a cell failing inside a live process (`CellCrash`, `PrepError`), so P5 is checked + on crashes and Ctrl-C, not on the cell-error path. P1 and P4 follow closely from how `Samples` + and `Counted` are defined; the mutations show they are not vacuous. +6. `run.sh` is not part of CI; the action → code table can drift from the code. ## A formal-verification evaluator for agent tasks (proposal) diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index 457adc076..80e300abd 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -19,7 +19,7 @@ from dokimi.cli import build_parser from dokimi.repos import runner as repo_runner -from dokimi.repos.report import CellFileError, summarize +from dokimi.repos.report import CellFileError, refuse_mixed_executions, summarize from repo_eval_fixture import FakeRunner, fake_harness, make_repo @@ -79,14 +79,13 @@ def run_cell(ctx, task, arm, rep, *args, **kwargs): return real(ctx, task, arm, rep, *args, **kwargs) monkeypatch.setattr(repo_runner, "run_cell", run_cell) - with pytest.raises(KeyboardInterrupt): - _run(setup, "--task", "fix_add", "--reps", "5", "--jobs", "2") - batch = setup["out"] / "b1" - for _ in range(100): # the running cells are not joined; they end on their own - if len(list(batch.glob("*/result.json"))) == 2: - break - time.sleep(0.05) - time.sleep(0.3) # a thread that would start another cell has had the time to + old = signal.signal(signal.SIGINT, signal.default_int_handler) # a shell may have left SIGINT ignored + try: + with pytest.raises(KeyboardInterrupt): + _run(setup, "--task", "fix_add", "--reps", "5", "--jobs", "2") + finally: + signal.signal(signal.SIGINT, old) + batch = setup["out"] / "b1" # the pool joined the two running cells before the interrupt left run_batch assert sorted(started) == [1, 2] summary = summarize(batch) # the running cells finished; the queued ones are missing, not failed assert summary["cells"] == 2 @@ -146,3 +145,18 @@ def crash(path, data): assert summary["missing"] == [] and summary["rows"][0]["n"] == 1 assert json.loads((rd / "meta.json").read_text())["start_sha"] == first assert len(_agents(setup)) == 2 # the retry is a second attempt at r1, not an r2 + + +def _cell(arm, model, ran, batch=""): + return {"batch": batch, "arm": arm, "model": model, "execution": {"id": ran}} + + +def test_the_mixed_execution_refusal_is_per_batch_arm_and_model(): + # one execution per row is the rule; two arms, two models or two batches may each have their own + ok = [_cell("a", "m", "e1"), _cell("a", "m", "e1"), _cell("b", "m", "e2"), _cell("a", "n", "e3"), + _cell("a", "m", "e4", batch="other")] + refuse_mixed_executions(ok, "b1") + with pytest.raises(CellFileError, match="arm a, model m ran with executions e1, e4"): + refuse_mixed_executions([*ok, _cell("a", "m", "e4")], "b1") + with pytest.raises(CellFileError, match="e1, unrecorded"): + refuse_mixed_executions([_cell("a", "m", "e1"), {"arm": "a", "model": "m"}], "b1") From 2d2fdb4df7a28d4ebe81bee429ab12a94ddd5daa Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Wed, 11 Nov 2026 19:24:34 -0800 Subject: [PATCH 03/18] test(compare): cover the compared-row refusal; fold self-review nits Signed-off-by: Nikolay Petrov --- dokimi/dokimi/repos/report.py | 4 ++-- dokimi/dokimi/repos/runner.py | 2 +- dokimi/tests/test_repo_batch_lifecycle.py | 13 +++++++++++++ 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/dokimi/dokimi/repos/report.py b/dokimi/dokimi/repos/report.py index c59c03d07..5969c8a5f 100644 --- a/dokimi/dokimi/repos/report.py +++ b/dokimi/dokimi/repos/report.py @@ -209,8 +209,8 @@ def refuse_mixed_executions(cells: list[dict[str, Any]], where: str) -> None: for (batch, arm, model), ids in sorted(seen.items()): if len(ids) > 1: raise CellFileError(f"{batch or where}: the cells of arm {arm}, model {model} ran with executions " - f"{', '.join(sorted(ids))}; rerun the cells of the older ones with --force " - "(--task, --arm, --model) to finish them, or use another --batch") + f"{', '.join(sorted(ids))}; rerun that arm and model with --force and the batch's --task and " + "--reps, so every cell has one execution, or use another --batch") def load_unsupported(batch_dir: Path) -> list[dict[str, Any]]: diff --git a/dokimi/dokimi/repos/runner.py b/dokimi/dokimi/repos/runner.py index 44311a6cc..10ad689a8 100644 --- a/dokimi/dokimi/repos/runner.py +++ b/dokimi/dokimi/repos/runner.py @@ -444,7 +444,7 @@ def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> No shared = sorted(name for name, n in names.items() if n > 1) if shared: raise ValueError(f"cell {shared[0]} is planned {names[shared[0]]} times (a repeated --task or --model, or " - "two --model strings with one name on disk, or a repeated --arm); give each once") + "two --model strings with one name on disk); give each once") UNSUPPORTED_FILE = "unsupported.json" diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index 80e300abd..cbe32b337 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -19,6 +19,7 @@ from dokimi.cli import build_parser from dokimi.repos import runner as repo_runner +from dokimi.repos.compare import compare from dokimi.repos.report import CellFileError, refuse_mixed_executions, summarize from repo_eval_fixture import FakeRunner, fake_harness, make_repo @@ -160,3 +161,15 @@ def test_the_mixed_execution_refusal_is_per_batch_arm_and_model(): refuse_mixed_executions([*ok, _cell("a", "m", "e4")], "b1") with pytest.raises(CellFileError, match="e1, unrecorded"): refuse_mixed_executions([_cell("a", "m", "e1"), {"arm": "a", "model": "m"}], "b1") + + +def test_compare_refuses_only_a_compared_row_of_two_executions(setup): + _run(setup, "--task", "fix_add", "--arm", "guidance:none,guidance:bridge", "--reps", "2") + b1 = setup["out"] / "b1" + target = b1 / "fix_add__guidance-bridge__m-1__r1/result.json" + rec = json.loads(target.read_text()) + rec["execution"]["id"] = "old" # what a --force run stopped part way leaves beside the new cells + target.write_text(json.dumps(rec)) + with pytest.raises(CellFileError, match="arm guidance:bridge, model m-1 ran with executions"): + compare([b1], "guidance:none", ["guidance:bridge"]) + assert compare([b1], "guidance:none", ["guidance:raw"])["comparisons"] # the mixed arm is not compared From 88111f63e8594b97050a3fb5e3e60c8617a77771 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Wed, 11 Nov 2026 23:05:54 -0800 Subject: [PATCH 04/18] chore(formal): license header on repo_batch/.gitignore Signed-off-by: Nikolay Petrov --- dokimi/formal/repo_batch/.gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dokimi/formal/repo_batch/.gitignore b/dokimi/formal/repo_batch/.gitignore index 0c1bb46b7..67c80f816 100644 --- a/dokimi/formal/repo_batch/.gitignore +++ b/dokimi/formal/repo_batch/.gitignore @@ -1,2 +1,4 @@ +# Copyright (C) 2026 Intel Corporation +# SPDX-License-Identifier: Apache-2.0 out/ RepoBatch_TTrace_* From 4b5924b2951a6e94bbf91410cc67a9219f57cb79 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Wed, 11 Nov 2026 23:30:21 -0800 Subject: [PATCH 05/18] ci(licenses): skip TLC .cfg files, headed in TLA+ comments Signed-off-by: Nikolay Petrov --- .github/.licenserc.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/.licenserc.yaml b/.github/.licenserc.yaml index dff08ffea..00a3ab711 100644 --- a/.github/.licenserc.yaml +++ b/.github/.licenserc.yaml @@ -66,6 +66,8 @@ header: # CHANGELOG.md, which carries the header itself. - 'dokimi/changelog.d/[0-9]*.md' - 'dokimi/changelog.d/fragment_template.md.j2' + # TLC configs carry the header in TLA+ \\* comments, a style eyes does not know. + - 'dokimi/formal/**/*.cfg' # Third-party eval files copied unchanged, under their own licenses # (dokimi/tests/fixtures/task_formats/MANIFEST.yaml, LICENSES/). - 'dokimi/tests/fixtures/task_formats/**' From d7d37e8c289c3f2a91ddddb8dbec0c0443837f3c Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Thu, 12 Nov 2026 00:06:04 -0800 Subject: [PATCH 06/18] test(repo): Ctrl-C test waits for the running cells; skip TLA+ files in eyes The with-block join can end after the interrupt leaves run_batch, so the second running cell's result.json could land after summarize read the batch (1 of 15 local runs, the 3.14 leg in CI). Wait for both cells. Signed-off-by: Nikolay Petrov --- .github/.licenserc.yaml | 3 ++- dokimi/tests/test_repo_batch_lifecycle.py | 9 +++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/.github/.licenserc.yaml b/.github/.licenserc.yaml index 00a3ab711..12380bba5 100644 --- a/.github/.licenserc.yaml +++ b/.github/.licenserc.yaml @@ -66,7 +66,8 @@ header: # CHANGELOG.md, which carries the header itself. - 'dokimi/changelog.d/[0-9]*.md' - 'dokimi/changelog.d/fragment_template.md.j2' - # TLC configs carry the header in TLA+ \\* comments, a style eyes does not know. + # TLA+ specs and TLC configs carry the header in TLA+ comments, a style eyes does not know. + - 'dokimi/formal/**/*.tla' - 'dokimi/formal/**/*.cfg' # Third-party eval files copied unchanged, under their own licenses # (dokimi/tests/fixtures/task_formats/MANIFEST.yaml, LICENSES/). diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index cbe32b337..0de97eb40 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -68,6 +68,7 @@ def test_ctrl_c_starts_no_queued_cell(setup, monkeypatch): # pool.map cancels the queued cells; _thread.interrupt_main() sends no signal and would let them start. started = [] both = threading.Barrier(2) + ended = threading.Semaphore(0) real = repo_runner.run_cell def run_cell(ctx, task, arm, rep, *args, **kwargs): @@ -77,7 +78,10 @@ def run_cell(ctx, task, arm, rep, *args, **kwargs): if rep == 1: os.kill(os.getpid(), signal.SIGINT) # what Ctrl-C sends time.sleep(0.3) # the main thread takes the interrupt while these cells still run - return real(ctx, task, arm, rep, *args, **kwargs) + try: + return real(ctx, task, arm, rep, *args, **kwargs) + finally: + ended.release() monkeypatch.setattr(repo_runner, "run_cell", run_cell) old = signal.signal(signal.SIGINT, signal.default_int_handler) # a shell may have left SIGINT ignored @@ -86,7 +90,8 @@ def run_cell(ctx, task, arm, rep, *args, **kwargs): _run(setup, "--task", "fix_add", "--reps", "5", "--jobs", "2") finally: signal.signal(signal.SIGINT, old) - batch = setup["out"] / "b1" # the pool joined the two running cells before the interrupt left run_batch + batch = setup["out"] / "b1" + assert all(ended.acquire(timeout=30) for _ in range(2)) # running cells finish, maybe after run_batch raised assert sorted(started) == [1, 2] summary = summarize(batch) # the running cells finished; the queued ones are missing, not failed assert summary["cells"] == 2 From 4aba5a223934cfe776131b0aaec21ff79799ac24 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Thu, 12 Nov 2026 18:41:03 -0800 Subject: [PATCH 07/18] Address review: name every repeated cell and refuse case-only collisions _refuse_shared_cells now lists every repeated cell with its count, and refuses names that differ only in case, since they share one directory on a case-insensitive volume. Thread: PRRT_kwDOVBg7g8624FgM Thread: PRRT_kwDOVBg7g8624Y6I Signed-off-by: Nikolay Petrov --- dokimi/dokimi/repos/runner.py | 16 +++++++++++----- dokimi/tests/test_repo_batch_lifecycle.py | 21 +++++++++++++++++++++ 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/dokimi/dokimi/repos/runner.py b/dokimi/dokimi/repos/runner.py index 10ad689a8..241ea5717 100644 --- a/dokimi/dokimi/repos/runner.py +++ b/dokimi/dokimi/repos/runner.py @@ -439,12 +439,18 @@ def one(cell: tuple[Task, str, AgentOptions, int]) -> None: def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> None: - """Refuse a plan naming one cell directory twice: with --jobs 2 both would run in it and mix their files.""" + """Refuse a plan naming one cell directory twice, or two names one case-insensitive volume maps to one + directory: with --jobs 2 both would run in it and mix their files (or one would delete the other's).""" names = Counter(cell_name(t.id, a, o.model, r) for t, a, o, r in cells) - shared = sorted(name for name, n in names.items() if n > 1) - if shared: - raise ValueError(f"cell {shared[0]} is planned {names[shared[0]]} times (a repeated --task or --model, or " - "two --model strings with one name on disk); give each once") + problems = [f"cell {name} is planned {names[name]} times" for name in sorted(names) if names[name] > 1] + by_fold: dict[str, list[str]] = {} + for name in names: + by_fold.setdefault(name.casefold(), []).append(name) + problems += [f"cells {' and '.join(sorted(group))} are one directory on a case-insensitive volume" + for group in by_fold.values() if len(group) > 1] + if problems: + raise ValueError("; ".join(problems) + " (a repeated --task or --model, two --model strings with one name " + "on disk, or names that differ only in case); give each once") UNSUPPORTED_FILE = "unsupported.json" diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index 0de97eb40..ce5cddb20 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -63,6 +63,27 @@ def test_a_plan_naming_one_cell_twice_is_refused_before_any_agent(setup, capsys, assert not list((setup["out"] / "b1").glob("*/result.json")) +def test_every_repeated_cell_is_named_in_the_refusal(setup, capsys): + # two repeated --task values plan two cells twice: the refusal names both, not only the first + with pytest.raises(SystemExit) as exc: + _run(setup, "--task", "fix_add", "--task", "fix_add", "--reps", "2", "--jobs", "2") + assert exc.value.code == 1 + err = capsys.readouterr().err + assert "cell fix_add__guidance-raw__m-1__r1 is planned 2 times" in err + assert "cell fix_add__guidance-raw__m-1__r2 is planned 2 times" in err + assert not _agents(setup) + + +def test_names_that_differ_only_in_case_are_refused_before_any_agent(setup, capsys): + # on a case-insensitive volume (default macOS APFS) ...__m-1__r1 and ...__M-1__r1 are one directory: the + # run of one would rmtree the other's while it works in it + with pytest.raises(SystemExit) as exc: + _run(setup, "--task", "fix_add", "--jobs", "2", models=("m-1", "M-1")) + assert exc.value.code == 1 + assert "case-insensitive volume" in capsys.readouterr().err + assert not _agents(setup) + + def test_ctrl_c_starts_no_queued_cell(setup, monkeypatch): # CancelContract of cfg/fixed.cfg (cfg/mut_no_cancel_guard.cfg breaks it): SIGINT wakes the main thread and # pool.map cancels the queued cells; _thread.interrupt_main() sends no signal and would let them start. From 0fa65be671b0e71ad225244bc53a89e3e871b7b7 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Thu, 12 Nov 2026 18:41:03 -0800 Subject: [PATCH 08/18] Address review: make the repo_batch runner portable and path-safe run.sh resolves its jar, output and config paths from the caller's directory before it changes directory, and uses only POSIX tools (sed, tail, no grep -P, date +%N or bc), so it runs on macOS and minimal Linux. Thread: PRRT_kwDOVBg7g8624FgR Thread: PRRT_kwDOVBg7g8624Y65 Thread: PRRT_kwDOVBg7g8624Y7X Thread: PRRT_kwDOVBg7g8624Y7x Signed-off-by: Nikolay Petrov --- dokimi/formal/repo_batch/run.sh | 29 +++++--- dokimi/tests/test_repo_batch_run_script.py | 82 ++++++++++++++++++++++ 2 files changed, 100 insertions(+), 11 deletions(-) create mode 100644 dokimi/tests/test_repo_batch_run_script.py diff --git a/dokimi/formal/repo_batch/run.sh b/dokimi/formal/repo_batch/run.sh index 7b920f480..3252be63b 100755 --- a/dokimi/formal/repo_batch/run.sh +++ b/dokimi/formal/repo_batch/run.sh @@ -1,43 +1,50 @@ #!/usr/bin/env bash # Copyright (C) 2026 Intel Corporation # SPDX-License-Identifier: Apache-2.0 -# Run TLC on the given cfgs (default every cfg/*.cfg) and check each against its "EXPECT:" line; see README.md. +# Run TLC on the given cfgs (default every cfg/*.cfg) against each "EXPECT:" line; see README.md; POSIX tools only. +# Paths are read from the caller's directory, so they are made absolute before the cd. set -euo pipefail here=$(cd "$(dirname "$0")" && pwd) +# absolute without touching the file system, so a path that does not exist yet still resolves +abspath() { case $1 in /*) printf '%s\n' "$1" ;; *) printf '%s/%s\n' "$PWD" "$1" ;; esac; } jar=${TLA2TOOLS_JAR:?set TLA2TOOLS_JAR to tla2tools.jar (v1.8.0)} +jar=$(abspath "$jar") java=${JAVA:-java} -out=${OUT:-$here/out} +out=$(abspath "${OUT:-$here/out}") workers=${TLC_WORKERS:-4} mkdir -p "$out" summary="$out/summary.tsv" printf 'cfg\texpect\tgot\tok\tgenerated\tdistinct\tdepth\tseconds\n' > "$summary" fail=0 [ $# -gt 0 ] || set -- "$here"/cfg/*.cfg -for cfg in "$@"; do +cfgs=() +for cfg in "$@"; do cfgs+=("$(abspath "$cfg")"); done +for cfg in "${cfgs[@]}"; do name=$(basename "$cfg" .cfg) expect=$(sed -n 's/^\\\* EXPECT: //p' "$cfg") log="$out/$name.log" - start=$(date +%s.%N) + start=$SECONDS set +e (cd "$here" && "$java" -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers "$workers" -deadlock -noGenerateSpecTE \ -metadir "$out/states/$name" -config "$cfg" RepoBatch.tla) > "$log" 2>&1 rc=$? set -e - secs=$(echo "$(date +%s.%N) - $start" | bc) + secs=$((SECONDS - start)) if grep -q '^Model checking completed. No error has been found.' "$log"; then got=pass - elif name_v=$(grep -oP '^Error: Invariant \K\S+(?= is violated)' "$log"); then + elif name_v=$(sed -n 's/^Error: Invariant \([^ ]*\) is violated.*/\1/p' "$log" | tail -n 1) && [ -n "$name_v" ]; then got="violation $name_v" - elif name_v=$(grep -oP '^Error: Temporal property \K\S+(?= was violated)' "$log"); then + elif name_v=$(sed -n 's/^Error: Temporal property \([^ ]*\) was violated.*/\1/p' "$log" | tail -n 1) \ + && [ -n "$name_v" ]; then got="violation $name_v" else got="error rc=$rc" fi - gen=$(grep -oP '^\d+ states generated, \K\d+(?= distinct)' "$log" | tail -1 || true) - all=$(grep -oP '^\K\d+(?= states generated)' "$log" | tail -1 || true) - depth=$(grep -oP 'depth of the complete state graph search is \K\d+' "$log" || true) + gen=$(sed -n 's/^[0-9][0-9]* states generated, \([0-9][0-9]*\) distinct.*/\1/p' "$log" | tail -n 1) + all=$(sed -n 's/^\([0-9][0-9]*\) states generated.*/\1/p' "$log" | tail -n 1) + depth=$(sed -n 's/.*depth of the complete state graph search is \([0-9][0-9]*\).*/\1/p' "$log" | tail -n 1) ok=yes; [ "$got" = "$expect" ] || { ok=NO; fail=1; } printf '%s\t%s\t%s\t%s\t%s\t%s\t%s\t%.1f\n' "$name" "$expect" "$got" "$ok" "${all:-}" "${gen:-}" "${depth:-}" "$secs" >> "$summary" done -column -t -s $'\t' "$summary" +if command -v column >/dev/null 2>&1; then column -t -s $'\t' "$summary"; else cat "$summary"; fi exit $fail diff --git a/dokimi/tests/test_repo_batch_run_script.py b/dokimi/tests/test_repo_batch_run_script.py new file mode 100644 index 000000000..60ba0bee3 --- /dev/null +++ b/dokimi/tests/test_repo_batch_run_script.py @@ -0,0 +1,82 @@ +# Copyright (C) 2026 Intel Corporation +# SPDX-License-Identifier: Apache-2.0 + +"""formal/repo_batch/run.sh: explicit paths resolve from the caller's directory, and the script needs no GNU-only tools. + +A fake ``java`` stands in for TLC: it checks that the jar and the config it is given exist, then prints the line +run.sh reads as a pass. No TLA+ tools, no JVM. +""" + +from __future__ import annotations + +import os +import shutil +import subprocess +import sys +from pathlib import Path + +import pytest + +REPO = Path(__file__).resolve().parents[1] +RUN = REPO / "formal" / "repo_batch" / "run.sh" +FIXED = REPO / "formal" / "repo_batch" / "cfg" / "fixed.cfg" + +pytestmark = pytest.mark.skipif(os.name == "nt" or shutil.which("bash") is None, reason="run.sh is a bash script") + +FAKE_TLC = f"""#!{sys.executable} -I +import os +import sys + +args = sys.argv[1:] +jar = args[args.index("-cp") + 1] +cfg = args[args.index("-config") + 1] +with open(os.environ["FAKE_TLC_LOG"], "a", encoding="utf-8") as log: + log.write(repr(args) + "\\n") +if os.path.isfile(jar) and os.path.isfile(cfg): + print("Model checking completed. No error has been found.") + sys.exit(0) +print("Error: no such file") +sys.exit(1) +""" + + +def _fake_java(tmp_path: Path) -> Path: + java = tmp_path / "fake-java" + java.write_text(FAKE_TLC, encoding="utf-8") + java.chmod(0o755) + return java + + +def test_relative_paths_resolve_from_the_callers_directory(tmp_path): + # run.sh changes into its own directory to run TLC; a cfg, a jar or an OUT given relative to the caller must + # still be the caller's files + (tmp_path / "cfgs").mkdir() + shutil.copy(FIXED, tmp_path / "cfgs" / "fixed.cfg") + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": "tla2tools.jar", "OUT": "out", "JAVA": str(_fake_java(tmp_path)), + "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + res = subprocess.run(["bash", str(RUN), "cfgs/fixed.cfg"], cwd=tmp_path, env=env, + capture_output=True, text=True, check=False) + assert res.returncode == 0, res.stdout + res.stderr + assert (tmp_path / "out" / "fixed.log").is_file() + assert "fixed\tpass\tpass\tyes" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") + args = (tmp_path / "tlc.log").read_text(encoding="utf-8") + assert str((tmp_path / "cfgs" / "fixed.cfg").resolve()) in args + assert str((tmp_path / "tla2tools.jar").resolve()) in args + + +def test_the_script_runs_with_only_posix_tools_on_path(tmp_path): + # no bc, no date %N, no grep -P: the timing and the verdict parsing use what every POSIX host has + bindir = tmp_path / "bin" + bindir.mkdir() + for tool in ("sed", "grep", "head", "tail", "mkdir", "basename", "dirname", "cat", "awk"): + found = shutil.which(tool) + if found: + (bindir / tool).symlink_to(found) + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {"PATH": str(bindir), "TLA2TOOLS_JAR": str(tmp_path / "tla2tools.jar"), "OUT": str(tmp_path / "out"), + "JAVA": str(_fake_java(tmp_path)), "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + res = subprocess.run([shutil.which("bash"), str(RUN), str(FIXED)], env=env, + capture_output=True, text=True, check=False) + assert res.returncode == 0, res.stdout + res.stderr + assert "pass" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") From 4d516194661dcc64569128a55fd488ffc4415dee Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Thu, 12 Nov 2026 21:46:46 -0800 Subject: [PATCH 09/18] Address review: resolve a relative JAVA path from the caller's directory run.sh runs java after it changes into its own directory, so a JAVA given with a slash must be made absolute first; a bare command name keeps its PATH lookup. Thread: PRRT_kwDOVBg7g86274J4 Signed-off-by: Nikolay Petrov --- dokimi/formal/repo_batch/run.sh | 2 ++ dokimi/tests/test_repo_batch_run_script.py | 31 ++++++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/dokimi/formal/repo_batch/run.sh b/dokimi/formal/repo_batch/run.sh index 3252be63b..703d191b9 100755 --- a/dokimi/formal/repo_batch/run.sh +++ b/dokimi/formal/repo_batch/run.sh @@ -10,6 +10,8 @@ abspath() { case $1 in /*) printf '%s\n' "$1" ;; *) printf '%s/%s\n' "$PWD" "$1" jar=${TLA2TOOLS_JAR:?set TLA2TOOLS_JAR to tla2tools.jar (v1.8.0)} jar=$(abspath "$jar") java=${JAVA:-java} +# a bare command name stays a PATH lookup; a path with a slash is the caller's file +case $java in */*) java=$(abspath "$java") ;; esac out=$(abspath "${OUT:-$here/out}") workers=${TLC_WORKERS:-4} mkdir -p "$out" diff --git a/dokimi/tests/test_repo_batch_run_script.py b/dokimi/tests/test_repo_batch_run_script.py index 60ba0bee3..930900436 100644 --- a/dokimi/tests/test_repo_batch_run_script.py +++ b/dokimi/tests/test_repo_batch_run_script.py @@ -80,3 +80,34 @@ def test_the_script_runs_with_only_posix_tools_on_path(tmp_path): capture_output=True, text=True, check=False) assert res.returncode == 0, res.stdout + res.stderr assert "pass" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") + + +def test_a_relative_java_path_resolves_from_the_callers_directory(tmp_path): + # JAVA given relative to the caller is run after run.sh changes into its own directory: it must still be the + # caller's executable, as the jar, the cfg and OUT are + (tmp_path / "tools").mkdir() + java = _fake_java(tmp_path) + java.rename(tmp_path / "tools" / "java") + (tmp_path / "cfgs").mkdir() + shutil.copy(FIXED, tmp_path / "cfgs" / "fixed.cfg") + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": "tla2tools.jar", "OUT": "out", "JAVA": "tools/java", + "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + res = subprocess.run(["bash", str(RUN), "cfgs/fixed.cfg"], cwd=tmp_path, env=env, + capture_output=True, text=True, check=False) + assert res.returncode == 0, res.stdout + res.stderr + assert "fixed\tpass\tpass\tyes" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") + + +def test_a_bare_java_name_is_still_looked_up_on_path(tmp_path): + # a command name without a slash is not a path: it stays a PATH lookup, not a file in the caller's directory + bindir = tmp_path / "bin" + bindir.mkdir() + _fake_java(tmp_path).rename(bindir / "fake-java-bare") + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "PATH": f"{bindir}{os.pathsep}{os.environ['PATH']}", "TLA2TOOLS_JAR": "tla2tools.jar", + "OUT": "out", "JAVA": "fake-java-bare", "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + res = subprocess.run(["bash", str(RUN), str(FIXED)], cwd=tmp_path, env=env, + capture_output=True, text=True, check=False) + assert res.returncode == 0, res.stdout + res.stderr + assert "pass" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") From 452f5cd81a9cfa740d636a82f7038ea4ed710ba5 Mon Sep 17 00:00:00 2001 From: vchamarthi <123653452+vchamarthi@users.noreply.github.com> Date: Fri, 13 Nov 2026 07:17:24 -0600 Subject: [PATCH 10/18] fix(repos): refuse a non-string batch, name the whole-batch --force rerun, check TLC exit status in run.sh - refuse_mixed_executions raised TypeError on a result.json with `batch` null, a list or a number; _check_cell now raises CellFileError - the mixed-execution message named an arm-only --force rerun that check_batch_executions refuses; it names a run over every arm and model - run.sh took a verdict line from the log whatever TLC's exit status; a pass needs 0 and a violation 12 or 13 - test_ctrl_c_starts_no_queued_cell is skipped on Windows, where os.kill with SIGINT ends the process Signed-off-by: vchamarthi <123653452+vchamarthi@users.noreply.github.com> --- ...11_180000_napetrov_repo-batch-lifecycle.md | 4 +-- dokimi/docs/repo-evaluation-contract.md | 2 +- dokimi/dokimi/repos/report.py | 4 ++- dokimi/formal/repo_batch/run.sh | 10 +++++-- dokimi/tests/test_repo_batch_lifecycle.py | 4 +++ dokimi/tests/test_repo_batch_run_script.py | 30 +++++++++++++++++++ .../tests/test_repo_report_unreadable_cell.py | 14 +++++++++ 7 files changed, 61 insertions(+), 7 deletions(-) diff --git a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md index 85f591926..23446f9da 100644 --- a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md +++ b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md @@ -7,8 +7,8 @@ - **`repo report` and `repo compare` refuse an arm and model whose cells hold two executions** — a `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell), or a harness binary replaced while the batch ran, left cells of two executions that were pooled in one - row. A batch that reported before can now be refused; the message names both ids, and `--force` - on the cells of the older one clears it. `repo compare` checks only the rows it compares. + row. A batch that reported before can now be refused; the message names both ids, and a `--force` + run over every arm and model of the batch with the same `--task` and `--reps` clears it. `repo compare` checks only the rows it compares. ### Added diff --git a/dokimi/docs/repo-evaluation-contract.md b/dokimi/docs/repo-evaluation-contract.md index 08230dddf..407505f6b 100644 --- a/dokimi/docs/repo-evaluation-contract.md +++ b/dokimi/docs/repo-evaluation-contract.md @@ -2306,7 +2306,7 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric way (Ctrl-C, a crash, a failed cell), or a harness binary replaced while the batch runs, can leave finished cells of two `id`s in one arm and model; `repo report` refuses such a batch and `repo compare` such a compared row, naming - both `id`s, until `--force` reruns the cells of the older one. A plan naming one cell twice (a + both `id`s, until a `--force` run over every arm and model of the batch (the same `--task` and `--reps`) reruns them. A plan naming one cell twice (a repeated `--task` or `--model`, or two `--model` strings with one directory name, `a/b` and `a:b`) is refused before any agent starts. Ctrl-C lets the running cells finish and starts no queued one. A batch stays on the eval tree it diff --git a/dokimi/dokimi/repos/report.py b/dokimi/dokimi/repos/report.py index 5969c8a5f..c71ac0e53 100644 --- a/dokimi/dokimi/repos/report.py +++ b/dokimi/dokimi/repos/report.py @@ -176,6 +176,8 @@ def _check_cell(path: Path, rec: dict[str, Any]) -> None: for key in ("task", "arm", "model"): if not isinstance(rec.get(key), str): raise CellFileError(f"{path} has no usable `{key}`") + if "batch" in rec and not isinstance(rec["batch"], str): + raise CellFileError(f"{path} has no usable `batch`") def load_cells(batch_dir: Path) -> tuple[list[dict[str, Any]], list[str]]: @@ -209,7 +211,7 @@ def refuse_mixed_executions(cells: list[dict[str, Any]], where: str) -> None: for (batch, arm, model), ids in sorted(seen.items()): if len(ids) > 1: raise CellFileError(f"{batch or where}: the cells of arm {arm}, model {model} ran with executions " - f"{', '.join(sorted(ids))}; rerun that arm and model with --force and the batch's --task and " + f"{', '.join(sorted(ids))}; rerun every arm and model of the batch with --force and the batch's --task and " "--reps, so every cell has one execution, or use another --batch") diff --git a/dokimi/formal/repo_batch/run.sh b/dokimi/formal/repo_batch/run.sh index 703d191b9..9f3719df4 100755 --- a/dokimi/formal/repo_batch/run.sh +++ b/dokimi/formal/repo_batch/run.sh @@ -32,11 +32,15 @@ for cfg in "${cfgs[@]}"; do rc=$? set -e secs=$((SECONDS - start)) - if grep -q '^Model checking completed. No error has been found.' "$log"; then + # TLC exits 0 on a pass, 12 on a violated invariant, 13 on a violated temporal property; any other status + # is a tool error whatever the log says + if [ "$rc" -eq 0 ] && grep -q '^Model checking completed. No error has been found.' "$log"; then got=pass - elif name_v=$(sed -n 's/^Error: Invariant \([^ ]*\) is violated.*/\1/p' "$log" | tail -n 1) && [ -n "$name_v" ]; then + elif { [ "$rc" -eq 12 ] || [ "$rc" -eq 13 ]; } \ + && name_v=$(sed -n 's/^Error: Invariant \([^ ]*\) is violated.*/\1/p' "$log" | tail -n 1) && [ -n "$name_v" ]; then got="violation $name_v" - elif name_v=$(sed -n 's/^Error: Temporal property \([^ ]*\) was violated.*/\1/p' "$log" | tail -n 1) \ + elif { [ "$rc" -eq 12 ] || [ "$rc" -eq 13 ]; } \ + && name_v=$(sed -n 's/^Error: Temporal property \([^ ]*\) was violated.*/\1/p' "$log" | tail -n 1) \ && [ -n "$name_v" ]; then got="violation $name_v" else diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index ce5cddb20..6d4ec95c0 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -84,6 +84,7 @@ def test_names_that_differ_only_in_case_are_refused_before_any_agent(setup, caps assert not _agents(setup) +@pytest.mark.skipif(os.name == "nt", reason="os.kill with SIGINT terminates the process on Windows") def test_ctrl_c_starts_no_queued_cell(setup, monkeypatch): # CancelContract of cfg/fixed.cfg (cfg/mut_no_cancel_guard.cfg breaks it): SIGINT wakes the main thread and # pool.map cancels the queued cells; _thread.interrupt_main() sends no signal and would let them start. @@ -187,6 +188,9 @@ def test_the_mixed_execution_refusal_is_per_batch_arm_and_model(): refuse_mixed_executions([*ok, _cell("a", "m", "e4")], "b1") with pytest.raises(CellFileError, match="e1, unrecorded"): refuse_mixed_executions([_cell("a", "m", "e1"), {"arm": "a", "model": "m"}], "b1") + # the remedy is a --force run over the whole batch: an arm-only rerun is refused while another arm holds the older id + with pytest.raises(CellFileError, match="rerun every arm and model of the batch with --force"): + refuse_mixed_executions([_cell("a", "m", "e1"), _cell("a", "m", "e2")], "b1") def test_compare_refuses_only_a_compared_row_of_two_executions(setup): diff --git a/dokimi/tests/test_repo_batch_run_script.py b/dokimi/tests/test_repo_batch_run_script.py index 930900436..7a6990d87 100644 --- a/dokimi/tests/test_repo_batch_run_script.py +++ b/dokimi/tests/test_repo_batch_run_script.py @@ -39,6 +39,15 @@ sys.exit(1) """ +# prints a verdict line, then exits with the status in FAKE_TLC_RC +FAKE_TLC_STATUS = f"""#!{sys.executable} -I +import os +import sys + +print(os.environ["FAKE_TLC_OUT"]) +sys.exit(int(os.environ["FAKE_TLC_RC"])) +""" + def _fake_java(tmp_path: Path) -> Path: java = tmp_path / "fake-java" @@ -111,3 +120,24 @@ def test_a_bare_java_name_is_still_looked_up_on_path(tmp_path): capture_output=True, text=True, check=False) assert res.returncode == 0, res.stdout + res.stderr assert "pass" in (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8") + + +@pytest.mark.parametrize("out, rc, cfg, got, exit_code", [ + ("Model checking completed. No error has been found.", 1, "fixed", "error rc=1", 1), + ("Error: Invariant CancelContract is violated.", 1, "mut_no_cancel_guard", "error rc=1", 1), + ("Error: Temporal property InvocationEnds was violated.", 1, "no_fairness", "error rc=1", 1), + ("Error: Invariant CancelContract is violated.", 12, "mut_no_cancel_guard", "violation CancelContract", 0), + ("Error: Temporal property InvocationEnds was violated.", 13, "no_fairness", "violation InvocationEnds", 0), +], ids=["pass-then-failure", "invariant-then-failure", "temporal-then-failure", "invariant-12", "temporal-13"]) +def test_a_verdict_in_the_log_counts_only_with_the_status_tlc_gives_it(tmp_path, out, rc, cfg, got, exit_code): + java = tmp_path / "fake-java" + java.write_text(FAKE_TLC_STATUS, encoding="utf-8") + java.chmod(0o755) + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": str(tmp_path / "tla2tools.jar"), "OUT": str(tmp_path / "out"), + "JAVA": str(java), "FAKE_TLC_OUT": out, "FAKE_TLC_RC": str(rc)} + res = subprocess.run(["bash", str(RUN), str(FIXED.with_name(f"{cfg}.cfg"))], env=env, + capture_output=True, text=True, check=False) + row = (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8").splitlines()[1].split("\t") + assert row[2] == got, res.stdout + res.stderr + assert res.returncode == exit_code, res.stdout + res.stderr diff --git a/dokimi/tests/test_repo_report_unreadable_cell.py b/dokimi/tests/test_repo_report_unreadable_cell.py index f1ce4714c..a33103ed5 100644 --- a/dokimi/tests/test_repo_report_unreadable_cell.py +++ b/dokimi/tests/test_repo_report_unreadable_cell.py @@ -436,3 +436,17 @@ def test_compare_with_a_baseline_no_cell_matches_exits_2_naming_it(tmp_path, cap _run("compare", str(batch), "--baseline", "nosucharm") assert exc.code == 2 assert "no finished cell matches the baseline 'nosucharm'" in capsys.readouterr().err + + +@pytest.mark.parametrize("batch_value", [None, [], 3], ids=["null", "list", "number"]) +@pytest.mark.parametrize("argv", [("report",), ("compare", "--baseline", "a")], ids=["report", "compare"]) +def test_a_result_file_with_a_batch_that_is_not_a_string_exits_2(tmp_path, capsys, argv, batch_value): + files = {"t__a__m__r1/result.json": json.dumps({**_GOOD, "batch": batch_value}).encode(), + "t__a__m__r2/result.json": json.dumps({**_GOOD, "batch": "b1"}).encode()} + batch = _batch(tmp_path, "b1", files) + with refusal() as exc: + _run(argv[0], str(batch), *argv[1:]) + assert exc.code == 2 + err = capsys.readouterr().err + assert f"{batch / 't__a__m__r1' / 'result.json'} has no usable `batch`" in err + assert "Traceback" not in err From 0f3a601a1dc7f430420eefb571c116a2973ac20a Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:28:40 -0800 Subject: [PATCH 11/18] test(repos): pin the --model narrowing and the refusal's remedy text A mixed arm of one model must not refuse a compare that selects another model, and the refusal names the --task and --reps of the remedy. Thread: PRRT_kwDOVBg7g863ez0W Thread: PRRT_kwDOVBg7g863ez0a Signed-off-by: Nikolay Petrov --- dokimi/tests/test_repo_batch_lifecycle.py | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index 6d4ec95c0..c19e0f572 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -189,7 +189,8 @@ def test_the_mixed_execution_refusal_is_per_batch_arm_and_model(): with pytest.raises(CellFileError, match="e1, unrecorded"): refuse_mixed_executions([_cell("a", "m", "e1"), {"arm": "a", "model": "m"}], "b1") # the remedy is a --force run over the whole batch: an arm-only rerun is refused while another arm holds the older id - with pytest.raises(CellFileError, match="rerun every arm and model of the batch with --force"): + with pytest.raises(CellFileError, match="rerun every arm and model of the batch with --force and " + "the batch's --task and --reps"): refuse_mixed_executions([_cell("a", "m", "e1"), _cell("a", "m", "e2")], "b1") @@ -203,3 +204,18 @@ def test_compare_refuses_only_a_compared_row_of_two_executions(setup): with pytest.raises(CellFileError, match="arm guidance:bridge, model m-1 ran with executions"): compare([b1], "guidance:none", ["guidance:bridge"]) assert compare([b1], "guidance:none", ["guidance:raw"])["comparisons"] # the mixed arm is not compared + + +def test_compare_with_a_model_refuses_only_a_mixed_row_of_that_model(setup): + # m-2 alone has the mixed arm: --model m-1 compares rows that are not mixed, so it must not be refused + _run(setup, "--task", "fix_add", "--arm", "guidance:none,guidance:bridge", "--reps", "2", models=("m-1", "m-2")) + b1 = setup["out"] / "b1" + target = b1 / "fix_add__guidance-bridge__m-2__r1/result.json" + rec = json.loads(target.read_text()) + rec["execution"]["id"] = "old" + target.write_text(json.dumps(rec)) + assert compare([b1], "guidance:none", ["guidance:bridge"], models=["m-1"])["comparisons"] + with pytest.raises(CellFileError, match="arm guidance:bridge, model m-2 ran with executions"): + compare([b1], "guidance:none", ["guidance:bridge"], models=["m-2"]) + with pytest.raises(CellFileError, match="arm guidance:bridge, model m-2 ran with executions"): + compare([b1], "guidance:none", ["guidance:bridge"]) From 2691411540ebca5028bb6f838940075ea2521915 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:28:40 -0800 Subject: [PATCH 12/18] test(formal): pin run.sh's verdict, exit status and paths Covers the mutants the fake-java tests let through: a pass line with status 12, exit 0 without the completion line, the last violation named, invariant status 13, a failing cfg before a passing one, a cfg with no EXPECT line, and a relative OUT for TLC's -metadir. Thread: PRRT_kwDOVBg7g863ez0b Signed-off-by: Nikolay Petrov --- dokimi/tests/test_repo_batch_run_script.py | 69 +++++++++++++++++++++- 1 file changed, 68 insertions(+), 1 deletion(-) diff --git a/dokimi/tests/test_repo_batch_run_script.py b/dokimi/tests/test_repo_batch_run_script.py index 7a6990d87..a2bf149d0 100644 --- a/dokimi/tests/test_repo_batch_run_script.py +++ b/dokimi/tests/test_repo_batch_run_script.py @@ -128,7 +128,13 @@ def test_a_bare_java_name_is_still_looked_up_on_path(tmp_path): ("Error: Temporal property InvocationEnds was violated.", 1, "no_fairness", "error rc=1", 1), ("Error: Invariant CancelContract is violated.", 12, "mut_no_cancel_guard", "violation CancelContract", 0), ("Error: Temporal property InvocationEnds was violated.", 13, "no_fairness", "violation InvocationEnds", 0), -], ids=["pass-then-failure", "invariant-then-failure", "temporal-then-failure", "invariant-12", "temporal-13"]) + ("Model checking completed. No error has been found.", 12, "fixed", "error rc=12", 1), + ("Usage: java -cp tla2tools.jar tlc2.TLC", 0, "fixed", "error rc=0", 1), + ("Error: Invariant CancelContract is violated.", 13, "mut_no_cancel_guard", "violation CancelContract", 0), + ("Error: Invariant First is violated.\nError: Invariant Second is violated.", 12, "mut_no_cancel_guard", + "violation Second", 1), # the last violation named wins; this cfg expects CancelContract, so the run fails +], ids=["pass-then-failure", "invariant-then-failure", "temporal-then-failure", "invariant-12", "temporal-13", + "pass-line-with-status-12", "completion-line-missing-status-0", "invariant-13", "last-named-violation"]) def test_a_verdict_in_the_log_counts_only_with_the_status_tlc_gives_it(tmp_path, out, rc, cfg, got, exit_code): java = tmp_path / "fake-java" java.write_text(FAKE_TLC_STATUS, encoding="utf-8") @@ -141,3 +147,64 @@ def test_a_verdict_in_the_log_counts_only_with_the_status_tlc_gives_it(tmp_path, row = (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8").splitlines()[1].split("\t") assert row[2] == got, res.stdout + res.stderr assert res.returncode == exit_code, res.stdout + res.stderr + + +FAKE_TLC_BY_CFG = f"""#!{sys.executable} -I +import os +import sys + +cfg = sys.argv[sys.argv.index("-config") + 1] +if os.path.basename(cfg).startswith("bad"): + print("Error: no such file") + sys.exit(1) +print("Model checking completed. No error has been found.") +sys.exit(0) +""" + + +def test_a_failing_cfg_fails_the_run_whichever_cfg_comes_after_it(tmp_path): + # a failing cfg followed by a passing one must still exit 1: the failure flag is not reset per cfg + java = tmp_path / "fake-java" + java.write_text(FAKE_TLC_BY_CFG, encoding="utf-8") + java.chmod(0o755) + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + for name in ("bad", "good"): + shutil.copy(FIXED, tmp_path / f"{name}.cfg") + env = {**os.environ, "TLA2TOOLS_JAR": str(tmp_path / "tla2tools.jar"), "OUT": str(tmp_path / "out"), + "JAVA": str(java)} + res = subprocess.run(["bash", str(RUN), str(tmp_path / "bad.cfg"), str(tmp_path / "good.cfg")], env=env, + capture_output=True, text=True, check=False) + rows = {r.split("\t")[0]: r.split("\t") for r in + (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8").splitlines()[1:]} + assert rows["bad"][3] == "NO" and rows["good"][3] == "yes", res.stdout + res.stderr + assert res.returncode == 1, res.stdout + res.stderr + + +def test_a_cfg_without_an_expect_line_is_not_ok(tmp_path): + # no EXPECT line gives no expected verdict: the cfg is not ok, even when TLC passes it + java = tmp_path / "fake-java" + java.write_text(FAKE_TLC_STATUS, encoding="utf-8") + java.chmod(0o755) + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + cfg = tmp_path / "noexpect.cfg" + cfg.write_text("".join(line for line in FIXED.read_text(encoding="utf-8").splitlines(True) + if "EXPECT:" not in line), encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": str(tmp_path / "tla2tools.jar"), "OUT": str(tmp_path / "out"), + "JAVA": str(java), "FAKE_TLC_OUT": "Model checking completed. No error has been found.", + "FAKE_TLC_RC": "0"} + res = subprocess.run(["bash", str(RUN), str(cfg)], env=env, capture_output=True, text=True, check=False) + row = (tmp_path / "out" / "summary.tsv").read_text(encoding="utf-8").splitlines()[1].split("\t") + assert row[3] == "NO", res.stdout + res.stderr + assert res.returncode == 1, res.stdout + res.stderr + + +def test_a_relative_out_is_made_absolute_for_the_tlc_metadir(tmp_path): + # the fake records its arguments: TLC's -metadir must be under the caller's OUT, not relative to run.sh's directory + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": "tla2tools.jar", "OUT": "out", "JAVA": str(_fake_java(tmp_path)), + "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + res = subprocess.run(["bash", str(RUN), str(FIXED)], cwd=tmp_path, env=env, capture_output=True, text=True, + check=False) + assert res.returncode == 0, res.stdout + res.stderr + args = (tmp_path / "tlc.log").read_text(encoding="utf-8") + assert str((tmp_path / "out" / "states" / "fixed").resolve()) in args From d1a5e536fb69d2ce6cfda1c78df03908d76217cc Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:28:40 -0800 Subject: [PATCH 13/18] docs: name the case-only refusal in the changelog and the contract Thread: PRRT_kwDOVBg7g863ez0d Signed-off-by: Nikolay Petrov --- .../20261111_180000_napetrov_repo-batch-lifecycle.md | 2 +- dokimi/docs/repo-evaluation-contract.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md index 23446f9da..bc4baee78 100644 --- a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md +++ b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md @@ -1,7 +1,7 @@ ### Fixed - **`repo run` refuses a plan that names one cell twice** — a repeated `--task` or `--model`, or two - `--model` strings with one directory name (`a/b` and `a:b`), put two runs in one cell directory; + `--model` strings with one directory name (`a/b` and `a:b`), or names that differ only in case, put two runs in one cell directory; with `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's `meta.json` and answer. The run now stops before any agent starts, naming the cell. - **`repo report` and `repo compare` refuse an arm and model whose cells hold two executions** — a diff --git a/dokimi/docs/repo-evaluation-contract.md b/dokimi/docs/repo-evaluation-contract.md index 36410aea8..ca59dcd05 100644 --- a/dokimi/docs/repo-evaluation-contract.md +++ b/dokimi/docs/repo-evaluation-contract.md @@ -2315,7 +2315,7 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric report` refuses such a batch and `repo compare` such a compared row, naming both `id`s, until a `--force` run over every arm and model of the batch (the same `--task` and `--reps`) reruns them. A plan naming one cell twice (a repeated `--task` or `--model`, or two `--model` strings with one directory - name, `a/b` and `a:b`) is refused before any agent starts. Ctrl-C lets the + name, `a/b` and `a:b`, or names that differ only in case) is refused before any agent starts. Ctrl-C lets the running cells finish and starts no queued one. A batch stays on the eval tree it started with: its revision, or for a working tree the digests of its `eval_dir` and of the image build context. A batch with a task that From 188e2cfc41d0a5b7c5009acecac23f9c6c5de18f Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:28:40 -0800 Subject: [PATCH 14/18] Address review: run.sh exit status check, already fixed The verdict and the exit status are checked together in run.sh (452f5cd81), covered by test_a_verdict_in_the_log_counts_only_with_the_status_tlc_gives_it. Thread: PRRT_kwDOVBg7g863Bfz3: already fixed in 452f5cd81 Signed-off-by: Nikolay Petrov From a24c429bb5957c5d95e8c692caf8f40bc26403b8 Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:30:45 -0800 Subject: [PATCH 15/18] Address review: answer the reviews and comments of 0fa65be to 452f5cd The findings these reviews and comments name are fixed on this branch; the one open question, where the evaluator proposal lives, is held. Thread: PRR_kwDOVBg7g88AAAABXs_Lvw: already fixed in 452f5cd81 Thread: PRR_kwDOVBg7g88AAAABXxLu2A: already fixed in 452f5cd81 Thread: IC_kwDOVBg7g88AAAABmY9fAw: already fixed in 452f5cd81 Thread: PRR_kwDOVBg7g88AAAABX_VGsw: fixed in the commits that name its threads Signed-off-by: Nikolay Petrov From 2130ad51a52b0f6857be04ff9bd441c9acd3e09f Mon Sep 17 00:00:00 2001 From: Nikolay Petrov Date: Sat, 14 Nov 2026 11:32:15 -0800 Subject: [PATCH 16/18] docs: say which case-only names are refused Names that differ only in case are refused on every system, since they share one directory on a case-insensitive volume. Thread: PRRT_kwDOVBg7g863ez0d Signed-off-by: Nikolay Petrov --- .../20261111_180000_napetrov_repo-batch-lifecycle.md | 8 +++++--- dokimi/docs/repo-evaluation-contract.md | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md index bc4baee78..2ad8bf370 100644 --- a/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md +++ b/dokimi/changelog.d/20261111_180000_napetrov_repo-batch-lifecycle.md @@ -1,9 +1,11 @@ ### Fixed - **`repo run` refuses a plan that names one cell twice** — a repeated `--task` or `--model`, or two - `--model` strings with one directory name (`a/b` and `a:b`), or names that differ only in case, put two runs in one cell directory; - with `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's - `meta.json` and answer. The run now stops before any agent starts, naming the cell. + names that share one cell directory (`a/b` and `a:b`), put two runs in one cell directory; with + `--jobs 2` each removed the other's files and `result.json` sat beside the other attempt's + `meta.json` and answer. The run now stops before any agent starts, naming the cell. Names that + differ only in case are refused on every system, since they share one directory on a + case-insensitive volume. - **`repo report` and `repo compare` refuse an arm and model whose cells hold two executions** — a `--force` run with another execution that stopped part way (Ctrl-C, a crash, a failed cell), or a harness binary replaced while the batch ran, left cells of two executions that were pooled in one diff --git a/dokimi/docs/repo-evaluation-contract.md b/dokimi/docs/repo-evaluation-contract.md index ca59dcd05..f0a6c2794 100644 --- a/dokimi/docs/repo-evaluation-contract.md +++ b/dokimi/docs/repo-evaluation-contract.md @@ -2315,8 +2315,8 @@ python cli.py repo compare repo-runs/authoring --baseline guidance:none --metric report` refuses such a batch and `repo compare` such a compared row, naming both `id`s, until a `--force` run over every arm and model of the batch (the same `--task` and `--reps`) reruns them. A plan naming one cell twice (a repeated `--task` or `--model`, or two `--model` strings with one directory - name, `a/b` and `a:b`, or names that differ only in case) is refused before any agent starts. Ctrl-C lets the - running cells finish and starts no queued one. A batch stays on the eval tree it + name, `a/b` and `a:b`, or names that differ only in case) is refused before any agent starts. + Ctrl-C lets the running cells finish and starts no queued one. A batch stays on the eval tree it started with: its revision, or for a working tree the digests of its `eval_dir` and of the image build context. A batch with a task that names a `dokimi:` grader (or a task directory that cannot be read) also stays on the built-in graders' sources. From 18e2755160fb5160fac0719629c665a9dc604489 Mon Sep 17 00:00:00 2001 From: Anton Volkov Date: Sat, 14 Nov 2026 21:42:08 +0000 Subject: [PATCH 17/18] run.sh: refuse two cfgs with the same basename Signed-off-by: Anton Volkov --- dokimi/formal/repo_batch/run.sh | 7 +++++++ dokimi/tests/test_repo_batch_run_script.py | 15 +++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/dokimi/formal/repo_batch/run.sh b/dokimi/formal/repo_batch/run.sh index 9f3719df4..329a72671 100755 --- a/dokimi/formal/repo_batch/run.sh +++ b/dokimi/formal/repo_batch/run.sh @@ -21,6 +21,13 @@ fail=0 [ $# -gt 0 ] || set -- "$here"/cfg/*.cfg cfgs=() for cfg in "$@"; do cfgs+=("$(abspath "$cfg")"); done +# two cfgs with one basename would share a log and a metadir: refuse before any check runs +seen=$'\n' +for cfg in "${cfgs[@]}"; do + name=$(basename "$cfg" .cfg) + case $seen in *$'\n'"$name"$'\n'*) echo "run.sh: two cfgs are named $name.cfg; their log and states would collide" >&2; exit 2 ;; esac + seen="$seen$name"$'\n' +done for cfg in "${cfgs[@]}"; do name=$(basename "$cfg" .cfg) expect=$(sed -n 's/^\\\* EXPECT: //p' "$cfg") diff --git a/dokimi/tests/test_repo_batch_run_script.py b/dokimi/tests/test_repo_batch_run_script.py index a2bf149d0..cf24f23ee 100644 --- a/dokimi/tests/test_repo_batch_run_script.py +++ b/dokimi/tests/test_repo_batch_run_script.py @@ -180,6 +180,21 @@ def test_a_failing_cfg_fails_the_run_whichever_cfg_comes_after_it(tmp_path): assert res.returncode == 1, res.stdout + res.stderr +def test_two_cfgs_with_one_basename_are_refused_before_any_run(tmp_path): + # both would write out/.log and share one -metadir: exit 2, name the cfg, run nothing + for sub in ("before", "after"): + (tmp_path / sub).mkdir() + shutil.copy(FIXED, tmp_path / sub / "fixed.cfg") + (tmp_path / "tla2tools.jar").write_text("", encoding="utf-8") + env = {**os.environ, "TLA2TOOLS_JAR": str(tmp_path / "tla2tools.jar"), "OUT": str(tmp_path / "out"), + "JAVA": str(_fake_java(tmp_path)), "FAKE_TLC_LOG": str(tmp_path / "tlc.log")} + cfgs = [str(tmp_path / "before" / "fixed.cfg"), str(tmp_path / "after" / "fixed.cfg")] + res = subprocess.run(["bash", str(RUN), *cfgs], env=env, capture_output=True, text=True, check=False) + assert res.returncode == 2, res.stdout + res.stderr + assert "fixed.cfg" in res.stderr + assert not (tmp_path / "tlc.log").exists() + + def test_a_cfg_without_an_expect_line_is_not_ok(tmp_path): # no EXPECT line gives no expected verdict: the cfg is not ok, even when TLC passes it java = tmp_path / "fake-java" From 370be678369f4e8329f406335f8b3e669d72acde Mon Sep 17 00:00:00 2001 From: vchamarthi <123653452+vchamarthi@users.noreply.github.com> Date: Sat, 14 Nov 2026 16:14:54 -0600 Subject: [PATCH 18/18] fix(repos): cancel queued cells on Ctrl-C during submission An interrupt raised while pool.map was still submitting cells let the queued cells start, because the pool exit waited without cancelling them. The pool now cancels its pending futures on KeyboardInterrupt. Signed-off-by: vchamarthi <123653452+vchamarthi@users.noreply.github.com> --- dokimi/dokimi/repos/runner.py | 16 +++++++++++--- dokimi/tests/test_repo_batch_lifecycle.py | 27 +++++++++++++++++++++++ 2 files changed, 40 insertions(+), 3 deletions(-) diff --git a/dokimi/dokimi/repos/runner.py b/dokimi/dokimi/repos/runner.py index 241ea5717..87937f988 100644 --- a/dokimi/dokimi/repos/runner.py +++ b/dokimi/dokimi/repos/runner.py @@ -41,7 +41,7 @@ import threading import uuid from collections import Counter -from collections.abc import Iterator +from collections.abc import Callable, Iterator from concurrent.futures import ThreadPoolExecutor from dataclasses import dataclass from pathlib import Path @@ -430,14 +430,24 @@ def one(cell: tuple[Task, str, AgentOptions, int]) -> None: state["spent"] += rec["agent"].get("charged_usd", rec["agent"]["cost_usd"]) or 0.0 _log_cell(log, name, rec) - with ThreadPoolExecutor(max(1, jobs)) as pool: - list(pool.map(one, cells)) + _map_cells(one, cells, jobs) return {"cells": len(cells), "ran": state["ran"], "skipped": state["skipped"], "errors": state["errors"], "budget_stopped": state["budget_stopped"], "unsupported": state["unsupported"], "unsupported_tasks": unsupported, "probe_failed": probe_failed, "spent_usd": round(state["spent"], 6)} +def _map_cells(one: Callable[[Any], None], cells: list[Any], jobs: int) -> None: + with ThreadPoolExecutor(max(1, jobs)) as pool: + try: + list(pool.map(one, cells)) + except KeyboardInterrupt: + # pool.map submits every cell before it returns the iterator that cancels the queue, so an + # interrupt during submission would otherwise let the queued cells start while the pool exits. + pool.shutdown(wait=False, cancel_futures=True) + raise + + def _refuse_shared_cells(cells: list[tuple[Task, str, AgentOptions, int]]) -> None: """Refuse a plan naming one cell directory twice, or two names one case-insensitive volume maps to one directory: with --jobs 2 both would run in it and mix their files (or one would delete the other's).""" diff --git a/dokimi/tests/test_repo_batch_lifecycle.py b/dokimi/tests/test_repo_batch_lifecycle.py index c19e0f572..cea72ee5b 100644 --- a/dokimi/tests/test_repo_batch_lifecycle.py +++ b/dokimi/tests/test_repo_batch_lifecycle.py @@ -120,6 +120,33 @@ def run_cell(ctx, task, arm, rep, *args, **kwargs): assert summary["missing"] == [f"fix_add__guidance-raw__m-1__r{r}" for r in (3, 4, 5)] +def test_an_interrupt_during_submission_starts_no_queued_cell(setup, monkeypatch): + # Ctrl-C lands in the main thread while pool.map is still submitting: the queued cells must not start. + started = [] + calls = [] + real = repo_runner.run_cell + real_submit = repo_runner.ThreadPoolExecutor.submit + + def submit(self, fn, *a, **k): + calls.append(1) + if len(calls) == 4: + time.sleep(0.2) + raise KeyboardInterrupt + return real_submit(self, fn, *a, **k) + + def run_cell(ctx, task, arm, rep, *args, **kwargs): + started.append(rep) + time.sleep(0.5) # both workers busy, cell 3 queued + return real(ctx, task, arm, rep, *args, **kwargs) + + monkeypatch.setattr(repo_runner, "run_cell", run_cell) + monkeypatch.setattr(repo_runner.ThreadPoolExecutor, "submit", submit) + with pytest.raises(KeyboardInterrupt): + _run(setup, "--task", "fix_add", "--reps", "5", "--jobs", "2") + time.sleep(1) + assert sorted(started) == [1, 2] + + def test_a_force_run_stopped_part_way_does_not_pool_two_executions(setup, monkeypatch, capsys): # cfg/code_main_force_crash.cfg: --force with another execution replaced r1, then stopped; r2 kept the old # execution and `repo report` pooled both in one row.