Module miri::concurrency

source ·

Modules

data_race
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.
range_object_map 🔒
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
sync
thread
Implements threads.
vector_clock 🔒
weak_memory
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