Re: LKMM litmus test for Roman Penyaev's rcu-rr

[Alan Stern <stern@rowland.harvard.edu>]

On Wed, 30 May 2018, Paul E. McKenney wrote:

> > > My current guess is that we need to change the memory-model tool.  If
> > > that is the case, here are some possible resolutions:
> > > 
> > > 1.	Make herd's C-language control dependencies work the same as its
> > > 	assembly language, so that they extend beyond the end of the
> > > 	"if" statement.  I believe that this would make Roman's case
> > > 	work, but it could claim that other situations are safe that
> > > 	are actually problematic due to compiler optimizations.
> > > 
> > > 	The fact that the model currently handles only READ_ONCE()
> > > 	and WRITE_ONCE() and not unmarked reads and writes make this
> > > 	option more attractive than it otherwise be, compilers not
> > > 	being allowed to reorder volatile accesses, but we are likely
> > > 	to introduce unmarked accesses sometime in the future.
> > 
> > Preserving the order of volatile accesses isn't sufficient.  The
> > compiler is still allowed to translate
> > 
> > 	r1 = READ_ONCE(x);
> > 	if (r1) {
> > 		...
> > 	}
> > 	WRITE_ONCE(y, r2);
> > 
> > into something resembling
> > 
> > 	r1 = READ_ONCE(x);
> > 	WRITE_ONCE(y, r2);
> > 	if (r1) {
> > 		...
> > 	}
> > 
> > (provided the "..." part doesn't contain any volatile accesses,
> > barriers, or anything affecting r2), which would destroy any run-time
> > control dependency.  The CPU could then execute the write before the
> > read.
> 
> True, but almost all current litmus tests do have at least one volatile
> access in their "if" statements.  I am guessing that this has the same
> memory-model tooling issues as #2 below, but I am as usual happy to be
> proven wrong.  ;-)

It shouldn't be all that bad.  The dependencies are generated by herd,
meaning that the code would have to be changed to make control
dependencies extend beyond the ends of "if" statements.  I don't think
the necessary changes would be tremendously big, especially since the
LISA front end already behaves this way.

> > > 2.	Like #1 above, but only if something in one of the "if"'s
> > > 	branches would prevent the compiler from reordering
> > > 	(smp_mb(), synchronize_rcu(), value-returning non-relaxed
> > > 	RMW atomic, ...).  Easy for me to say, but I am guessing
> > > 	that much violence would be needed to the tooling to make
> > > 	this work.  ;-)
> > 
> > This would be my preference.  But I'm afraid it isn't practical at the 
> > moment.
> 
> I bet that some combination of scripting and smallish modifications to
> tooling could make it happen in reasonably short term.  Might be more
> difficult to make something more future-proof, though, agreed.

I have no idea what sort of scripting/smallish modifications could do 
the job.  You could ask Luc, if you're not afraid of giving him an 
aneurysm.  :-)

> > > If I understand Alan correctly, there is not an obvious way to make
> > > this change within the confines of the memory model's .bell and .cat
> > > files.
> > 
> > No way at all.  It would require significant changes to herd's internal 
> > workings and its external interface -- my original point.
> 
> I was afraid of that.  ;-)
> 
> Though truth be told, I was expecting an issue like this to crop up
> sooner rather than later, so I was actually getting a bit nervous
> about the fact that it had not yet shown itself...

The fact is, herd was never meant to act like a compiler.  Some 
disagreements are inevitable.

Alan