Document, test, and fix --race-check instrumentation#8846
Open
tautschnig wants to merge 4 commits intodiffblue:developfrom
Open
Document, test, and fix --race-check instrumentation#8846tautschnig wants to merge 4 commits intodiffblue:developfrom
tautschnig wants to merge 4 commits intodiffblue:developfrom
Conversation
tautschnig
requested review from
TGWDB,
jimgrundy,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR improves the --race-check instrumentation in goto-instrument by documenting the approach, fixing user-facing help/manpage text, extending instrumentation to more instruction kinds (guards, call arguments, returns), and adding regression tests.
Changes:
- Extend race-check read/write discovery and instrumentation to cover
SET_RETURN_VALUEand additional instruction kinds beyondASSIGN. - Improve documentation (inline header overview + user manual entry) and fix incorrect
--race-checkhelp/manpage text. - Add a new regression test suite under
regression/goto-instrument/race-check/to exercise newly-covered cases.
Reviewed changes
Copilot reviewed 27 out of 27 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| src/goto-instrument/rw_set.cpp | Treat SET_RETURN_VALUE expressions as reads for race analysis. |
| src/goto-instrument/race_check.h | Add high-level documentation of the race-check instrumentation scheme and API docs. |
| src/goto-instrument/race_check.cpp | Add dirty-local support, exclude function symbols, tag generated assertions with property_class="race-check", and instrument additional instruction kinds. |
| src/goto-instrument/goto_instrument_parse_options.cpp | Fix --race-check help text. |
| regression/goto-instrument/race-check/*.c / *.desc | Add new regression tests for read/write race patterns and newly instrumented constructs. |
| doc/man/goto-instrument.1 | Fix --race-check manpage entry text. |
| doc/cprover-manual/properties.md | Document --race-check in the user manual properties table. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Collaborator
Author
|
Looks like GitHub is having issues: https://www.githubstatus.com/incidents/n07yy1bk6kc4. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8846 +/- ##
===========================================
+ Coverage 80.00% 80.08% +0.07%
===========================================
Files 1700 1700
Lines 188271 188294 +23
Branches 73 73
===========================================
+ Hits 150632 150787 +155
+ Misses 37639 37507 -132 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Add Doxygen documentation to race_check.h explaining the Eraser-inspired write-guard instrumentation scheme for data-race detection, including the two kinds of races detected (R/W and W/W), the 5-step instrumentation sequence, and how pointer dereferences are resolved through value-set analysis for alias-aware race detection. Document internal functions in race_check.cpp. Fix the --race-check help text, man page, and cprover manual: the option performs general data-race checking, not floating-point specific checks. Add --race-check to the goto-instrument properties table in the cprover manual. Add regression tests exercising the basic race-check scenarios: write-write, read-write, no-race (thread-local), no-race (sequential), conditional write, and pointer-based race detection. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Set property_class to "race-check" on all generated assertions, consistent with other instrumentation passes (e.g., uninitialized-check, stack-depth). This enables users to filter race-check properties by class and produces property names like [main.race-check.1] instead of [main.1]. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…red variables The race-check instrumentation previously only instrumented ASSIGN instructions. This missed R/W data races where shared variables are read by other instruction types: - GOTO: reading a shared variable in a branch condition (if/while guard) - FUNCTION_CALL: reading shared variables as function arguments, writing return values - SET_RETURN_VALUE: reading a shared variable in a return statement - ASSUME/ASSERT: reading shared variables in conditions For these instructions, R/W and W/W race-check assertions are now inserted before the instruction to detect concurrent writes by other threads. Also add SET_RETURN_VALUE handling to rw_set_loct::compute(), which previously did not track reads from return statements. Also exclude function symbols from race checking: function symbols are not variables and should not generate race-check assertions when read as part of a FUNCTION_CALL instruction. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…taken locals
The race-check instrumentation previously only considered globally shared
variables (symbol.is_shared()). Local variables whose address is taken
and passed to other threads ("dirty locals") were not instrumented,
missing potential data races.
Now use the dirtyt analysis, consistent with how goto-symex determines
shared access: a variable is considered shared if symbol.is_shared() or
dirty(identifier). The dirty analysis is computed once over all functions
in the goto_modelt overload.
Add a CORE regression test (dirty-local.desc) that verifies the
instrumentation is generated for a dirty local by matching on the
--show-goto-functions output.
Add a KNOWNBUG regression test (dirty-local-verification.desc) that
attempts full verification of the dirty-local race. This is marked
KNOWNBUG because CBMC's symex currently aborts with "pointer handling
for concurrency is unsound" when a pointer to a local is shared between
threads.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
race-check-fixes
branch
from
19ab665 to
bae0cd8
Compare
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.
Please review commit-by-commit. Overall summary:
Improve
--race-check: docs, bug fixes, dirty-locals supportDocument the Eraser-inspired write-guard instrumentation scheme. Fix the incorrect "floating-point" help text and add
--race-checkto the cprover manual.Fix missed races: instrument GOTO guards, function call arguments, and return statements (not just ASSIGN). Exclude function symbols from race checking. Set
property_classto"race-check"on generated assertions.Use
dirtytanalysis to treat address-taken locals as shared, matchinggoto-symexbehavior.Add 11 regression tests in
regression/goto-instrument/race-check/.