linux-kernel - Re: LKMM: Making RMW barriers explicit

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: <ZlAJzioZnQqNLivU@andrea>
Date: Fri, 24 May 2024 05:30:22 +0200
From: Andrea Parri <parri.andrea@...il.com>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: Alan Stern <stern@...land.harvard.edu>,
	Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>,
	"Paul E. McKenney" <paulmck@...nel.org>,
	linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
	kernel-team@...a.com, boqun.feng@...il.com, j.alglave@....ac.uk,
	luc.maranget@...ia.fr, Joel Fernandes <joel@...lfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit

> Do you mean the one example in Table 3?
> What about cmpxchg() or cmpxchg_acquire()?

Yes, Table 3.

The cmpxchg*() primitives were not discussed in the paper.  IIRC, their
representation has not changed since at least 1c27b644c0fd.


> We're definitely getting rid of some lines in herd7, that have been added
> solely for dealing with this specific case of LKMM.

Good.  If the herd7 maintainers are "tired" of dealing with those lines,
that's definitely a big fat "why" to put in a changelog.


> Deal with what, no longer having to learn OCaml to be sure that the LKMM's
> formal definition matches the description in memory_barriers.txt?

Nope.  ;-)   Dealing with the review, testing, and maintainance of a new
representation.


> - it makes it easier to maintain the LKMM in the future, because you don't
> have to work around hidden transformations inside herd7
> - it makes implicit behavior explicit
> - it makes it easier to understand that the formalization matches the
> intention
> - it makes it easier to learn the LKMM from the formalization without having
> to cross-reference every bit with the informal documentation to avoid
> misunderstandings

Jonas -  You write "less hidden", "less implicit", but I keep reading "a
representation I/some people would expect".  We've already acknowledged
that's no deciding factor to abandon the current seasoned representation.

  Andrea