Module miri::concurrency

source ·

Modules

Implementation of a data-race detector using Lamport Timestamps / Vector-clocks based on the Dynamic Race Detection for C++: https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf 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”): https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf