Conversation
…l counterexample Per B-0179 verify-then-claim sweep. Re-running TLC on SpineAsyncProtocol revealed: TLC reports "Deadlock reached" at the all-done quiescent state (processed=NumBatches, channel empty, both PCs idle). This is intended termination, not bug-deadlock. Local TLC run before fix: Error: Deadlock reached. 21 states generated, 15 distinct states found, 0 states left on queue. Depth 9. The 3 invariants (InvMonotonic, InvEventuallyDrains, InvFlushTerminates) all hold across all 15 explored states. The ONLY violation is the deadlock-at-terminal warning. Fix: add CHECK_DEADLOCK FALSE to SpineAsyncProtocol.cfg (same pattern as CircuitRegistration.cfg + TwoPCSink.cfg + several others). Tells TLC that reaching quiescence is acceptable for bounded protocols. Local verification: Model checking completed. No error has been found. 21 states generated, 15 distinct states found, 0 states left on queue. Added [Fact] entry registering SpineAsyncProtocol in TLC test list. Closes B-0179 P2 backlog row. B1 progress: 3 of 4 deferred specs now in CI (DbspSpec via #1397, CircuitRegistration via #1401, SpineAsyncProtocol via this PR). Remaining: B-0181 SpineMergeInvariants (depth-17 trace; substantial counterexample investigation possibly indicating real bug).
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
Pull request overview
Registers SpineAsyncProtocol as a passing TLC-checked spec by disabling TLC’s default deadlock detection for its intended terminal quiescent state, aligning it with other bounded/terminating specs in the repo.
Changes:
- Set
CHECK_DEADLOCK FALSEintools/tla/specs/SpineAsyncProtocol.cfgto avoid treating the intended terminal state as a deadlock. - Added an xUnit
[<Fact>]to run TLC forSpineAsyncProtocolvia the existingassertSpecValidtest harness.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| tools/tla/specs/SpineAsyncProtocol.cfg | Disables TLC deadlock detection for the spec’s intended terminal quiescent state. |
| tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs | Adds a TLC validation test case for SpineAsyncProtocol. |
…s, not temporal liveness Reviewer #1411 caught: my comment described the 3 invariants as if they were temporal-liveness properties (eventually-drains, flush-terminates), but the actual TLC-checked predicates are state invariants. The 'eventually' / 'terminates' naming is historical from the spec author's intent comments — the actual predicates are conditional state assertions (when channel empty, processed = sent at that instant). Updated comment to: - Mark them explicitly as STATE invariants - Describe each predicate's actual TLC-checkable form - Note that real liveness would require LTL properties + WF/SF fairness assumptions (not what this spec does) This is the documentation-is-current-state-not-history rule applied to comment-vs-implementation alignment: comments must describe what TLC actually checks, not what the spec author labeled the property in their intent.
4 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…run-tlc.ts
Per Aaron 2026-05-03 "another one bites the dust > ts" (also B-0183
backlog row): the F# Tlc.Runner.Tests.fs is really an xunit wrapper
around shelling to TLC — no F# operator-algebra logic involved. This
TS wrapper is the natural shape.
Three modes:
- `bun tools/formal-verification/run-tlc.ts <SpecName>`
Runs TLC on tools/tla/specs/<SpecName>.tla with the matching .cfg.
Exit 0 on "Model checking completed. No error has been found.";
exit 1 on TLC error / invariant violation / etc.; exit 2 if
toolchain not ready.
- `bun tools/formal-verification/run-tlc.ts --all`
Runs the curated CATALOGUE (matches F# Tlc.Runner.Tests.fs
registration) and aggregates pass/fail/skip counts. Exit 0 only
if all pass.
- `bun tools/formal-verification/run-tlc.ts --check-toolchain`
Useful for CI gating + dev-local diagnostics. Exit 0/2.
Local verification:
- --check-toolchain → OK (java + tla2tools.jar present)
- SmokeCheck → OK
- DbspSpec → OK (1M states / ~11s)
- --all on this branch → 10/11 pass; SpineAsyncProtocol fails
because #1411 (CHECK_DEADLOCK FALSE fix) not yet on main this
branch was forked from. Once #1411 merges + this branch rebases,
expected: 11/11 pass.
- Total wall time for --all: 16s (faster than dotnet test
overhead alone).
Trace cleanup matches F# version: <SpecName>_TTrace_*.tla, *.bin,
MC*.tla. Working directory set to specs/ so TLC's file resolution
finds module + cfg without absolute paths.
Phase 2 (next PR) wires this into a Linux-only CI workflow.
Phase 3 retires Tlc.Runner.Tests.fs after parity verification across
N PRs (per B-0183).
Composes with B-0182 (the F# 3-axis filter; tactical band-aid until
this TS migration completes — Phase 3 removes that filter as
vestigial).
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…run-tlc.ts (#1412) * feat(B-0183 Phase 1): TS wrapper for TLC — tools/formal-verification/run-tlc.ts Per Aaron 2026-05-03 "another one bites the dust > ts" (also B-0183 backlog row): the F# Tlc.Runner.Tests.fs is really an xunit wrapper around shelling to TLC — no F# operator-algebra logic involved. This TS wrapper is the natural shape. Three modes: - `bun tools/formal-verification/run-tlc.ts <SpecName>` Runs TLC on tools/tla/specs/<SpecName>.tla with the matching .cfg. Exit 0 on "Model checking completed. No error has been found."; exit 1 on TLC error / invariant violation / etc.; exit 2 if toolchain not ready. - `bun tools/formal-verification/run-tlc.ts --all` Runs the curated CATALOGUE (matches F# Tlc.Runner.Tests.fs registration) and aggregates pass/fail/skip counts. Exit 0 only if all pass. - `bun tools/formal-verification/run-tlc.ts --check-toolchain` Useful for CI gating + dev-local diagnostics. Exit 0/2. Local verification: - --check-toolchain → OK (java + tla2tools.jar present) - SmokeCheck → OK - DbspSpec → OK (1M states / ~11s) - --all on this branch → 10/11 pass; SpineAsyncProtocol fails because #1411 (CHECK_DEADLOCK FALSE fix) not yet on main this branch was forked from. Once #1411 merges + this branch rebases, expected: 11/11 pass. - Total wall time for --all: 16s (faster than dotnet test overhead alone). Trace cleanup matches F# version: <SpecName>_TTrace_*.tla, *.bin, MC*.tla. Working directory set to specs/ so TLC's file resolution finds module + cfg without absolute paths. Phase 2 (next PR) wires this into a Linux-only CI workflow. Phase 3 retires Tlc.Runner.Tests.fs after parity verification across N PRs (per B-0183). Composes with B-0182 (the F# 3-axis filter; tactical band-aid until this TS migration completes — Phase 3 removes that filter as vestigial). * fix(run-tlc.ts): address 6 #1412 review findings + tighten typing per Aaron 2026-05-03 P0 fixes (security + correctness): - Regex injection: cleanupTraceFiles now escapes specName before embedding in RegExp constructor. Added escapeRegex() helper. Without this, a specName containing regex metacharacters could cause unintended file deletion under tools/tla/specs. - Exit code orthogonality: was using exit 2 for both "toolchain not ready" AND "unknown flag". Split: 2 = toolchain; 3 = argument/usage error. Documented in header doc. P1 fixes (correctness + portability): - which() now uses in-process PATH-scan (no /usr/bin/env which shell-out). Matches F# Tlc.Runner.Tests.fs's pattern; portable to Windows + minimal images that lack /usr/bin/env which. - runAll() treats missing-from-catalogue specs as failures (NOT silent skips). Matches the documented contract "exit 0 only if all pass" and gates against catalogue drift. - Removed unused readFileSync import (tsc lint failure). P2 fixes (DX): - runAll() now prints failure stdout-tail (last 30 lines) per failed spec + a "rerun with: bun ... <SpecName>" hint. Saves CI triage from re-invoking with --one. Aaron 2026-05-03 meta-feedback: "we want to be strongly typed to a large degree in ts it verifies your assumptions more at lint time". Tightened ExitCode union to include 3; orthogonal exit-code contract documented. Future TS authoring should default to strong types. Local verification: --all passes 11/11 specs in ~16s wall. Regex-injection fix verified by passing Spec.With.Dots — now returns "ERROR: ... not found" instead of regex-matching unrelated files.
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes B-0179. The "depth-9 TTrace dump" surfaced by the verify-then-claim sweep on #1397 was NOT a real counterexample — TLC reports "Deadlock reached" at the all-done quiescent state (processed=NumBatches=4, channel empty, both PCs idle). That's intended termination for a bounded protocol, not bug-deadlock.
Analysis
Fix
Added
CHECK_DEADLOCK FALSEtoSpineAsyncProtocol.cfg. Same pattern asCircuitRegistration.cfg+TwoPCSink.cfg(bounded protocols that correctly terminate).Local verification (post-fix)
dotnet test --filter SpineAsyncProtocolpasses in 1.7s.B1 progress
3 of 4 deferred specs now in CI:
Test plan
🤖 Generated with Claude Code