Re: [GIT PULL tools] Linux kernel memory model

[Alan Stern]

On Sat, 3 Feb 2018, Paul E. McKenney wrote:

> Please see below for an initial patch to this effect.  This activity
> proved to be more productive than expected for these tests, which certainly
> supports our assertion that locking needs more testing...
> 
> MP+polocks.litmus
> MP+porevlocks.litmus
> 
> 	These are allowed by the current model, which surprised me a bit,
> 	given that even powerpc would forbid them.  Is the rationale
> 	that a lock-savvy compiler could pull accesses into the lock's
> 	critical section and then reorder those accesses?  Or does this
> 	constitute a bug in our model of locking?
> 
> 	(And these were allowed when I wrote recipes.txt, embarrassingly
> 	enough...)
> 
> Z6.0+pooncelock+poonceLock+pombonce.litmus
> 
> 	This was forbidden when I wrote recipes.txt, but now is allowed.
> 	The header comment for smp_mb__after_spinlock() makes it pretty
> 	clear that it must be forbidden.  So this one is a bug in our
> 	model of locking.

I just tried testing these under the most recent version of herd, and 
all three were forbidden.

Alan