Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

["Paul E. McKenney" <paulmck@kernel.org>]

On Mon, Oct 05, 2020 at 03:48:34PM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:
> > 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.
> 
> > (*
> >  * LB plus crypto-mb-data plus data.
> 
> The actual pattern is LB+mb+data.
> 
> >  *
> >  * 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.
> 
> >  *)
> > 
> > {}
> > 
> > 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 <stern@rowland.harvard.edu>
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.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

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
+(*
+ * LB plus crypto-mb-data plus data.
+ *
+ * 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)