On Tue, Oct 06, 2020 at 01:05:25PM -0400, Alan Stern wrote:

On Tue, Oct 06, 2020 at 09:39:54AM -0700, Paul E. McKenney wrote:

quoted

On Mon, Oct 05, 2020 at 03:48:34PM -0400, Alan Stern wrote:

quoted

On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:

quoted

Aside from naming and comment, how about my adding the following?

							Thanx, Paul

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

C crypto-control-data-1

Let's call it something more along the lines of 
dependencies-in-nested-expressions.  Maybe you can think of something a 
little more succinct, but that's the general idea of the test.

quoted

(*
 * LB plus crypto-mb-data plus data.

The actual pattern is LB+mb+data.

quoted

 *
 * Result: Never
 *
 * This is an example of OOTA and we would like it to be forbidden.
 * If you want herd7 to get the right answer, you must use herdtools
 * 0f3f8188a326 (" [herd] Fix dependency definition") or later.

Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency 
definition") recognize data dependencies only when they flow through an 
intermediate local variable.  Since the dependency in P1 doesn't, those
versions get the wrong answer for this test.

quoted

 *)

{}

P0(int *x, int *y)
{
	int r1;

	r1 = READ_ONCE(*x);
	smp_mb();
	WRITE_ONCE(*y, r1);
}

P1(int *x, int *y)
{
	int r2;

No need for r2.

Thank you for looking this over!

Like this, then?

							Thanx, Paul

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

commit 51898676302d8ebc93856209f7c587f1ac0fdd11
Author: Alan Stern [off-list ref]
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB+mb+data litmus test
    
    Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
    definition") recognize data dependencies only when they flow through an
    intermediate local variable.  Since the dependency in P1 doesn't, those
    versions get the wrong answer for this test.

Shouldn't the commit message be different from the actual contents of 
the update?  It's supposed to explain why the update was made, not just 
say what it does.  How about this:

Test whether herd7 can detect a data dependency when there is no 
intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).  
Commit 0f3f8188a326 fixed an oversight which caused such dependencies 
to be missed.

Much better, thank you!  I added "in herdtools" just in case someone was
confused enough to look for this commit in the Linux kernel or some such.
Which I should have done more explicitly in the original, to be sure.

quoted

    Signed-off-by: Alan Stern [off-list ref]
    Signed-off-by: Paul E. McKenney [off-list ref]

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..673eec9
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus

@@ -0,0 +1,29 @@
+C LB+mb+data.litmus

Do you normally put ".litmus" at the end of test names?  I leave it out, 
including it only in the filename.

No, I don't, and thank you for catching this.

quoted

+(*
+ * LB plus crypto-mb-data plus data.

As I said earlier, the actual pattern is LB+mb+data.  There's nothing 
"crypto" about this litmus test (for example, no control dependencies).

Besides, it hardly seems worthwhile making the first comment line a 
repeat of the test name immediately above it.  Just leave it out.

Done!  ;-)

quoted

+ *
+ * Result: Never
+ *
+ * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
+ * definition") recognize data dependencies only when they flow through
+ * an intermediate local variable.  Since the dependency in P1 doesn't,
+ * those versions get the wrong answer for this test.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Otherwise okay.

And here is the updated version.

							Thanx, Paul

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

commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
Author: Alan Stern [off-list ref]
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB+mb+data litmus test
    
    Test whether herd7 can detect a data dependency when there is no
    intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
    Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
    dependencies to be missed.
    
    Signed-off-by: Alan Stern [off-list ref]
    Signed-off-by: Paul E. McKenney [off-list ref]

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..0cf9a7a
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus

@@ -0,0 +1,27 @@
+C LB+mb+data
+(*
+ * Result: Never
+ *
+ * Test whether herd7 can detect a data dependency when there is no
+ * intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
+ * Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
+ * dependencies to be missed.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)