Detect data races #1372
Labels
A-concurrency
Area: affects our concurrency (multi-thread) support
C-project
Category: a larger project is being tracked here, usually with checkmarks for individual steps
I-misses-UB
Impact: makes Miri miss UB, i.e., a false negative (with default settings)
#1284 adds support for concurrency, but is not able to detect data races incurred by missing synchronization. We should try to find a way to detect data races.
I think the usual approach for this is some kind of vector clock -- valgrind race detectors use that, and they have some very clever schemes going on to make it more efficient. Still, I am worried about the impact this will have on non-concurrent executions. Maybe we need flags to control whether race checking happens or not.
As a follow-up, at some point we might want to look into better implementations of weak memory models, where a read will not always return the latest value that was written. That's even more expensive though and also figuring out the exact rules is still subject of PL research.
Cc @vakaras
The text was updated successfully, but these errors were encountered: