Fix VTIME_PROFILING-only part of the code so that TimeTrace::printPretty() does not crash in the timer thread when something else is happening in the main thread - #928
Open
quickbeam123 wants to merge 1 commit into
Conversation
limitReached() runs on timer_thread and calls env.statistics->print(), which reaches TimeTrace::printPretty() (Shell/Statistics.cpp:339), while the main thread is still proving and still mutating the time trace. Three of the interactions were memory-unsafe: - printPrettyRec() sorted `children` *in place*. That is a Lib::Stack<unique_ptr<Node>> which the main thread's ScopedTimer constructor scans and appends to; a concurrent append reallocates the array std::sort is writing into, and the main thread can meanwhile read a moved-from unique_ptr. - printPretty() iterates `_stack` twice while every TIME_TRACE scope pushes and pops it, ~10^9 times per run, reallocating it under the iterator. - Node carried USE_ALLOCATOR(Node), and Lib::Stack::expand uses ALLOC_KNOWN; both route to GLOBAL_SMALL_OBJECT_ALLOCATOR, which is plain free lists with no synchronisation (Lib/Allocator.hpp). Node::flatten() therefore allocated dozens of nodes on timer_thread while the main thread allocated clauses from the same free lists. This corrupts the heap silently and faults later, which is why it only appeared under load. Fix: freeze the trace rather than stop the thread, so the main thread needs no new check anywhere. _enabled becomes atomic and limitReached() clears it (plus a one-tick settle) before reporting; ScopedTimer remembers in _active whether it actually pushed, so a frozen trace is never written to again, not even by already-open scopes. printPrettyRec() orders a local vector<Node*>, and the whole TimeTrace subsystem now uses std::vector and the system allocator, so timer_thread never enters the prover's pool. Storing _active also fixes a latent bug: the destructor used to re-read _enabled, so any flip between construction and destruction unbalanced _stack and mis-attributed every subsequent scope. limitReached() additionally flushes std::cout, which terminateImmediately() (std::_Exit) does not -- the tail of the report was lost whenever stdout was a file rather than a tty. Reproducer: a full TPTP sweep (26504 problems, -i 100000 -tstat on, 120 jobs in parallel) produced 2450 logs containing "Aborted by signal" -- 2120 SIGSEGV plus SIGBUS/SIGABRT -- roughly one in five of the instruction-limited runs, with 2239 further logs losing their profile section to truncated or interleaved output. In all 2450 the abort line lands *inside* the time-trace output (1676 inside the flattened profile, 774 inside the trace tree, none before it). Count these with `grep -la`: plain `grep -l` skips the interleaved logs as binary and undercounts to 1900. No small deterministic reproducer; the same code path is reached locally by `vampire -tstat on -t 3 <any problem that will not finish>`, but an idle machine does not hit the race often enough to be a test. Verified: unit tests 100/100, checks/sanity clean against a release build, and every node's `cnt` on AGT001+1.p identical before and after (the flattened profile's ordering of near-equal entries varies run to run in the old binary too). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
MichaelRawson
left a comment
MichaelRawson
left a comment
Contributor
There was a problem hiding this comment.
The "set a flag and wait for a bit" approach feels like a mutex done badly. Did you try a mutex? Otherwise no objection.
|
|
||
| // terminateImmediately is std::_Exit, which does not flush: without this the tail of | ||
| // the report is lost whenever stdout is a (fully buffered) file rather than a tty. | ||
| std::cout.flush(); |
Contributor
There was a problem hiding this comment.
We could consider putting this into terminateImmediately.
| // Order a local copy rather than sorting `children` in place: this is called on the | ||
| // timer thread while the main thread may still be scanning and appending to | ||
| // `children` (Lib/Timer.cpp, limitReached()), and an in-place sort would move | ||
| // elements under it. Also makes printing idempotent. |
Contributor
There was a problem hiding this comment.
The whole point of acquiring the lock is that this part is not multi-threaded, no?
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.
More details in the commit message ...