Draft
Conversation
Detects WAW/RAW races between thread blocks by recording Load/Store/Atomic accesses and comparing overlapping addresses across blocks. Atomic-only overlaps are correctly excluded.
Replace the concrete-only race detector with a symbolic-first approach:
run one representative block symbolically to build Z3 address expressions,
then use an SMT solver to check if two different blocks can access
overlapping memory. Falls back to concrete execution with inverted-index
detection for kernels with data-dependent addresses (e.g., histogram).
Key changes:
- Add SymbolicMemoryAccess dataclass in data.py
- Rewrite race_detector.py with op overriders for all op types, Z3
cross-block checking, and concrete fallback with dynamic overrider
disabling
- Fix ConstSymbolicExpr.concretize() in symbolic_engine.py to handle
multi-element TensorHandles created by replace_subtree("load")
…detector SymbolicSanitizer and RaceDetector shared ~500 lines of duplicated code: operation overrider functions, numpy-to-symbolic-op mappings, RangeWrapper, and for-loop callback infrastructure. This extracts the shared code into a SymbolicClient(Client) base class in symbolic_engine.py, with subclass hooks (_on_data_dependent_value, _should_skip_loop_hooks, _loop_hook_before/after) for domain-specific behavior.
…olic_engine Move shared symbolic operation overriders and for-loop infrastructure from Sanitizer into a new SymbolicClient base class in symbolic_engine.py. This enables other symbolic clients to reuse the common logic without duplicating code. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… base class Move _op_atomic_cas_overrider and _op_atomic_rmw_overrider into SymbolicClient since they are generic value-to-SymbolicExpr conversions with no sanitizer-specific logic. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…olic_engine Move shared symbolic operation overriders and for-loop infrastructure from Sanitizer into a new SymbolicClient base class in symbolic_engine.py. This enables other symbolic clients to reuse the common logic without duplicating code.
… base class Move _op_atomic_cas_overrider and _op_atomic_rmw_overrider into SymbolicClient since they are generic value-to-SymbolicExpr conversions with no sanitizer-specific logic.
Move _op_raw_load_overrider and _op_raw_store_overrider from sanitizer into SymbolicClient since they are identical delegation methods that any symbolic client will need.
mark14wu
force-pushed
the
refactor/symbolic-client
branch
from
325c6ec to
8d9a3ba
Compare
… SymbolicClient - Move _op_raw_load_overrider and _op_raw_store_overrider from both sanitizer and race_detector into the SymbolicClient base class - Simplify race_detector atomic overriders to call super() instead of duplicating SymbolicExpr creation logic - Remove redundant entries from overrider_map.update() in both subclasses
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.
Detects WAW/RAW races between thread blocks by recording Load/Store/Atomic accesses and comparing overlapping addresses across blocks.