Module 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.

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

• AtomicMemoryCellClocks 🔒
  Externally stored memory cell clocks explicitly to reduce memory usage for the common case where no atomic operations exists on the memory cell.
• DataRace
  Error returned by finding a data race should be elaborated upon.
• FrameState
  Vector clock state for a stack frame (tracking the local variables that do not have an allocation yet).
• GlobalState
  Global data-race detection state, contains the currently executing thread as well as the vector-clocks associated with each of the threads.
• LocalClocks 🔒
  Stripped-down version of MemoryCellClocks for the clocks we need to keep track of in a local that does not yet have addressable memory – and hence can only be accessed from the thread its stack frame belongs to, and cannot be access atomically.
• MemoryCellClocks 🔒
  Per-byte vector clock metadata for data-race detection.
• ThreadClockSet 🔒
  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.
• ThreadExtraState 🔒
  Extra metadata associated with a thread.
• VClockAlloc
  Vector clock metadata for a logical memory allocation.

Enums

• AccessType 🔒
• AtomicAccessType 🔒
• AtomicFenceOrd
  Valid atomic fence orderings, subset of atomic::Ordering.
• AtomicReadOrd
  Valid atomic read orderings, subset of atomic::Ordering.
• AtomicRwOrd
  Valid atomic read-write orderings, alias of atomic::Ordering (not non-exhaustive).
• AtomicWriteOrd
  Valid atomic write orderings, subset of atomic::Ordering.
• NaReadType
  Type of a non-atomic read operation.
• NaWriteType
  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.

Traits

• EvalContextExt
• EvalContextPrivExt 🔒

Type Aliases

• AllocState