tools: memory-model: Make plain accesses carry dependencies
authorJonas Oberhauser <jonas.oberhauser@huawei.com>
Fri, 2 Dec 2022 12:51:00 +0000 (13:51 +0100)
committerPaul E. McKenney <paulmck@kernel.org>
Wed, 4 Jan 2023 04:47:04 +0000 (20:47 -0800)
commit9ba7d3b3b826ef47c1b7b8dbc2d57da868168128
tree417b56e883b2ff7d3f5a65ff3a4871616b94b63e
parentaae0c8a50d6d312d87188cf4dc8bde8c253978d7
tools: memory-model: Make plain accesses carry dependencies

As reported by Viktor, plain accesses in LKMM are weaker than
accesses to registers: the latter carry dependencies but the former
do not. This is exemplified in the following snippet:

  int r = READ_ONCE(*x);
  WRITE_ONCE(*y, r);

Here a data dependency links the READ_ONCE() to the WRITE_ONCE(),
preserving their order, because the model treats r as a register.
If r is turned into a memory location accessed by plain accesses,
however, the link is broken and the order between READ_ONCE() and
WRITE_ONCE() is no longer preserved.

This is too conservative, since any optimizations on plain
accesses that might break dependencies are also possible on
registers; it also contradicts the intuitive notion of "dependency"
as the data stored by the WRITE_ONCE() does depend on the data read
by the READ_ONCE(), independently of whether r is a register or a
memory location.

This is resolved by redefining all dependencies to include
dependencies carried by memory accesses; a dependency is said to be
carried by memory accesses (in the model: carry-dep) from one load
to another load if the initial load is followed by an arbitrarily
long sequence alternating between stores and loads of the same
thread, where the data of each store depends on the previous load,
and is read by the next load.

Any dependency linking the final load in the sequence to another
access also links the initial load in the sequence to that access.

More deep details can be found in this LKML discussion:

https://lore.kernel.org/lkml/d86295788ad14a02874ab030ddb8a6f8@huawei.com/

Reported-by: Viktor Vafeiadis <viktor@mpi-sws.org>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huawei.com>
Reviewed-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
tools/memory-model/Documentation/explanation.txt
tools/memory-model/linux-kernel.bell
tools/memory-model/litmus-tests/dep+plain.litmus [new file with mode: 0644]