The relation tools rely on
The happens before relation orders events that are causally connected. Tools use it to decide whether two memory accesses are ordered or concurrent.
How edges are added
A tool builds a happens before graph by adding edges for synchronization:
- an unlock happens before the next lock of the same mutex
- a thread start happens before the threads first action
- a join happens after the joined threads last action
- a release on an atomic happens before a matching acquire
Two accesses with no path between them are concurrent, and a concurrent conflicting pair is a race.
Why ordering not timing
Happens before captures causality, not wall clock time. Two events can overlap in real time yet be ordered by a lock, or run far apart yet be concurrent because nothing connects them.
Key idea
Tools order events by adding happens before edges for locks, starts, joins, and atomics, then call any pair with no connecting path concurrent and a possible race.