Description
#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