linux-kernel - [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Message-Id: <20240919130634.298181-1-jonas.oberhauser@huaweicloud.com>
Date: Thu, 19 Sep 2024 15:06:29 +0200
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: paulmck@...nel.org
Cc: stern@...land.harvard.edu,
	parri.andrea@...il.com,
	will@...nel.org,
	peterz@...radead.org,
	boqun.feng@...il.com,
	npiggin@...il.com,
	dhowells@...hat.com,
	j.alglave@....ac.uk,
	luc.maranget@...ia.fr,
	akiyks@...il.com,
	dlustig@...dia.com,
	joel@...lfernandes.org,
	urezki@...il.com,
	quic_neeraju@...cinc.com,
	frederic@...nel.org,
	linux-kernel@...r.kernel.org,
	lkmm@...ts.linux.dev,
	hernan.poncedeleon@...weicloud.com,
	Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Subject: [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model

Currently, the effect of several tag on operations is defined only in
the herd7 tool's OCaml code as syntax transformations, while the effect
of all other tags is defined in tools/memory-model.
This asymmetry means that two seemingly analogous definitions in 
tools/memory-model behave quite differently because the generated
representation is sometimes modified by hardcoded behavior in herd7.

It also makes it hard to see that the behavior of the formalization 
matches the intuition described in explanation.txt without delving into
the implementation of herd7.

Furthermore, this hardcoded behavior is hard to maintain inside herd7 and
other tools implementing WMM, and has caused several bugs and confusions
with the tool maintainers, e.g.:

  https://github.com/MPI-SWS/genmc/issues/22
  https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904
  https://github.com/hernanponcedeleon/Dat3M/issues/254

It also means that potential future extensions of LKMM with new tags may
not work without changing internals of the herd7 tool.

In this patch series, we first emulate the effect of herd7 transformations
in tools/memory-model through explicit rules in .cat and .bell files that
reference the transformed tags.
These transformations do not have any immediate effect with the current
herd7 implementation, because they apply after the syntax transformations
have already modified those tags.

In a second step, we then distinguish between syntactic tags (that are
placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the
read and write of an xchg_acquire() operation) and sets of events (that
would be defined after the (emulated) transformations, e.g., an Acquire
set that includes only on the read of the xchg_acquire(), but "has been
removed" from the write).

This second step (comprising patches 4 and 5) is incompatible with the
current herd7 implementation, since herd7 uses hardcoded tag names to decide
what to do with LKMM; therefore, the newly introduced syntactic tags will be
ignored or processed incorrectly by herd7.

Have fun,
  jonas

Changes from v1 to v2:
   - addressed several spelling/style issues pointed out by Alan
   - simplified the definition of Marked accesses based on a
      suggestion by Alan

Changes from v2 to v3:
  - addressed imprecise comment pointed out by Boqun
  - addressed the backwards compatibility issue pointed out by Akira
    with help of Hernan: improved version compatibility by adding
    an error message on older versions of herd and relying on a new
    flag -lkmmv1 to select the version
  - integrated recent patches, like the herd representation table
    and primitives like atomic_add_unless or atomic_and_not

Jonas Oberhauser (5):
  tools/memory-model: Legitimize current use of tags in LKMM macros
  tools/memory-model: Define applicable tags on operation in tools/...
  tools/memory-model: Define effect of Mb tags on RMWs in tools/...
  tools/memory-model: Switch to softcoded herd7 tags
  tools/memory-model: Distinguish between syntactic and semantic tags

 .../Documentation/herd-representation.txt     |  27 +--
 tools/memory-model/linux-kernel.bell          |  33 ++-
 tools/memory-model/linux-kernel.cat           |  10 +
 tools/memory-model/linux-kernel.cfg           |   1 +
 tools/memory-model/linux-kernel.def           | 196 +++++++++---------
 .../litmus-tests/add-unless-mb.litmus         |  27 +++
 6 files changed, 176 insertions(+), 118 deletions(-)
 create mode 100644 tools/memory-model/litmus-tests/add-unless-mb.litmus

-- 
2.34.1