tools/memory-model: Tie acquire loads to reads-from

This commit explicitly makes the connection between acquire loads and
the reads-from relation.  It also adds an entry for happens-before,
and refers to the corresponding section of explanation.txt.

Reported-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit is contained in:
Paul E. McKenney 2020-11-06 09:58:01 -08:00
parent 5c8fe583cc
commit 8881e7a774

View file

@ -33,10 +33,11 @@ Acquire: With respect to a lock, acquiring that lock, for example,
acquire loads.
When an acquire load returns the value stored by a release store
to that same variable, then all operations preceding that store
happen before any operations following that load acquire.
to that same variable, (in other words, the acquire load "reads
from" the release store), then all operations preceding that
store "happen before" any operations following that load acquire.
See also "Relaxed" and "Release".
See also "Happens-Before", "Reads-From", "Relaxed", and "Release".
Coherence (co): When one CPU's store to a given variable overwrites
either the value from another CPU's store or some later value,
@ -119,6 +120,11 @@ Fully Ordered: An operation such as smp_mb() that orders all of
that orders all of its CPU's prior accesses, itself, and
all of its CPU's subsequent accesses.
Happens-Before (hb): A relation between two accesses in which LKMM
guarantees the first access precedes the second. For more
detail, please see the "THE HAPPENS-BEFORE RELATION: hb"
section of explanation.txt.
Marked Access: An access to a variable that uses an special function or
macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".