[−][src]Module testbench::race_cell
This module contains shareable mutable containers designed for enabling and detecting race conditions in thread synchronization testing code.
Motivation
The main purpose of a thread synchronization protocol is to ensure that some operations which are not atomic in hardware, such as writing to two unrelated memory locations, appear to occur as atomic transactions from the point of view of other threads: at any point of time, either a given operation appears to be done, or it appears not to have started.
Testing a thread synchronization primitive involves showing that inconsistent states (where an operation appears to be half-performed) have a negligible probability of being exposed to the outside world in all expected usage scenarios. It is typically done by showing that a given non-atomic operation is properly encapsulated by the transactional semantics of the synchronization protocol, and will never appear as half-done to observers.
Non-atomic operations are easier said than done, however, when the set of operations which can be atomic in hardware is larger than most people think (at the time of writing, current Intel CPUs can access memory in blocks of 128 bits, and current NVidia GPUs can do so in blocks of 1024 bits), not well-defined by the architecture (and thus subjected to increase in future hardware), and highly dependent on the compiler's optimization choices in a high-level programming language such as Rust.
Which is why I think we need some types whose operations are guaranteed to be non-atomic under a set of reasonable assumptions, and which can easily be observed to be in an inconsistent state.
Functionality
This module provides the RaceCell type, which can hold a value of a
certain type T like a Cell<T> would, but is guaranteed not to be read
or written to in a single atomic operation, even if the corresponding type T
can be atomically read or written to in hardware.
Furthermore, a RaceCell can detect scenarios where it is read at the same time as it is being written (which constitutes a read-after-write race condition) and report them to the reader thread.
Such "controlled data races" can, in turn, be used to detect failures in thread synchronization protocols, manifesting as inconsistent shared states being exposed to the outside world.
Requirements on T
In principle, any Clone + Eq type T whose equality operator and clone() implementation behave well even if the inner data is in a inconsistent state (e.g. filled with random bits) could be used. This is true of all primitive integral types and aggregates thereof, for example.
However, in practice, unsynchronized concurrent read/write access to arbitrary data from multiple threads constitutes a data race, which is undefined behaviour in Rust even when it occurs inside an UnsafeCell. This is problematic because rustc's optimizer allows itself to transform code which relies on undefined behaviour however it likes, leading to breakages in release builds such as infinite loops appearing out of nowhere.
For this reason, we currently only support some specific types T which have
atomic load and store operations, implemented as part of an atomic wrapper.
Note that although individual loads and stores to T are atomic, loads and
stores to RaceCell
Structs
| RaceCell | Shareable mutable container for triggering and detecting write-after-read data races in a well-controlled fashion. |
Enums
| Racey | This is the result of a RaceCell read |
Traits
| AtomicData | Requirements on the data held by a RaceCell |
| AtomicLoadStore | Atomic wrapper type for a certain kind of value |