Hi Alan,
Just a minor nit in the litmus test.
On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> To expand on my statement about the LKMM's weakness regarding control
> constructs, here is a litmus test to illustrate the issue. You might
> want to add this to one of the archives.
>
> Alan
>
> C crypto-control-data
> (*
> * LB plus crypto-control-data plus data
> *
> * Expected result: allowed
> *
> * 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);
> }
>
> P1(int *x, int *y)
> {
> WRITE_ONCE(*x, READ_ONCE(*y));
Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
When I changed P1 to
P1(int *x, int *y)
{
int r1;
r1 = READ_ONCE(*y);
WRITE_ONCE(*x, r1);
}
and replaced the WRITE_ONCE() in P0 with smp_store_release(),
I got the result of:
-----
Test crypto-control-data Allowed
States 1
0:r1=0;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r1=1)
Observation crypto-control-data Never 0 3
Time crypto-control-data 0.01
Hash=9b9aebbaf945dad8183d2be0ccb88e11
-----
Restoring the WRITE_ONCE() in P0, I got the result of:
-----
Test crypto-control-data Allowed
States 2
0:r1=0;
0:r1=1;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (0:r1=1)
Observation crypto-control-data Sometimes 1 4
Time crypto-control-data 0.01
Hash=843eaa4974cec0efae79ce3cb73a1278
-----
As this is the same as the expected result, I suppose you have missed another
limitation of herd7 + LKMM.
By the way, I think this weakness on control dependency + data dependency
deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.
In the LIMITATIONS section, item #1 mentions some situation where
LKMM may not recognize possible losses of control-dependencies by
compiler optimizations.
What this litmus test demonstrates is a different class of mismatch.
Alan, can you come up with an update in this regard?
Thanks, Akira
> }
>
> exists (0:r1=1)
>
