perf(tla): cache the compiled IR in the action-call guard path - #189
Merged
Conversation
`try_eval_compiled_guard_as_action` recompiled the resolved action's IR (`compile_action_ir` + `CompiledActionIr::from_ir` + `compile_expr`/`lower`) on EVERY guard evaluation. This guard is on the hot path — each `\E`-quantified disjunct of a Next disjunction (e.g. ACP's `\E i,j : parDie(i) \/ parProgNB(i,j)`) resolves through it — so a fairness spec that re-explores the state graph during trace reconstruction spun for minutes re-compiling `parProg`/`decideOnForward`/`abortOnTimeout` on every re-visited state (gdb showed 4+ worker threads deep in `from_ir`/`compile_expr`/`lower` under `reconstruct_trace_limited`). Reuse the existing thread-local/prewarmed `get_or_compile_action` cache instead. ACP_NB_WRONG_TLC now completes in ~143s (previously stalled past 300s in trace reconstruction) with the same verdict (AC1 violated). Gate: diff_tlc 19/19, cargo test --release clean (the lone `prop_pause_visibility` blip is the known flaky checkpoint-concurrency proptest — passes in isolation). Pure caching change; no behavior difference.
zoratu
added a commit
that referenced
this pull request
Jul 20, 2026
`split_action_body_clauses` and `split_action_body_disjuncts` (action_ir.rs) are pure functions of their input text — the v2 layout-aware parse is deterministic and `v2_enabled()` is fixed per process — but they are re-invoked on the SAME action/clause text on every `next_states` call. During full-space exploration, and especially trace reconstruction (which re-explores the whole graph), re-running the Pratt parse + string scans per visit dominated the hot path for fairness/reconstruction specs once #189 removed the compiled-IR recompilation (gdb showed `split_action_body_clauses`/`split_top_level`/`matches_keyword_at`). Wrap each splitter as an `_uncached` inner fn behind a thread-local memoization keyed by the input string (returns a cheap `Vec<String>` clone instead of re-parsing). Thread-local, so no cross-worker contention. Result: ACP_NB_WRONG_TLC completes in ~29s (was ~143s post-#189, ~5x), same verdict (AC1 violated). Gate: diff_tlc 20/20, cargo test --release 1486 passed / 0 failed — pure memoization, no behavior change.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
try_eval_compiled_guard_as_actionrecompiled the resolved action's IR —compile_action_ir+CompiledActionIr::from_ir+compile_expr/lower— on every guard evaluation. This guard is on the hot path: each\E-quantified disjunct of a Next disjunction (e.g. ACP's\E i,j : parDie(i) \/ parProgNB(i,j)) resolves through it.For a fairness spec that re-explores the state graph during trace reconstruction (
reconstruct_trace_limited, a full re-BFS when the parent-map isn't available), this meant re-compilingparProg/decideOnForward/abortOnTimeouton every re-visited state. A gdb sample of the stall showed 4+ worker threads deep infrom_ir→compile_action_clause_text→compile_expr/lower.The fix reuses the existing thread-local + prewarmed
get_or_compile_actioncache (already used by the inlineexecute_branchpath) instead of the fresh compile.Result
ACP_NB_WRONG_TLCnow completes in ~143s — previously it stalled past 300s in trace reconstruction — with the same verdict (invariant 'AC1' violated). A gdb backtrace after the fix confirmsfrom_iris gone from the hot path.Validation
scripts/diff_tlc.sh: 19/19.cargo test --release: clean (the loneprop_pause_visibilityblip is the known-flaky checkpoint-concurrency proptest — passes in isolation).get_or_compile_actionapplies the same resolution schema as every other compiled-IR consumer, so no behavior difference (confirmed by the gate).Note: this speeds up ACP's completion but the spec still over-generates its distinct count (~13.7k vs TLC 12,893) and that count is run-to-run nondeterministic — a separate correctness issue tracked independently.