linux-kernel - Re: [PATCH v4 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-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <70907739-56b9-4712-a1db-e55161c2a8d6@paulmck-laptop>
Date: Mon, 28 Oct 2024 13:16:23 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
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
Subject: Re: [PATCH v4 0/5] tools/memory-model: Define more of LKMM in
 tools/memory-model

On Mon, Sep 30, 2024 at 12:57:05PM +0200, Jonas Oberhauser wrote:
> 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.

Thank you, Jonas!

Queued for further review and testing.  This does need at least an ack to
proceed to mainline (hint to LKMM maintainers).

							Thanx, Paul

> 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
> 
> Changes from v3 to v4:
>   - removed a litmus test (submitted to Paul's larger test repo instead)
>   - fixed several formatting/naming issues pointed out by Akira
>   - updated the reference herd version number in memory-model/README.md.
>     *Note*: this may need to be retouched after herd is updated.
>     I also did not update the table under klitmus7 compatibility, which
>     I took to refer only to klitmus7, although its header is "herdtools7"
> 
> 
> 
> 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/README                     |   2 +-
>  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 +++++++++---------
>  6 files changed, 150 insertions(+), 119 deletions(-)
> 
> -- 
> 2.34.1
>