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: <ZlClXpjGga-6cv00@Boquns-Mac-mini.home>
Date: Fri, 24 May 2024 07:34:06 -0700
From: Boqun Feng <boqun.feng@...il.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>,
	Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
	"Paul E. McKenney" <paulmck@...nel.org>,
	linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
	kernel-team@...a.com, parri.andrea@...il.com, j.alglave@....ac.uk,
	luc.maranget@...ia.fr, Joel Fernandes <joel@...lfernandes.org>
Subject: Re: LKMM: Making RMW barriers explicit

On Fri, May 24, 2024 at 10:14:25AM -0400, Alan Stern wrote:
[...]
> > Not really, RMW events contains all events generated from
> > read-modify-write primitives, if there is an R event without a rmw
> > relation (i.e there is no corresponding write event), it's a failed RWM
> > by definition: it cannot be anything else.
> 
> Not true.  An R event without an rmw relation could be a READ_ONCE().  

No, the R event is already in the RWM events, it has come from a rwm
atomic.

> Or a plain read.  The memory model uses the tag to distinguish these 
> cases.
> 
> > > that it would work is merely an artifact of herd7's internal actions.  I 
> > > think it would be much cleaner if herd7 represented these events in some 
> > > other way, particularly if we can tell it how.
> > > 
> > > After all, herd7 already does generate different sets of events for 
> > > successful (both R and W) and failed (only R) RMWs.  It's not such a big 
> > > stretch to make the R events it generates different in the two cases.
> > > 
> > 
> > I thought we want to simplify the herd internal processing by avoid
> > adding mb events in cmpxchg() cases, in the same spirit, if syntactic
> > tagging is already good enough, why do we want to make herd complicate?
> 
> Herd7 already is complicated by the fact that it needs to handle 
> cmpxchg() instructions in two ways: success and failure.  This 
> complication is unavoidable.  Adding one extra layer (different tags for 
> the different ways) is an insignificant increase in the complication, 
> IMO. And it's a net reduction when you compare it to the amount of 
> complication currently in the herd7 code.
> 
> Also what about cmpxchg_acquire()?  If it fails, it will generate an R 
> event with an acquire tag not in the rmw relation.  There is no way to 
> tell such events apart from a normal smp_load_acquire(), and so the .cat 
> file would have no way to know that the event should not have acquire 
> semantics.  I guess we would have to rename this tag, as well.

No,

	let read_of_rmw = (RMW & R) 
	let fail_read_of_rmw = read_of_rmw / dom(rmw)
	let fail_cmpxchg_acquire = fail_read_of_rmw & [Acquire]

gives you all the failed cmpxchg_acquire() apart from a normal
smp_load_acquire().

Regards,
Boqun

> 
> Alan