Module miri::concurrency::data_race
source · Expand description
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.
The implementation contains modifications to correctly model the changes to the memory model in C++20 regarding the weakening of release sequences: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0982r1.html. Relaxed stores now unconditionally block all currently active release sequences and so per-thread tracking of release sequences is not needed.
The implementation also models races with memory allocation and deallocation via treating allocation and deallocation as a type of write internally for detecting data-races.
Weak memory orders are explored but not all weak behaviours are exhibited, so it can still miss data-races but should not report false-positives
Data-race definition from(https://en.cppreference.com/w/cpp/language/memory_model#Threads_and_data_races): a data race occurs between two memory accesses if they are on different threads, at least one operation is non-atomic, at least one operation is a write and neither access happens-before the other. Read the link for full definition.
This re-uses vector indexes for threads that are known to be unable to report data-races, this is valid
because it only re-uses vector indexes once all currently-active (not-terminated) threads have an internal
vector clock that happens-after the join operation of the candidate thread. Threads that have not been joined
on are not considered. Since the thread’s vector clock will only increase and a data-race implies that
there is some index x where clock[x] > thread_clock, when this is true clock[candidate-idx] > thread_clock
can never hold and hence a data-race can never be reported in that vector index again.
This means that the thread-index can be safely re-used, starting on the next timestamp for the newly created
thread.
The timestamps used in the data-race detector assign each sequence of non-atomic operations followed by a single atomic or concurrent operation a single timestamp. Write, Read, Write, ThreadJoin will be represented by a single timestamp value on a thread. This is because extra increment operations between the operations in the sequence are not required for accurate reporting of data-race values.
As per the paper a threads timestamp is only incremented after a release operation is performed so some atomic operations that only perform acquires do not increment the timestamp. Due to shared code some atomic operations may increment the timestamp when not necessary but this has no effect on the data-race detection code.
Structs§
- Externally stored memory cell clocks explicitly to reduce memory usage for the common case where no atomic operations exists on the memory cell.
- Error returned by finding a data race should be elaborated upon.
- Global data-race detection state, contains the currently executing thread as well as the vector-clocks associated with each of the threads.
- Memory Cell vector clock metadata for data-race detection.
- The current set of vector clocks describing the state of a thread, contains the happens-before clock and additional metadata to model atomic fence operations.
- Extra metadata associated with a thread.
- Vector clock metadata for a logical memory allocation.
Enums§
- Valid atomic fence orderings, subset of atomic::Ordering.
- Valid atomic read orderings, subset of atomic::Ordering.
- Valid atomic read-write orderings, alias of atomic::Ordering (not non-exhaustive).
- Valid atomic write orderings, subset of atomic::Ordering.
- Type of a non-atomic read operation.
- Type of a non-atomic write operation: allocating memory, non-atomic writes, and deallocating memory are all treated as writes for the purpose of the data-race detector.