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: Sun, 4 Oct 2020 16:31:46 -0700 [thread overview]
Message-ID: <20201004233146.GP29330@paulmck-ThinkPad-P72> (raw)
In-Reply-To: <20201003132212.GB318272@rowland.harvard.edu>
On Sat, Oct 03, 2020 at 09:22:12AM -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));
> }
>
> exists (0:r1=1)
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)
next prev parent reply other threads:[~2020-10-04 23:31 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 ` Paul E. McKenney [this message]
2020-10-05 2:38 ` Litmus test for question from Al Viro 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
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=20201004233146.GP29330@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.