Re: [PATCH v6 4/5] MCS Lock: Barrier corrections

[Ingo Molnar <mingo@kernel.org>]

* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:

> On Sat, Nov 23, 2013 at 12:24:50PM +0100, Ingo Molnar wrote:
> > 
> > * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote:
> > 
> > > > x86 does have that extra "Memory ordering obeys causality (memory 
> > > > ordering respects transitive visibility)." rule, and the example 
> > > > in the architecture manual (section 8.2.3.6 "Stores Are 
> > > > Transitively Visible") seems to very much about this, but your 
> > > > particular example is subtly different, so..
> > > 
> > > Indeed, my example needs CPU 1's -load- from y to be transitively 
> > > visible, so I am nervous about this one as well.
> > > 
> > > > I will have to ruminate on this.
> > > 
> > > The rules on the left-hand column of page 5 of the below URL apply 
> > > to this example more straightforwardly, but I don't know that Intel 
> > > and AMD stand behind them:
> > > 
> > > 	http://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf
> > > 
> > > My guess is that x86 does guarantee this ordering, but at this point 
> > > I would have to ask someone from Intel and AMD.
> > 
> > An additional option might be to create a user-space testcase 
> > engineered to hit all the exotic ordering situations, one that 
> > might disprove any particular assumptions we have about the 
> > behavior of hardware. (Back a decade ago when the x86 space first 
> > introduced quad core CPUs with newfangled on-die cache coherency I 
> > managed to demonstrate a causality violation by simulating kernel 
> > locks in user-space, which turned out to be a hardware bug. Also, 
> > when Hyperthreading/SMT was new it demonstrated many interesting 
> > bugs never seen in practice before. So running stuff on real 
> > hardware is useful.)
> > 
> > And a cache coherency (and/or locking) test suite would be very 
> > useful anyway, for so many other purposes as well: such as a new 
> > platform/CPU bootstrap, or to prove the correctness of some fancy 
> > new locking scheme people want to add. Maybe as an extension to 
> > rcutorture, or a generalization of it?
> 
> I have the locking counterpart of rcutorture on my todo list.  ;-)
> 
> Of course, we cannot prove locks correct via testing, but a quick 
> test can often find a bug faster and more reliably than manual 
> inspection.

We cannot prove them correct via testing, but we can test our 
hypothesis about how the platform works and chances are that if the 
tests are smart enough then we will be proven wrong via an actual 
failure if our assumptions are wrong.

Thanks,

	Ingo

--
To unsubscribe, send a message with 'unsubscribe linux-mm' in
the body to majordomo@kvack.org.  For more info on Linux MM,
see: http://www.linux-mm.org/ .
Don't email: <a href=mailto:"dont@kvack.org"> email@kvack.org </a>