message-format-runtime: Reuse halts_reachable visited buffer via epoch counter#5
Merged
waywardmonkeys merged 1 commit intoforest-rs:mainfrom Apr 27, 2026
Conversation
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.
The catalog verifier called
halts_reachableonce per message insideverify_code, allocating a freshvec![false; pcs.len()]every time. For catalogs with many messages this dominates load cost. The memset is O(messages × code_len), so verify time scales superlinearly with message count.This change introduces a small
HaltsScratchworkspace that lives for the duration ofverify_code. The visited buffer is a generationalVec<u32>: each message bumps anepochcounter and marksvisited[idx] = epoch; a slot counts as "visited for the current pass" iff its value equals the current epoch. No memset is needed between messages, and on the (theoretical)u32wrap, the buffer is re-zeroed and the epoch resets to 1. The DFS work stack is also reused across passes.Two unit tests cover the correctness boundaries that would otherwise be silent:
halts_reachable_buffer_is_reset_between_messages: three messages share a singleHALTat pc 0. If the visited buffer leaks state across messages, the second and third would falsely reportUnterminatedEntry.halts_scratch_epoch_sequencing_and_wrap: exercises the epoch increment and theu32wrap path directly, asserting the buffer is re-zeroed before reuse.Both tests fail in the buggy variant (verified by temporarily stubbing
begin_passto skip the bump). The full workspace test suite, clippy, and fmt all pass.Measured on a synthetic catalog where every message back-edges to a shared
HALT(criterion, release build):The improvement scales with message count exactly as expected: per-message O(N) memset work has been collapsed into an O(1) epoch bump, so
halts_reachable's contribution to verification went from O(M·N) to O(M·d̄), where d̄ is the average reachable depth from each entry. All p < 0.05.