Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Detect data races #1372

Closed
RalfJung opened this issue Apr 27, 2020 · 1 comment
Closed

Detect data races #1372

RalfJung opened this issue Apr 27, 2020 · 1 comment
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)

Comments

@RalfJung
Copy link
Member

RalfJung commented Apr 27, 2020 •
edited
Loading

#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
@RalfJung RalfJung added 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) A-concurrency Area: affects our concurrency (multi-thread) support labels Apr 27, 2020
@JCTyblaidd JCTyblaidd mentioned this issue Nov 2, 2020
Merged
bors added a commit that referenced this issue Nov 29, 2020
@bors
Auto merge of #1617 - JCTyblaidd:data_race_detector, r=RalfJung
d473242 
Add simple data-race detector

Partially fixes data-race detection, see #1372, based on Dynamic Race Detection for C++11

- This does not explore weak memory behaviour, only exploring one sequentially consistent ordering.
- Data-race detection is only enabled after the first thread is created, so should have minimal overhead for non-concurrent execution.
- ~~Does not attempt to re-use thread id's so creating and joining threads lots of time in an execution will result in the vector clocks growing in size and slowing down program execution~~ It does now
@RalfJung
Copy link
Member Author

Fixed by #1617. Miri still does not support weak memory, but that is a separate problem I would say.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
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)
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@RalfJung