Module miri::concurrency::vector_clock

source ·

Structs§

  • A vector clock for detecting data-races, this is conceptually a map from a vector index (and thus a thread id) to a timestamp. The compare operations require that the invariant that the last element in the internal timestamp slice must not be a 0, hence all zero vector clocks are always represented by the empty slice; and allows for the implementation of compare operations to short circuit the calculation and return the correct result faster, also this means that there is only one unique valid length for each set of vector clock values and hence the PartialEq and Eq derivations are correct.
  • The time-stamps recorded in the data-race detector consist of both a 32-bit unsigned integer which is the actual timestamp, and a Span so that diagnostics can report what code was responsible for an operation.
  • A vector clock index, this is associated with a thread id but in some cases one vector index may be shared with multiple thread ids if it’s safe to do so.

Constants§

  • The size of the vector-clock to store inline clock vectors larger than this will be stored on the heap