feat(modelchecker): add --experimental_no_graph for low-memory model …#350
Merged
Conversation
…checking
WIP commit on the experimental-no-graph branch — will be rebased onto
the early-deadlock-detection PR (option A in the design discussion)
before final merge.
Drops the in-memory state graph after each yield-point is expanded.
Keeps symmetry reduction, dedup, unique-state count, and safety /
transition assertions. Refuses to run if the spec declares any
liveness assertions (eventually / always-eventually / eventually-always)
since cycle-based liveness checks cannot run without a graph.
Mechanism:
- visited stores hashes only (values nil).
- Attach() is skipped (no Outbound edges built).
- ForkForAction/ForkForAlternatePaths' child Inbound[0].Node is
nilled out immediately after scheduling (preserves link Name for
diagnostics; breaks the back-reference that would otherwise pin
the parent Process).
- A lightweight pathNode chain (action name + parent pointer; no
Process refs) is attached to each scheduled node so a failure
trace can be reconstructed without keeping ancestor Process
objects alive.
- After a yp's expansion completes in startProcessedQueue's Phase 2,
yp.Process.Heap / Threads / Roles / Channels / ChannelMessages /
Parent / Children are nilled out — making yp + its ancestor
Process objects GC-eligible.
On slatedb 3-writer DFS (322,464 nodes, 111,134 unique states):
- Wall time: 29m → 12m (2.4x faster, less GC pressure).
- Max RSS: 13.51 GB → 93 MB (148x reduction).
Open follow-up: deadlock detection still relies on post-run
traverseBFS in regular mode; in no_graph mode there's no graph so
deadlock_detection currently has no effect. Early deadlock detection
at expansion time (independent of no_graph) lands separately.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts:
# main.go
# modelchecker/processor.go
jp-fizzbee
pushed a commit
that referenced
this pull request
May 18, 2026
The --experimental_no_graph flag landed in #350 but wasn't wired through the fizz wrapper script — users invoking via ./fizz couldn't opt in to no_graph mode. Add the parse case, args-forwarding, and default-false initializer. Also document both experimental flags in the usage() output so they appear in --help. The wrapper had silently forwarded --experimental_processed_queue without listing it in usage; users discovered it only via the binary's --help. The new usage block calls them out as experimental-and-off-by-default with a one-line summary each, including the no_graph caveats (no liveness, no crash simulation, auto-enables processed_queue). Verified: ./fizz --help now lists both flags; ./fizz --experimental_no_graph <spec> runs in no_graph mode (visible from the auto-enable note and the "Peak (new)" line confirming the NEW queue path). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
jp-fizzbee
added a commit
that referenced
this pull request
May 18, 2026
…gs (#351) The --experimental_no_graph flag landed in #350 but wasn't wired through the fizz wrapper script — users invoking via ./fizz couldn't opt in to no_graph mode. Add the parse case, args-forwarding, and default-false initializer. Also document both experimental flags in the usage() output so they appear in --help. The wrapper had silently forwarded --experimental_processed_queue without listing it in usage; users discovered it only via the binary's --help. The new usage block calls them out as experimental-and-off-by-default with a one-line summary each, including the no_graph caveats (no liveness, no crash simulation, auto-enables processed_queue). Verified: ./fizz --help now lists both flags; ./fizz --experimental_no_graph <spec> runs in no_graph mode (visible from the auto-enable note and the "Peak (new)" line confirming the NEW queue path). Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
2 participants
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.
…checking
WIP commit on the experimental-no-graph branch — will be rebased onto the early-deadlock-detection PR (option A in the design discussion) before final merge.
Drops the in-memory state graph after each yield-point is expanded. Keeps symmetry reduction, dedup, unique-state count, and safety / transition assertions. Refuses to run if the spec declares any liveness assertions (eventually / always-eventually / eventually-always) since cycle-based liveness checks cannot run without a graph.
Mechanism:
On slatedb 3-writer DFS (322,464 nodes, 111,134 unique states):
Open follow-up: deadlock detection still relies on post-run traverseBFS in regular mode; in no_graph mode there's no graph so deadlock_detection currently has no effect. Early deadlock detection at expansion time (independent of no_graph) lands separately.
Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com
Conflicts:
main.go
modelchecker/processor.go