lkml.org 
[lkml]   [2020]   [Oct]   [5]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    From
    SubjectRE: Litmus test for question from Al Viro
    Date
    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@rowland.harvard.edu>
    > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
    >
    > 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.

    David

    -
    Registered Address Lakeside, Bramley Road, Mount Farm, Milton Keynes, MK1 1PT, UK
    Registration No: 1397386 (Wales)

    \
     
     \ /
      Last update: 2020-10-05 10:39    [W:2.567 / U:0.100 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site