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

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Tue, Nov 26, 2013 at 01:02:18PM +0100, Ingo Molnar wrote:
> 
> * 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.

There actually is an open-source program designed to test this sort
of hypothesis...  http://diy.inria.fr/  Don't miss the advertisement
at the bottom of the page.

That said, you do need some machine time.  Some of the invalid hypotheses
have failure rates in the 1-in-a-billion range.  ;-)

Or you can read some of the papers that this group has written, some
of which include failure rates from empirical testing.  Here is the
one for ARM and Power:

http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf

							Thanx, Paul

--
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>