Race Conditions Defined
1. Every data structure defines invariant conditions.
defines the space of possible legal states of the structure
defines what it means for the structure to be “well-formed”
2. Operations depend on and preserve the invariants.
The invariant must hold when the operation begins.
The operation may temporarily violate the invariant.
The operation restores the invariant before it completes.
3. Arbitrarily interleaved operations violate invariants.
Rudely interrupted operations leave a mess behind for others.
4. Therefore we must constrain the set of possible schedules.