Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 08:36:51AM +0000, David Laight wrote:
> From: Paul E. McKenney
> > Sent: 05 October 2020 00:32
> ...
> >     manual/kernel: Add a litmus test with a hidden dependency
> > 
> >     This commit adds a litmus test that has a data dependency that can be
> >     hidden by control flow.  In this test, both the taken and the not-taken
> >     branches of an "if" statement must be accounted for in order to properly
> >     analyze the litmus test.  But herd7 looks only at individual executions
> >     in isolation, so fails to see the dependency.
> > 
> >     Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> >     Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
> > 
> > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 0000000..6baecf9
> > --- /dev/null
> > +++ b/manual/kernel/crypto-control-data.litmus
> > @@ -0,0 +1,31 @@
> > +C crypto-control-data
> > +(*
> > + * LB plus crypto-control-data plus data
> > + *
> > + * Result: Sometimes
> > + *
> > + * This is an example of OOTA and we would like it to be forbidden.
> > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > + * hidden by the form of the conditional control construct, hence the
> > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = 1;
> > +	if (READ_ONCE(*x) == 0)
> > +		r1 = 0;
> > +	WRITE_ONCE(*y, r1);
> > +}
> 
> Hmmm.... the compiler will semi-randomly transform that to/from:
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	else
> 		r1 = 1;
> and
> 	r1 = READ_ONCE(*x) != 0;
> 
> Both of which (probably) get correctly detected as a write to *y
> that is dependant on *x - so is 'problematic' with P1() which
> does the opposite assignment.
> 
> Which does rather imply that hurd is a bit broken.

I agree that herd7 does not match all compilers, but the intent was
always to approximate them.  There has been some research work towards
the goal of accurately modeling all possible compiler optimizations,
and it gets extremely complex, and thus computationally infeasible,
very quickly.  And we do need herd7 to stay strictly in the realm of
the computationally feasible.

Hence, any use of control dependencies should follow up with something
like klitmus7 (as Joel Fernandes did earlier in this thread) or KCSAN.
These tools have their own limitations, for example, using a specific
compiler rather than saying something about all possible compilers, but
they do reflect what a specific real toolchain actually does.  They are
also execution based, so have only some probability of finding problems.
In contrast, herd7 does the moral equivalent of a full state-space search.

It would be nice to be able to say that we have one tools that does
everything, but that might be a long way down the road.

							Thanx, Paul