lkml.org 
[lkml]   [2020]   [Oct]   [3]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
SubjectRe: Litmus test for question from Al Viro
From
Date
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)
>

\
 
 \ /
  Last update: 2020-10-03 17:17    [W:0.152 / U:1.592 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site