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]

Date: Wed, 22 May 2024 18:54:25 +0200
From: Andrea Parri <parri.andrea@...il.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
	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

Alan, all,

("randomly" picking a recent post in the thread, after having observed
this discussion for a while...)

> It would be better if there was a way to tell herd7 not to add the 'mb 
> tag to failed instructions in the first place.  This approach is 
> brittle; see below.

AFAIU, changing the herd representation to generate mb-accesses in place
of certain mb-fences...

> If you do want to use this approach, it should be simplified.  All you 
> need is:
> 
> 	[M] ; po ; [RMW_MB]
> 
> 	[RMW_MB] ; po ; [M]
> 
> This is because events tagged with RMW_MB always are memory accesses, 
> and accesses that aren't part of the RMW are already covered by the 
> fencerel(Mb) thing above.

.. and updating the .cat file to the effects of something like

  -let mb = ([M] ; fencerel(Mb) ; [M]) |
  +let mb = (([M] ; po? ; [Mb] ; po? ; [M]) \ id) |

.. can hardly be called "making RMW barriers explicit".  (So much so
that the first commit in PR #865 was titled "Remove explicit barriers
from RMWs".  :-))

Overall, this discussion rather seems to confirm the close link between
tools/memory-model/ and herdtools7.  (After all, to what extent could
any putative RMW_MB be considered "explicit" without _knowing the under-
lying representation of the RMW operations...)  My understanding is that
this discussion was at least in part motivated by a desire to experiment
and familiarize with the current herd representation (that does indeed
require some getting-used-to...); this suggests, as some of you already
mentioned, to add some comments or a .txt in tools/memory-model/ in order
to document such representation and ameliorate that experience.  OTOH, I
must admit, I'm unable to see here sufficient motivation(tm) for changing
the current representation (and model): not the how, but the why...

  Andrea