cnf: keep Cnf_CutDeriveTruth's truth tables per call - #14
Merged
Merged
Conversation
Cnf_CutDeriveTruth() evaluated a cut's truth table into a static word S[256]. Two managers deriving CNF on separate threads therefore wrote the same array, and a cut's table could be overwritten by another thread's between the write and the read. ThreadSanitizer reports the race when independent STP instances bit-blast concurrently, and it surfaces as a rare crash in the caller. Make the array local to the call. It is 2 KiB of stack, filled before it is read on every call, so nothing carries over from one call to the next that a static would have preserved. Truth6 and C stay static: they are constant tables that are only read. Assisted-by: Claude, via Claude Code
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.
Cnf_CutDeriveTruth() evaluated a cut's truth table into a static `word S[256]`, so two managers deriving CNF on separate threads wrote the same array. STP documents that independent managers may be used on separate threads; ThreadSanitizer reports this as the only race in ABC when independent STP instances bit-blast concurrently, and it surfaces as a rare crash (about one in a thousand runs of STP's concurrent-managers test).
The array becomes local to the call. It is filled before it is read on every call, so nothing that a static would have preserved carries over. Truth6 and C stay static: they are constant tables that are only read.
This is based on b6e26a0, the commit STP pins today, so STP can move its pin to this change alone. With it merged, STP drops the fetch-time patch it currently carries for the same line.