Re: "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models"

[Alan Stern]

On Sat, Aug 27, 2022 at 01:47:48AM +0200, Peter Zijlstra wrote:
> On Fri, Aug 26, 2022 at 01:10:39PM -0400, Alan Stern wrote:
> 
> > >  - some babbling about a missing propagation -- ISTR Linux if stuffed
> > >    full of them, specifically we require stores to auto propagate
> > >    without help from barriers
> > 
> > Not a missing propagation; a late one.
> > 
> > Don't understand what you mean by "auto propagate without help from 
> > barriers".
> 
> Linux hard relies on:
> 
> 	CPU0				CPU1
> 
> 	WRITE_ONCE(foo, 1);		while (!READ_ONCE(foo));
> 
> making forward progress.

Indeed yes.  As far as I can tell, this requirement is not explicitly 
mentioned in the LKMM, although it certainly is implicit.  I can't even 
think of a way to express it in a form Herd could verify.

> There were a few 'funny' uarchs that were broken, see for example commit
> a30718868915f.

Ha!  That commit should be a lesson in something, although I'm not sure 
what.  :-)

Alan