Module miri::concurrency

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.
• init_once
• 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