tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

A recent discussion[1] shows that we are in favor of strengthening the
ordering of unlock + lock on the same CPU: a unlock and a po-after lock
should provide the so-called RCtso ordering, that is a memory access S
po-before the unlock should be ordered against a memory access R
po-after the lock, unless S is a store and R is a load.

The strengthening meets programmers' expection that "sequence of two
locked regions to be ordered wrt each other" (from Linus), and can
reduce the mental burden when using locks. Therefore add it in LKMM.

[1]: https://lore.kernel.org/lkml/[email protected]/

Co-developed-by: Alan Stern <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Boqun Feng <[email protected]>
Reviewed-by: Michael Ellerman <[email protected]> (powerpc)
Acked-by: Palmer Dabbelt <[email protected]> (RISC-V)
Acked-by: Peter Zijlstra (Intel) <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>

0 files changed, 0 insertions, 0 deletions