Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18;
Subject: Re: Litmus test for question from Al Viro
To:     Alan Stern <stern@rowland.harvard.edu>,
        "Paul E. McKenney" <paulmck@kernel.org>
Cc:     parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
        boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
        j.alglave@ucl.ac.uk, luc.maranget@inria.fr, dlustig@nvidia.com,
        joel@joelfernandes.org, viro@zeniv.linux.org.uk,
        linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        Akira Yokosawa <akiyks@gmail.com>
References: <20201001045116.GA5014@paulmck-ThinkPad-P72>
 <20201001161529.GA251468@rowland.harvard.edu>
 <20201001213048.GF29330@paulmck-ThinkPad-P72>
 <20201003132212.GB318272@rowland.harvard.edu>
From:   Akira Yokosawa <akiyks@gmail.com>
Message-ID: <045c643f-6a70-dfdf-2b1e-f369a667f709@gmail.com>
Date:   Sun, 4 Oct 2020 00:16:31 +0900
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101
 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <20201003132212.GB318272@rowland.harvard.edu>
Content-Type: text/plain; charset=utf-8
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Precedence: bulk

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)
>