All of lore.kernel.org
 help / color / mirror / Atom feed
From: "Paul E. McKenney" <paulmck@kernel.org>
To: Alan Stern <stern@rowland.harvard.edu>
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, akiyks@gmail.com,
	dlustig@nvidia.com, joel@joelfernandes.org,
	viro@zeniv.linux.org.uk, linux-kernel@vger.kernel.org,
	linux-arch@vger.kernel.org
Subject: Re: Litmus test for question from Al Viro
Date: Mon, 5 Oct 2020 07:03:53 -0700	[thread overview]
Message-ID: <20201005140353.GW29330@paulmck-ThinkPad-P72> (raw)
In-Reply-To: <20201005023846.GA359428@rowland.harvard.edu>

On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > Nice simple example!  How about like this?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Sun Oct 4 16:27:03 2020 -0700
> > 
> >     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);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > +}
> > +
> > +exists (0:r1=1)
> 
> Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> 
> P1(int *x, int *y)
> {
> 	int r2;
> 
> 	r = READ_ONCE(*y);
> 	WRITE_ONCE(*x, r2);
> }
> 
> Other than that, this is fine.

Updated as suggested by Will, like this?

							Thanx, Paul

------------------------------------------------------------------------

commit adf43667b702582331d68acdf3732a6a017a182c
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Sun Oct 4 16:27:03 2020 -0700

    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..cdcdec9
--- /dev/null
+++ b/manual/kernel/crypto-control-data.litmus
@@ -0,0 +1,34 @@
+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);
+}
+
+P1(int *x, int *y)
+{
+	int r2;
+
+	r2 = READ_ONCE(*y);
+	WRITE_ONCE(*x, r2);
+}
+
+exists (0:r1=1)

  parent reply	other threads:[~2020-10-05 14:03 UTC|newest]

Thread overview: 52+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-10-01  4:51 Litmus test for question from Al Viro Paul E. McKenney
2020-10-01 16:15 ` Alan Stern
2020-10-01 16:36   ` Al Viro
2020-10-01 18:39     ` Alan Stern
2020-10-01 19:29       ` Al Viro
2020-10-01 21:30   ` Paul E. McKenney
2020-10-03  2:01     ` Alan Stern
2020-10-03 13:22     ` Alan Stern
2020-10-03 15:16       ` Akira Yokosawa
2020-10-03 17:13         ` Bug in herd7 [Was: Re: Litmus test for question from Al Viro] Alan Stern
2020-10-03 22:50           ` Akira Yokosawa
2020-10-04  1:40           ` [PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies Alan Stern
2020-10-04 21:07             ` joel
2020-10-04 23:12               ` Paul E. McKenney
2020-10-05 15:15           ` Bug in herd7 [Was: Re: Litmus test for question from Al Viro] Luc Maranget
2020-10-05 15:53             ` Alan Stern
2020-10-05 16:52               ` Paul E. McKenney
2020-10-05 18:19                 ` Alan Stern
2020-10-05 19:18                   ` Paul E. McKenney
2020-10-05 19:48                     ` Alan Stern
2020-10-06 16:39                       ` Paul E. McKenney
2020-10-06 17:05                         ` Alan Stern
2020-10-07 17:50                           ` Paul E. McKenney
2020-10-07 19:40                             ` Alan Stern
2020-10-07 22:38                               ` Paul E. McKenney
2020-10-08  2:25                                 ` Alan Stern
2020-10-08  2:50                                   ` Paul E. McKenney
2020-10-08 14:01                                     ` Alan Stern
2020-10-08 18:32                                       ` Paul E. McKenney
2020-10-05 15:54             ` Paul E. McKenney
2020-10-04 23:31       ` Litmus test for question from Al Viro Paul E. McKenney
2020-10-05  2:38         ` Alan Stern
2020-10-05  8:20           ` Will Deacon
2020-10-05  9:12             ` Will Deacon
2020-10-05 14:01               ` Paul E. McKenney
2020-10-05 14:23               ` Alan Stern
2020-10-05 15:13                 ` Will Deacon
2020-10-05 15:16                   ` Alan Stern
2020-10-05 15:35                     ` Peter Zijlstra
2020-10-05 15:49                       ` Paul E. McKenney
2020-10-05 14:16             ` Alan Stern
2020-10-05 14:03           ` Paul E. McKenney [this message]
2020-10-05 14:24             ` Alan Stern
2020-10-05 14:44             ` joel
2020-10-05 15:55               ` Paul E. McKenney
2020-10-05  8:36         ` David Laight
2020-10-05 13:59           ` Paul E. McKenney
2020-10-03 16:08     ` joel
2020-10-03 16:11       ` joel
2020-10-04 23:13         ` Paul E. McKenney
2020-10-03  2:35   ` Jon Masters
2020-10-04 23:32     ` Paul E. McKenney

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20201005140353.GW29330@paulmck-ThinkPad-P72 \
    --to=paulmck@kernel.org \
    --cc=akiyks@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=dhowells@redhat.com \
    --cc=dlustig@nvidia.com \
    --cc=j.alglave@ucl.ac.uk \
    --cc=joel@joelfernandes.org \
    --cc=linux-arch@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=luc.maranget@inria.fr \
    --cc=npiggin@gmail.com \
    --cc=parri.andrea@gmail.com \
    --cc=peterz@infradead.org \
    --cc=stern@rowland.harvard.edu \
    --cc=viro@zeniv.linux.org.uk \
    --cc=will@kernel.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.