Module miri::concurrency

source ·


Implementation of a data-race detector using Lamport Timestamps / Vector-clocks based on the Dynamic Race Detection for C++: which does not report false-positives when fences are used, and gives better accuracy in presence of read-modify-write operations.
Implements a map from allocation ranges to data. This is somewhat similar to RangeMap, but the ranges and data are discrete and non-splittable – they represent distinct “objects”. An allocation in the map will always have the same range until explicitly removed
Implements threads.
Implementation of C++11-consistent weak memory emulation using store buffers based on Dynamic Race Detection for C++ (“the paper”):