Improve exp.single-threaded for analysis without threadflag and escape#1981
Conversation
sim642
added
cleanup
There was a problem hiding this comment.
Pull request overview
This PR strengthens the effect of exp.single-threaded by routing multi-threadedness and escape-related decisions through centralized helper functions, allowing more precise analysis of single-threaded programs even when threadflag, threadid, or escape analyses are disabled.
Changes:
- Add regression tests covering
exp.single-threadedbehavior whenescape/threadflag(andthreadid) are deactivated. - Introduce/extend helper-based semantics for
MayEscapeandMustBeSingleThreadedqueries viaThreadEscape.has_escapedandThreadFlag.{is_currently_multi,has_ever_been_multi}. - Update multiple analyses to use these helpers instead of directly querying
Queries.MayEscape/Queries.MustBeSingleThreaded.
Reviewed changes
Copilot reviewed 17 out of 17 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/regression/00-sanity/42-no-threadflag.t | New cram test for single-threaded mode with threadflag/threadid deactivated (and earlyglobs toggled). |
| tests/regression/00-sanity/42-no-threadflag.c | C input for the above test (simple global flow-sensitivity expectation). |
| tests/regression/00-sanity/43-no-escape.t | New cram test for single-threaded mode with escape deactivated (with earlyglobs enabled). |
| tests/regression/00-sanity/43-no-escape.c | C input for the above test (address-taken local should remain non-escaped under forced single-threaded mode). |
| src/domains/queries.ml | Document intended access paths for MayEscape / MustBeSingleThreaded via helper functions. |
| src/analyses/threadFlag.ml | Make helper functions respect exp.single-threaded by forcing “not multi-threaded”. |
| src/analyses/threadEscape.ml | Make ThreadEscape.has_escaped return false under exp.single-threaded. |
| src/analyses/singleThreadedLifter.ml | Use ThreadFlag.has_ever_been_multi for multithreaded detection. |
| src/analyses/raceAnalysis.ml | Use ThreadEscape.has_escaped for “treat as global/escaped” decision. |
| src/analyses/mutexAnalysis.ml | Use ThreadEscape.has_escaped for “treat as global/escaped” decision. |
| src/analyses/wrapperFunctionAnalysis.ml | Use ThreadFlag.has_ever_been_multi instead of direct MustBeSingleThreaded query. |
| src/analyses/varEq.ml | Use ThreadFlag.has_ever_been_multi instead of direct MustBeSingleThreaded query. |
| src/analyses/useAfterFree.ml | Use ThreadFlag.has_ever_been_multi for multi-threaded warning gating. |
| src/analyses/memLeak.ml | Use ThreadFlag helpers for multi-threadedness checks and simplify prior helper. |
| src/analyses/basePriv.ml | Use ThreadFlag helpers to detect “recovered to single-threaded” state. |
| src/analyses/apron/relationPriv.apron.ml | Use ThreadFlag.has_ever_been_multi for branched sync decisions. |
| src/analyses/mCP.ml | Add TODOs around exp.single-threaded spawn suppression message behavior. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Due to 7b2a223, locals which have vaddrof false are not longer queried at all by mutex/race analysis.
1. Don't output final message if no thread creations are even attempted by the program. 2. Output non-final message for each suppressed thread.
|
In my rsync runs (goblint/bench@58495e9), something strange happens with this change. When deactivating threadflag and escape in favor of I thought that maybe the |
Apparently our |
There was a problem hiding this comment.
Great PR, I think not using the query with the since_start flag directly makes the intent easier to follow.
The warning message in maingoblint.ml about not enabling escape should be adapted so it is not produced if exp.single-threaded is on.
Also, should we maybe make an issue for the improved autotuner (or ask AI to fix the autotuner right away)?
I redid the rsync comparison after removing the remaining signal handlers in goblint/bench@9192101.
Indeed, I'll update it.
I'll open a separate issue about it because unlike the existing single-threaded SV-COMP autotuner, this is more aggressive and requires a bit more care. This can become unsound if there are other things which we also treat as thread-like (signal handlers, I'd like to have it for SV-COMP 2027 and it's easy to do closer to it happening. I want to see where we can get with the signal handlers (like #1966) before needing to worry about the SV-COMP interactions. |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 21 out of 21 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
So far,
exp.single-threadedonly prevented new threads from being spawned but did not override multi-threadedness related queries.Now, using the queries through the corresponding helper functions, the option has stronger effect.
In particular, this allows analyzing a single-threaded program without the threadflag and escape analyses enabled, without immediately becoming flow-insensitive for globals (like
exp.earlyglobs) and assuming all locals may have escaped (and become globals).There is a performance benefit for having less analyses activated, even if they don't compute anything for single-threaded programs.
This is also what motivated the single-threaded autotuner for SV-COMP. This PR would allow pushing that autotuner even further to disable threadflag and escape analyses for such programs.