Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Thu, Oct 08, 2020 at 10:01:48AM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 07:50:25PM -0700, Paul E. McKenney wrote:
> > There are some distractions at the moment.
> >
> > Please see below. If this is not exactly correct, I will use "git rm"
> > and let you submit the patch as you wish.
> >
> > Thanx, Paul
> >
> >
> >
> > commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
> > Author: Alan Stern
> > Date: Tue Oct 6 09:38:37 2020 -0700
> >
> > manual/kernel: Add LB data dependency test with no intermediate variable
> >
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/C-LB+mb+data.litmus
> > b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 000..e9e24e0
> > --- /dev/null
> > +++ b/manual/kernel/C-LB+mb+data.litmus
> > @@ -0,0 +1,27 @@
> > +C LB+mb+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)
>
> Okay, that's exactly what it should be. :-)
Whew!!! ;-)
Thanx, Paul
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Wed, Oct 07, 2020 at 07:50:25PM -0700, Paul E. McKenney wrote:
> There are some distractions at the moment.
>
> Please see below. If this is not exactly correct, I will use "git rm"
> and let you submit the patch as you wish.
>
> Thanx, Paul
>
>
>
> commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
> Author: Alan Stern
> Date: Tue Oct 6 09:38:37 2020 -0700
>
> manual/kernel: Add LB data dependency test with no intermediate variable
>
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/C-LB+mb+data.litmus
> b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 000..e9e24e0
> --- /dev/null
> +++ b/manual/kernel/C-LB+mb+data.litmus
> @@ -0,0 +1,27 @@
> +C LB+mb+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)
Okay, that's exactly what it should be. :-)
Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Wed, Oct 07, 2020 at 10:25:37PM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 03:38:51PM -0700, Paul E. McKenney wrote:
> > On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote:
> > > On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> > > > And here is the updated version.
> > > >
> > > > Thanx, Paul
> > > >
> > > >
> > > >
> > > > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> > > > Author: Alan Stern
> > > > Date: Tue Oct 6 09:38:37 2020 -0700
> > > >
> > > > manual/kernel: Add LB+mb+data litmus test
> > >
> > > Let's change this to:
> > >
> > > manual/kernel: Add LB data dependency test with no intermediate
> > > variable
> > >
> > > Without that extra qualification, people reading just the title would
> > > wonder why we need a simple LB litmus test in the archive.
>
> > I might get this right sooner or later. You never know.
> >
> > Like this?
> >
> > Thanx, Paul
>
> Paul, I think you must need new reading glasses. You completely missed
> the text above.
There are some distractions at the moment.
Please see below. If this is not exactly correct, I will use "git rm"
and let you submit the patch as you wish.
Thanx, Paul
commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
Author: Alan Stern
Date: Tue Oct 6 09:38:37 2020 -0700
manual/kernel: Add LB data dependency test with no intermediate variable
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
Signed-off-by: Paul E. McKenney
diff --git a/manual/kernel/C-LB+mb+data.litmus
b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 000..e9e24e0
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,27 @@
+C LB+mb+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)
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Wed, Oct 07, 2020 at 03:38:51PM -0700, Paul E. McKenney wrote: > On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote: > > On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote: > > > And here is the updated version. > > > > > > Thanx, Paul > > > > > > > > > > > > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228 > > > Author: Alan Stern > > > Date: Tue Oct 6 09:38:37 2020 -0700 > > > > > > manual/kernel: Add LB+mb+data litmus test > > > > Let's change this to: > > > > manual/kernel: Add LB data dependency test with no intermediate > > variable > > > > Without that extra qualification, people reading just the title would > > wonder why we need a simple LB litmus test in the archive. > I might get this right sooner or later. You never know. > > Like this? > > Thanx, Paul Paul, I think you must need new reading glasses. You completely missed the text above. Alan > > > commit 5b6a4ff2c8ad25fc77f4151e71e6cbd8f3268d7b > Author: Alan Stern > 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 > Signed-off-by: Paul E. McKenney
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> > And here is the updated version.
> >
> > Thanx, Paul
> >
> >
> >
> > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> > Author: Alan Stern
> > Date: Tue Oct 6 09:38:37 2020 -0700
> >
> > manual/kernel: Add LB+mb+data litmus test
>
> Let's change this to:
>
> manual/kernel: Add LB data dependency test with no intermediate variable
>
> Without that extra qualification, people reading just the title would
> wonder why we need a simple LB litmus test in the archive.
>
> >
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/C-LB+mb+data.litmus
> > b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 000..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.
>
> You changed this comment! It should have remained the way it was:
I might get this right sooner or later. You never know.
Like this?
Thanx, Paul
commit 5b6a4ff2c8ad25fc77f4151e71e6cbd8f3268d7b
Author: Alan Stern
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
Signed-off-by: Paul E. McKenney
diff --git a/manual/kernel/C-LB+mb+data.litmus
b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 000..e9e24e0
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,27 @@
+C LB+mb+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)
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> And here is the updated version.
>
> Thanx, Paul
>
>
>
> commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> Author: Alan Stern
> Date: Tue Oct 6 09:38:37 2020 -0700
>
> manual/kernel: Add LB+mb+data litmus test
Let's change this to:
manual/kernel: Add LB data dependency test with no intermediate variable
Without that extra qualification, people reading just the title would
wonder why we need a simple LB litmus test in the archive.
>
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/C-LB+mb+data.litmus
> b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 000..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.
You changed this comment! It should have remained the way it was:
+ * 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)
Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
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:
> > 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
> > 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.
> > Signed-off-by: Alan Stern
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/C-LB+mb+data.litmus
> > b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 000..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.
> > +(*
> > + * 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! ;-)
> > + *
> > + * 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
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
inte
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Tue, Oct 06, 2020 at 09:39:54AM -0700, Paul E. McKenney wrote:
> 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
> 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.
> Signed-off-by: Alan Stern
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/C-LB+mb+data.litmus
> b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 000..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.
> +(*
> + * 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.
> + *
> + * 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.
Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
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
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
Signed-off-by: Paul E. McKenney
diff --git a/manual/kernel/C-LB+mb+data.litmus
b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 000..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)
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
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.
>
> WRITE_ONCE(*x, READ_ONCE(*y));
> }
>
> exists (0:r1=1)
Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Mon, Oct 05, 2020 at 02:19:49PM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 09:52:23AM -0700, Paul E. McKenney wrote:
> > On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> > > I tested the new commit -- it does indeed fix the problem.
> >
> > Beat me to it, very good! ;-)
> >
> > But were you using the crypto-control-data litmus test?
>
> I was not. The test I used was what you get by starting from the
> version of crypto-control-data that had the one-liner in P1, and then
> replacing P0 with:
>
> P0(int *x, int *y)
> {
> int r1;
>
> r1 = READ_ONCE(*x);
> smp_mb();
> WRITE_ONCE(*y, 1);
> }
>
> Without the new commit this test is allowed; with the new commit it
> isn't (as we would expect). Also, the graphical output from herd7 shows
> the data dependency in P1 with the commit, and doesn't show it without
> the commit.
>
> > That one still
> > gets me Sometimes:
> >
> > $ herd7 -version
> > 7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
> > $ herd7 -conf linux-kernel.cfg
> > ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
> > 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.00
> > Hash=10898119bac87e11f31dc22bbb7efe17
> >
> > Or did I mess something up?
>
> You didn't mess up anything. That's the whole point of this litmus
> test: It should be forbidden because it is an example of OOTA, but LKMM
> allows it. Even with Luc's new commit.
OK, got it.
Aside from naming and comment, how about my adding the following?
Thanx, Paul
C crypto-control-data-1
(*
* LB plus crypto-mb-data plus 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.
*)
{}
P0(int *x, int *y)
{
int r1;
r1 = READ_ONCE(*x);
smp_mb();
WRITE_ONCE(*y, r1);
}
P1(int *x, int *y)
{
int r2;
WRITE_ONCE(*x, READ_ONCE(*y));
}
exists (0:r1=1)
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Mon, Oct 05, 2020 at 09:52:23AM -0700, Paul E. McKenney wrote:
> On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> > I tested the new commit -- it does indeed fix the problem.
>
> Beat me to it, very good! ;-)
>
> But were you using the crypto-control-data litmus test?
I was not. The test I used was what you get by starting from the
version of crypto-control-data that had the one-liner in P1, and then
replacing P0 with:
P0(int *x, int *y)
{
int r1;
r1 = READ_ONCE(*x);
smp_mb();
WRITE_ONCE(*y, 1);
}
Without the new commit this test is allowed; with the new commit it
isn't (as we would expect). Also, the graphical output from herd7 shows
the data dependency in P1 with the commit, and doesn't show it without
the commit.
> That one still
> gets me Sometimes:
>
> $ herd7 -version
> 7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
> $ herd7 -conf linux-kernel.cfg
> ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
> 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.00
> Hash=10898119bac87e11f31dc22bbb7efe17
>
> Or did I mess something up?
You didn't mess up anything. That's the whole point of this litmus
test: It should be forbidden because it is an example of OOTA, but LKMM
allows it. Even with Luc's new commit.
Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > > > 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.
> > >
> > > You're right. This is definitely a bug in herd7.
> > >
> > > Luc, were you aware of this?
> >
> > Hi Alan,
> >
> > No I was not aware of it. Now I am, the bug is normally fixed in the master
> > branch of herd git deposit.
> >
> >
> > Thanks for the report.
>
> I tested the new commit -- it does indeed fix the problem.
Beat me to it, very good! ;-)
But were you using the crypto-control-data litmus test? That one still
gets me Sometimes:
$ herd7 -version
7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
$ herd7 -conf linux-kernel.cfg
~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
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.00
Hash=10898119bac87e11f31dc22bbb7efe17
Or did I mess something up?
Thanx, Paul
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 10:44:22AM -0400, j...@joelfernandes.org wrote:
> On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> > 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
> > > > 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
> > > > Signed-off-by: Paul E. McKenney
> > > >
> > > > diff --git a/manual/kernel/crypto-control-data.litmus
> > > > b/manual/kernel/crypto-control-data.litmus
> > > > new file mode 100644
> > > > index 000..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?
>
> LGTM as well,
>
> FWIW:
> Reviewed-by: Joel Fernandes (Google)
Applied, thank you all!
This has been pushed to my github litmus archive.
Thanx, Paul
> thanks,
>
> - Joel
>
> >
> > Thanx, Paul
> >
> >
> >
> > commit adf43667b702582331d68acdf3732a6a017a182c
> > Author: Alan Stern
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/crypto-control-data.litmus
> > b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 000..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
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > 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.
> >
> > You're right. This is definitely a bug in herd7.
> >
> > Luc, were you aware of this?
>
> Hi Alan,
>
> No I was not aware of it. Now I am, the bug is normally fixed in the master
> branch of herd git deposit.
>
>
> Thanks for the report.
Thank you very much, Luc! I will rebuild and give it a try.
Thanx, Paul
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > > 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.
> >
> > You're right. This is definitely a bug in herd7.
> >
> > Luc, were you aware of this?
>
> Hi Alan,
>
> No I was not aware of it. Now I am, the bug is normally fixed in the master
> branch of herd git deposit.
>
>
> Thanks for the report.
I tested the new commit -- it does indeed fix the problem.
Thanks.
Alan
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 05:35:19PM +0200, Peter Zijlstra wrote: > On Mon, Oct 05, 2020 at 11:16:39AM -0400, Alan Stern wrote: > > On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote: > > > > The failure to recognize the dependency in P0 should be considered a > > > > combined limitation of the memory model and herd7. It's not a simple > > > > mistake that can be fixed by a small rewrite of herd7; rather it's a > > > > deliberate choice we made based on herd7's inherent design. We > > > > explicitly said that control dependencies extend only to the code in > > > > the > > > > branches of an "if" statement; anything beyond the end of the statement > > > > is not considered to be dependent. > > > > > > Interesting. How does this interact with loops that are conditionally > > > broken > > > out of, e.g. a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call > > > prior to a WRITE_ONCE()? > > > > Heh -- We finesse this issue by not supporting loops at all! :-) > > Right, so something like: > > smp_cond_load_relaxed(x, !VAL); > WRITE_ONCE(*y, 1); > > Would be modeled like: > > r1 = READ_ONCE(*x); > if (!r1) > WRITE_ONCE(*y, 1); > > with an r1==0 constraint in the condition I suppose ? Yes, you got it! However, it is more efficient to use the "filter" clause to tell herd7 about executions that are to be discarded. Thanx, Paul
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 11:16:39AM -0400, Alan Stern wrote: > On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote: > > > The failure to recognize the dependency in P0 should be considered a > > > combined limitation of the memory model and herd7. It's not a simple > > > mistake that can be fixed by a small rewrite of herd7; rather it's a > > > deliberate choice we made based on herd7's inherent design. We > > > explicitly said that control dependencies extend only to the code in the > > > branches of an "if" statement; anything beyond the end of the statement > > > is not considered to be dependent. > > > > Interesting. How does this interact with loops that are conditionally broken > > out of, e.g. a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call > > prior to a WRITE_ONCE()? > > Heh -- We finesse this issue by not supporting loops at all! :-) Right, so something like: smp_cond_load_relaxed(x, !VAL); WRITE_ONCE(*y, 1); Would be modeled like: r1 = READ_ONCE(*x); if (!r1) WRITE_ONCE(*y, 1); with an r1==0 constraint in the condition I suppose ?
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote: > > The failure to recognize the dependency in P0 should be considered a > > combined limitation of the memory model and herd7. It's not a simple > > mistake that can be fixed by a small rewrite of herd7; rather it's a > > deliberate choice we made based on herd7's inherent design. We > > explicitly said that control dependencies extend only to the code in the > > branches of an "if" statement; anything beyond the end of the statement > > is not considered to be dependent. > > Interesting. How does this interact with loops that are conditionally broken > out of, e.g. a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call > prior to a WRITE_ONCE()? Heh -- We finesse this issue by not supporting loops at all! :-) Alan
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
> On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > 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.
>
> You're right. This is definitely a bug in herd7.
>
> Luc, were you aware of this?
Hi Alan,
No I was not aware of it. Now I am, the bug is normally fixed in the master
branch of herd git deposit.
Thanks for the report.
--Luc
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 10:23:51AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> > On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > > 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);
> > >
> > > (r2?)
> > >
> > > > WRITE_ONCE(*x, r2);
> > > > }
> > > >
> > > > Other than that, this is fine.
> > >
> > > But yes, module the typo, I agree that this rewrite is much better than
> > > the
> > > proposal above. The definition of control dependencies on arm64 (per the
> > > Arm
> > > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > > executed on both paths of the branch, and I believe there are ongoing
> > > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > > from the "bug in herd" topic to avoid extra confusion.
> >
> > Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> > about claiming that this is a bug in herd without input from Jade or Luc,
> > as it does unfortunately tie into the definition of control dependencies
> > and it could be a deliberate choice.
>
> I think you misunderstood. The bug in herd7 affects the way it handles
> P1, not P0. With
>
> r2 = READ_ONCE(*y);
> WRITE_ONCE(*x, r2);
>
> herd7 generates a data dependency from the read to the write. With
>
> WRITE_ONCE(*x, READ_ONCE(*y));
>
> it doesn't generate any dependency, even though the code does exactly
> the same thing as far as the memory model is concerned. That's the bug
> I was referring to.
Thanks, that clears things up. There were lots of mentions of "control
dependency" in the mail thread that threw me, because this bug is clearly
about data dependencies!
> The failure to recognize the dependency in P0 should be considered a
> combined limitation of the memory model and herd7. It's not a simple
> mistake that can be fixed by a small rewrite of herd7; rather it's a
> deliberate choice we made based on herd7's inherent design. We
> explicitly said that control dependencies extend only to the code in the
> branches of an "if" statement; anything beyond the end of the statement
> is not considered to be dependent.
Interesting. How does this interact with loops that are conditionally broken
out of, e.g. a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
prior to a WRITE_ONCE()?
Will
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> 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
> > > 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
> > > Signed-off-by: Paul E. McKenney
> > >
> > > diff --git a/manual/kernel/crypto-control-data.litmus
> > > b/manual/kernel/crypto-control-data.litmus
> > > new file mode 100644
> > > index 000..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?
LGTM as well,
FWIW:
Reviewed-by: Joel Fernandes (Google)
thanks,
- Joel
>
> Thanx, Paul
>
>
>
> commit adf43667b702582331d68acdf3732a6a017a182c
> Author: Alan Stern
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/crypto-control-data.litmus
> b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 000..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)
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> Updated as suggested by Will, like this?
>
> Thanx, Paul
>
>
>
> commit adf43667b702582331d68acdf3732a6a017a182c
> Author: Alan Stern
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/crypto-control-data.litmus
> b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 000..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)
Perfect!
Alan
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > 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);
> >
> > (r2?)
> >
> > > WRITE_ONCE(*x, r2);
> > > }
> > >
> > > Other than that, this is fine.
> >
> > But yes, module the typo, I agree that this rewrite is much better than the
> > proposal above. The definition of control dependencies on arm64 (per the Arm
> > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > executed on both paths of the branch, and I believe there are ongoing
> > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > from the "bug in herd" topic to avoid extra confusion.
>
> Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> about claiming that this is a bug in herd without input from Jade or Luc,
> as it does unfortunately tie into the definition of control dependencies
> and it could be a deliberate choice.
I think you misunderstood. The bug in herd7 affects the way it handles
P1, not P0. With
r2 = READ_ONCE(*y);
WRITE_ONCE(*x, r2);
herd7 generates a data dependency from the read to the write. With
WRITE_ONCE(*x, READ_ONCE(*y));
it doesn't generate any dependency, even though the code does exactly
the same thing as far as the memory model is concerned. That's the bug
I was referring to.
The failure to recognize the dependency in P0 should be considered a
combined limitation of the memory model and herd7. It's not a simple
mistake that can be fixed by a small rewrite of herd7; rather it's a
deliberate choice we made based on herd7's inherent design. We
explicitly said that control dependencies extend only to the code in the
branches of an "if" statement; anything beyond the end of the statement
is not considered to be dependent.
Alan
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > 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);
>
> (r2?)
Oops, yes, thank you.
> > WRITE_ONCE(*x, r2);
> > }
> >
> > Other than that, this is fine.
>
> But yes, module the typo, I agree that this rewrite is much better than the
> proposal above. The definition of control dependencies on arm64 (per the Arm
> ARM [1]) isn't entirely clear that it provides order if the WRITE is
> executed on both paths of the branch, and I believe there are ongoing
> efforts to try to tighten that up.
Do you mean that people aren't yet in agreement about what the answer
should be?
How can the CPU tell whether a write is executed on both branches?
Speculatively execute both and see if they both reach the same write
instruction? What if the same instruction is reached on both branches
but the values written or the addresses written to are different?
> I'd rather keep _that_ topic separate
> from the "bug in herd" topic to avoid extra confusion.
Indeed.
Alan
Re: Litmus test for question from Al Viro
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
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/crypto-control-data.litmus
> > b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 000..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
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
Signed-off-by: Paul E. McKenney
diff --git a/manual/kernel/crypto-control-data.litmus
b/manual/kernel/crypto-control-data.litmus
new file mode 100644
index 000..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)
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > 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
> > > > 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
> > > > Signed-off-by: Paul E. McKenney
> > > >
> > > > diff --git a/manual/kernel/crypto-control-data.litmus
> > > > b/manual/kernel/crypto-control-data.litmus
> > > > new file mode 100644
> > > > index 000..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);
> >
> > (r2?)
> >
> > > WRITE_ONCE(*x, r2);
> > > }
> > >
> > > Other than that, this is fine.
> >
> > But yes, module the typo, I agree that this rewrite is much better than the
> > proposal above. The definition of control dependencies on arm64 (per the Arm
> > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > executed on both paths of the branch, and I believe there are ongoing
> > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > from the "bug in herd" topic to avoid extra confusion.
>
> Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> about claiming that this is a bug in herd without input from Jade or Luc,
> as it does unfortunately tie into the definition of control dependencies
> and it could be a deliberate choice.
>
> Jade, Luc: apparently herd doesn't emit a control dependency edge from
> the READ_ONCE() to the WRITE_ONCE() in the following:
>
>
> P0(int *x, int *y)
> {
> int r1;
>
> r1 = 1;
> if (READ_ONCE(*x) == 0)
> r1 = 0;
> WRITE_ONCE(*y, r1);
> }
>
>
> Is that deliberate?
>
> Setting the arm64 architecture aside for one moment, I think the Linux
> memory model would very much like the control dependency to exist in this
> case. Documenting the unexpected outcome is one thing, but I think it would
> be much better to do it in a way where users can reason about whether or not
> they're falling into this trap rather than warning them that the results may
> be unreliable, which is not likely to build confidence in the tool.
It was in fact a deliberate choice. Exact modeling of what compilers can
and cannot do gets extremely computationally intensive very quickly given
the current state of the art.
Thanx, Paul
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 08:36:51AM +, David Laight wrote:
> From: Paul E. McKenney
> > Sent: 05 October 2020 00:32
> ...
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/crypto-control-data.litmus
> > b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 000..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);
> > +}
>
> Hmmm the compiler will semi-randomly transform that to/from:
> if (READ_ONCE(*x) == 0)
> r1 = 0;
> else
> r1 = 1;
> and
> r1 = READ_ONCE(*x) != 0;
>
> Both of which (probably) get correctly detected as a write to *y
> that is dependant on *x - so is 'problematic' with P1() which
> does the opposite assignment.
>
> Which does rather imply that hurd is a bit broken.
I agree that herd7 does not match all compilers, but the intent was
always to approximate them. There has been some research work towards
the goal of accurately modeling all possible compiler optimizations,
and it gets extremely complex, and thus computationally infeasible,
very quickly. And we do need herd7 to stay strictly in the realm of
the computationally feasible.
Hence, any use of control dependencies should follow up with something
like klitmus7 (as Joel Fernandes did earlier in this thread) or KCSAN.
These tools have their own limitations, for example, using a specific
compiler rather than saying something about all possible compilers, but
they do reflect what a specific real toolchain actually does. They are
also execution based, so have only some probability of finding problems.
In contrast, herd7 does the moral equivalent of a full state-space search.
It would be nice to be able to say that we have one tools that does
everything, but that might be a long way down the road.
Thanx, Paul
Re: Litmus test for question from Al Viro
On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> 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
> > > 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
> > > Signed-off-by: Paul E. McKenney
> > >
> > > diff --git a/manual/kernel/crypto-control-data.litmus
> > > b/manual/kernel/crypto-control-data.litmus
> > > new file mode 100644
> > > index 000..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);
>
> (r2?)
>
> > WRITE_ONCE(*x, r2);
> > }
> >
> > Other than that, this is fine.
>
> But yes, module the typo, I agree that this rewrite is much better than the
> proposal above. The definition of control dependencies on arm64 (per the Arm
> ARM [1]) isn't entirely clear that it provides order if the WRITE is
> executed on both paths of the branch, and I believe there are ongoing
> efforts to try to tighten that up. I'd rather keep _that_ topic separate
> from the "bug in herd" topic to avoid extra confusion.
Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
about claiming that this is a bug in herd without input from Jade or Luc,
as it does unfortunately tie into the definition of control dependencies
and it could be a deliberate choice.
Jade, Luc: apparently herd doesn't emit a control dependency edge from
the READ_ONCE() to the WRITE_ONCE() in the following:
P0(int *x, int *y)
{
int r1;
r1 = 1;
if (READ_ONCE(*x) == 0)
r1 = 0;
WRITE_ONCE(*y, r1);
}
Is that deliberate?
Setting the arm64 architecture aside for one moment, I think the Linux
memory model would very much like the control dependency to exist in this
case. Documenting the unexpected outcome is one thing, but I think it would
be much better to do it in a way where users can reason about whether or not
they're falling into this trap rather than warning them that the results may
be unreliable, which is not likely to build confidence in the tool.
Will
RE: Litmus test for question from Al Viro
From: Paul E. McKenney
> Sent: 05 October 2020 00:32
...
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/crypto-control-data.litmus
> b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 000..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);
> +}
Hmmm the compiler will semi-randomly transform that to/from:
if (READ_ONCE(*x) == 0)
r1 = 0;
else
r1 = 1;
and
r1 = READ_ONCE(*x) != 0;
Both of which (probably) get correctly detected as a write to *y
that is dependant on *x - so is 'problematic' with P1() which
does the opposite assignment.
Which does rather imply that hurd is a bit broken.
David
-
Registered Address Lakeside, Bramley Road, Mount Farm, Milton Keynes, MK1 1PT,
UK
Registration No: 1397386 (Wales)
Re: Litmus test for question from Al Viro
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
> > 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
> > Signed-off-by: Paul E. McKenney
> >
> > diff --git a/manual/kernel/crypto-control-data.litmus
> > b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 000..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);
(r2?)
> WRITE_ONCE(*x, r2);
> }
>
> Other than that, this is fine.
But yes, module the typo, I agree that this rewrite is much better than the
proposal above. The definition of control dependencies on arm64 (per the Arm
ARM [1]) isn't entirely clear that it provides order if the WRITE is
executed on both paths of the branch, and I believe there are ongoing
efforts to try to tighten that up. I'd rather keep _that_ topic separate
from the "bug in herd" topic to avoid extra confusion.
Will
[1] https://developer.arm.com/documentation/ddi0487/fc/
Re: Litmus test for question from Al Viro
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
> 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
> Signed-off-by: Paul E. McKenney
>
> diff --git a/manual/kernel/crypto-control-data.litmus
> b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 000..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.
Alan
Re: Litmus test for question from Al Viro
On Fri, Oct 02, 2020 at 10:35:45PM -0400, Jon Masters wrote:
> On 10/1/20 12:15 PM, Alan Stern wrote:
> > On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > > Hello!
> > >
> > > Al Viro posted the following query:
> > >
> > >
> > >
> > > fun question regarding barriers, if you have time for that
> > > V->A = V->B = 1;
> > >
> > > CPU1:
> > > to_free = NULL
> > > spin_lock(&LOCK)
> > > if (!smp_load_acquire(&V->B))
> > > to_free = V
> > > V->A = 0
> > > spin_unlock(&LOCK)
> > > kfree(to_free)
> > >
> > > CPU2:
> > > to_free = V;
> > > if (READ_ONCE(V->A)) {
> > > spin_lock(&LOCK)
> > > if (V->A)
> > > to_free = NULL
> > > smp_store_release(&V->B, 0);
> > > spin_unlock(&LOCK)
> > > }
> > > kfree(to_free);
> > > 1) is it guaranteed that V will be freed exactly once and that
> > > no accesses to *V will happen after freeing it?
> > > 2) do we need smp_store_release() there? I.e. will anything
> > > break if it's replaced with plain V->B = 0?
> >
> > Here are my answers to Al's questions:
> >
> > 1) It is guaranteed that V will be freed exactly once. It is not
> > guaranteed that no accesses to *V will occur after it is freed, because
> > the test contains a data race. CPU1's plain "V->A = 0" write races with
> > CPU2's READ_ONCE; if the plain write were replaced with
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
> > CPU1's smp_load_acquire could be replaced with a plain read while the
> > plain write is replaced with smp_store_release.
> >
> > 2) The smp_store_release in CPU2 is not needed. Replacing it with a
> > plain V->B = 0 will not break anything.
>
> This was my interpretation also. I made the mistake of reading this right
> before trying to go to bed the other night and ended up tweeting at Paul
> that I'd regret it if he gave me scary dreams. Thought about it and read
> your write up and it is still exactly how I see it.
Should I have added a "read at your own risk" disclaimer? ;-)
Thanx, Paul
Re: Litmus test for question from Al Viro
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
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
Signed-off-by: Paul E. McKenney
diff --git a/manual/kernel/crypto-control-data.litmus
b/manual/kernel/crypto-control-data.litmus
new file mode 100644
index 000..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)
Re: Litmus test for question from Al Viro
On Sat, Oct 03, 2020 at 12:11:59PM -0400, j...@joelfernandes.org wrote:
> On Sat, Oct 03, 2020 at 12:08:46PM -0400, j...@joelfernandes.org wrote:
> [...]
> > static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
> >
> > struct v_struct *r1; /* to_free */
> >
> > r1 = NULL;
> > spin_lock(l);
> > if (!smp_load_acquire(&v->b))
> > r1 = v;
> > v->a = 0;
> > spin_unlock(l);
> >
> > *out_0_r1 = !!r1;
> > }
> >
> > static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
> >
> > struct v_struct *r1; /* to_free */
> >
> > r1 = v;
> > if (READ_ONCE(v->a)) {
> > spin_lock(l);
> > if (v->a)
> > r1 = NULL;
> > smp_store_release(&v->b, 0);
> > spin_unlock(l);
> > }
> >
> > *out_1_r1 = !!r1;
> > }
> >
> > Results on both arm64 and x86:
> >
> > Histogram (2 states)
> > 19080852:>0:r1=1; 1:r1=0;
> > 20919148:>0:r1=0; 1:r1=1;
> > No
> >
> > Witnesses
> > Positive: 0, Negative: 4000
> > Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
> > Hash=4a8c15603ffb5ab464195ea39ccd6382
> > Observation AL+test Never 0 4000
> > Time AL+test 6.24
> >
> > I guess I could do an alloc and free of v_struct. However, I just checked
> > for
> > whether the to_free in Al's example could ever be NULL for both threads.
>
> Sorry, here I meant "ever be non-NULL".
>
> So basically I was trying to experimentally confirm that to_free could never
> be non-NULL in both code0 and code1 threads.
Thank you for running these! In conjunction with Alan's analysis,
this seems quite convincing. ;-)
Thanx, Paul
Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Sat, 3 Oct 2020 13:13:38 -0400, Alan Stern wrote:
> On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
>> 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.
>
> You're right. This is definitely a bug in herd7.
>
> Luc, were you aware of this?
>
>> 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
>> -
>
> What you should have done was put smp_store_release in P0 and left P1 in
> its original form. That test should not be allowed, but herd7 says that
> it is.
Yea, that was what I tried first, expecting the result of "Never".
>
>> As this is the same as the expected result, I suppose you have missed another
>> limitation of herd7 + LKMM.
>
> It would be more accurate to say that we all missed it. :-) (And it's
> a bug in herd7, not a limitation of either herd7 or LKMM.) How did you
> notice it?
:-) :-) :-)
Well, I thought I had never seen a litmus test with such one-liner.
So I split the READ_ONCE() and WRITE_ONCE() into two lines and
got the expected result.
I don't expect much from herd7's C mode in the first place.
(No offense intended!)
>> 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.
>
> Yes, one in which LKMM does not recognize a genuine dependency because
> it can't tell that some optimizations are not valid.
>
> This flaw is fundamental to the way herd7 works. It examines only one
> execution at a time, and it doesn't consider the code in a conditional
> branch while it's examining an execution where that branch wasn't taken.
> Therefore it has no way to know that the code in the unexecuted branch
> would prevent a certain optimization. But the compiler does consider
> all the code in all branches when deciding what optimizations to apply.
I see.
>
> Here's another trivial example:
>
> r1 = READ_ONCE(*x);
> if (r1 == 0)
> smp_mb();
> WRITE_ONCE(*y, 1);
>
> The compiler can't move the WRITE_ONCE before the READ_ONCE or the "if"
> statement, because it's not allowed to move shared memory accesses past
> a memory barrier -- even if that memory barrier isn't always executed.
> Therefore the WRITE_ONCE actually is ordered after the READ_ONCE, but
> the memory model doesn't realize it.>
>> Alan, can you come up with an update in this regard?
>
> I'll write something.
Thanks!
Akira
>
> Alan
>
Bug in herd7 [Was: Re: Litmus test for question from Al Viro]
On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> 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.
You're right. This is definitely a bug in herd7.
Luc, were you aware of this?
> 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
> -
What you should have done was put smp_store_release in P0 and left P1 in
its original form. That test should not be allowed, but herd7 says that
it is.
> As this is the same as the expected result, I suppose you have missed another
> limitation of herd7 + LKMM.
It would be more accurate to say that we all missed it. :-) (And it's
a bug in herd7, not a limitation of either herd7 or LKMM.) How did you
notice it?
> 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.
Yes, one in which LKMM does not recognize a genuine dependency because
it can't tell that some optimizations are not valid.
This flaw is fundamental to the way herd7 works. It examines only one
execution at a time, and it doesn't consider the code in a conditional
branch while it's examining an execution where that branch wasn't taken.
Therefore it has no way to know that the code in the unexecuted branch
would prevent a certain optimization. But the compiler does consider
all the code in all branches when deciding what optimizations to apply.
Here's another trivial example:
r1 = READ_ONCE(*x);
if (r1 == 0)
smp_mb();
WRITE_ONCE(*y, 1);
The compiler can't move the WRITE_ONCE before the READ_ONCE or the "if"
statement, because it's not allowed to move shared memory accesses past
a memory barrier -- even if that memory barrier isn't always executed.
Therefore the WRITE_ONCE actually is ordered after the READ_ONCE, but
the memory model doesn't realize it.
> Alan, can you come up with an update in this regard?
I'll write something.
Alan
Re: Litmus test for question from Al Viro
On Sat, Oct 03, 2020 at 12:08:46PM -0400, j...@joelfernandes.org wrote:
[...]
> static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
>
> struct v_struct *r1; /* to_free */
>
> r1 = NULL;
> spin_lock(l);
> if (!smp_load_acquire(&v->b))
> r1 = v;
> v->a = 0;
> spin_unlock(l);
>
> *out_0_r1 = !!r1;
> }
>
> static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
>
> struct v_struct *r1; /* to_free */
>
> r1 = v;
> if (READ_ONCE(v->a)) {
> spin_lock(l);
> if (v->a)
> r1 = NULL;
> smp_store_release(&v->b, 0);
> spin_unlock(l);
> }
>
> *out_1_r1 = !!r1;
> }
>
> Results on both arm64 and x86:
>
> Histogram (2 states)
> 19080852:>0:r1=1; 1:r1=0;
> 20919148:>0:r1=0; 1:r1=1;
> No
>
> Witnesses
> Positive: 0, Negative: 4000
> Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
> Hash=4a8c15603ffb5ab464195ea39ccd6382
> Observation AL+test Never 0 4000
> Time AL+test 6.24
>
> I guess I could do an alloc and free of v_struct. However, I just checked for
> whether the to_free in Al's example could ever be NULL for both threads.
Sorry, here I meant "ever be non-NULL".
So basically I was trying to experimentally confirm that to_free could never
be non-NULL in both code0 and code1 threads.
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 02:30:48PM -0700, Paul E. McKenney wrote:
> On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > > Hello!
> > >
> > > Al Viro posted the following query:
> > >
> > >
> > >
> > > fun question regarding barriers, if you have time for that
> > > V->A = V->B = 1;
> > >
> > > CPU1:
> > > to_free = NULL
> > > spin_lock(&LOCK)
> > > if (!smp_load_acquire(&V->B))
> > > to_free = V
> > > V->A = 0
> > > spin_unlock(&LOCK)
> > > kfree(to_free)
> > >
> > > CPU2:
> > > to_free = V;
> > > if (READ_ONCE(V->A)) {
> > > spin_lock(&LOCK)
> > > if (V->A)
> > > to_free = NULL
> > > smp_store_release(&V->B, 0);
> > > spin_unlock(&LOCK)
> > > }
> > > kfree(to_free);
> > > 1) is it guaranteed that V will be freed exactly once and that
> > > no accesses to *V will happen after freeing it?
> > > 2) do we need smp_store_release() there? I.e. will anything
> > > break if it's replaced with plain V->B = 0?
> >
> > Here are my answers to Al's questions:
> >
> > 1) It is guaranteed that V will be freed exactly once. It is not
> > guaranteed that no accesses to *V will occur after it is freed, because
> > the test contains a data race. CPU1's plain "V->A = 0" write races with
> > CPU2's READ_ONCE; if the plain write were replaced with
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
> > CPU1's smp_load_acquire could be replaced with a plain read while the
> > plain write is replaced with smp_store_release.
> >
> > 2) The smp_store_release in CPU2 is not needed. Replacing it with a
> > plain V->B = 0 will not break anything.
> >
> > Analysis: Apart from the kfree calls themselves, the only access to a
> > shared variable outside of a critical section is CPU2's READ_ONCE of
> > V->A. So let's consider two possibilities:
> >
> > 1: The READ_ONCE returns 0. Then CPU2 doesn't execute its critical
> > section and does kfree(V). However, the fact that the READ_ONCE got 0
> > means that CPU1 has already entered its critical section, has already
> > written to V->A (but with a plain write!) and therefore has already seen
> > V->B = 1 (because of the smp_load_acquire), and therefore will not free
> > V. This case shows that the ordering we require is for CPU1 to read
> > V->B before it writes V->A. The ordering can be enforced by using
> > either a load-acquire (as in the litmus test) or a store-release.
> >
> > 2: The READ_ONCE returns 1. Then CPU2 does execute its critical
> > section, and we can simply treat this case the same as if the critical
> > section was executed unconditionally. Whichever CPU runs its critical
> > section second will free V, and the other CPU won't try to access V
> > after leaving its own critical section (and thus won't access V after it
> > has been freed).
> >
> > >
> > >
> > > Of course herd7 supports neither structures nor arrays
FWIW, I turned Al's example into a klitmus test which gave me the freedom to
modify it offline and use structures.
The code of the 2 threads look like this (full module enclosed later in the
email). I don't see any issues with the example above on either x86 or arm64
which I luckily have these days. Al or others could also modify the module
with any variations and test as well:
static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
struct v_struct *r1; /* to_free */
r1 = NULL;
spin_lock(l);
if (!smp_load_acquire(&v->b))
r1 = v;
v->a = 0;
spin_unlock(l);
*out_0_r1 = !!r1;
}
static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
struct v_struct *r1; /* to_free */
r1 = v;
if (READ_ONCE(v->a)) {
spin_lock(l);
if (v->a)
r1 = NULL;
smp_store_release(&v->b, 0);
spin_unlock(l);
}
*out_1_r1 = !!r1;
}
Results on both arm64 and x86:
Histogram (2 states)
19080852:>0:r1=1; 1:r1=0;
20919148:>0:r1=0; 1:r1=1;
No
Witnesses
Positive: 0, Negative: 4000
Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
Hash=4a8c15603ffb5ab464195ea39ccd6382
Observation AL+test Never 0 4000
Time AL+test 6.24
I guess I could do an alloc and free of v_struct. However, I just checked for
whether the to_free in Al's example could ever be NULL for both threads.
Here is the full test. To run it:
modprobe litmus nruns=200
cat /proc/litmus
rmmod
(The file_operations may need to be replaced trivially with proc_operations
for
Re: Litmus test for question from Al Viro
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)
>
Re: Litmus test for question from Al Viro
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)
Re: Litmus test for question from Al Viro
On 10/1/20 12:15 PM, Alan Stern wrote:
On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
Hello!
Al Viro posted the following query:
fun question regarding barriers, if you have time for that
V->A = V->B = 1;
CPU1:
to_free = NULL
spin_lock(&LOCK)
if (!smp_load_acquire(&V->B))
to_free = V
V->A = 0
spin_unlock(&LOCK)
kfree(to_free)
CPU2:
to_free = V;
if (READ_ONCE(V->A)) {
spin_lock(&LOCK)
if (V->A)
to_free = NULL
smp_store_release(&V->B, 0);
spin_unlock(&LOCK)
}
kfree(to_free);
1) is it guaranteed that V will be freed exactly once and that
no accesses to *V will happen after freeing it?
2) do we need smp_store_release() there? I.e. will anything
break if it's replaced with plain V->B = 0?
Here are my answers to Al's questions:
1) It is guaranteed that V will be freed exactly once. It is not
guaranteed that no accesses to *V will occur after it is freed, because
the test contains a data race. CPU1's plain "V->A = 0" write races with
CPU2's READ_ONCE; if the plain write were replaced with
"WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
CPU1's smp_load_acquire could be replaced with a plain read while the
plain write is replaced with smp_store_release.
2) The smp_store_release in CPU2 is not needed. Replacing it with a
plain V->B = 0 will not break anything.
This was my interpretation also. I made the mistake of reading this
right before trying to go to bed the other night and ended up tweeting
at Paul that I'd regret it if he gave me scary dreams. Thought about it
and read your write up and it is still exactly how I see it.
Jon.
--
Computer Architect
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 02:30:48PM -0700, Paul E. McKenney wrote:
> > Not the way I would have done it, but okay. I would have modeled the
> > kfree by setting a and b both to some sentinel value.
>
> Might be well worth pursuing! But how would you model the address
> dependencies in that approach?
Al's original test never writes to V. So the address dependencies don't
matter.
> > Why didn't this flag the data race?
>
> Because I turned Al's simple assignments into *_ONCE() or better.
> In doing this, I was following the default KCSAN settings which
> (for better or worse) forgive the stores from data races.
Ah, yes. I had realized that when reading the litmus test for the first
time, and then forgot it.
> With your suggested change and using simple assignments where Al
> indicated them:
>
>
>
> $ herd7 -conf linux-kernel.cfg
> ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
> Test C-viro-2020.09.29a Allowed
> States 5
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1;
> 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1;
> 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2;
> 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1;
> 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1;
> 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
> Ok
> Witnesses
> Positive: 3 Negative: 2
> Flag data-race
> Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0
> \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
> Observation C-viro-2020.09.29a Sometimes 3 2
> Time C-viro-2020.09.29a 17.95
> Hash=14ded51102b668bc38b790e8c3692227
>
>
>
> So still "Sometimes", but the "Flag data-race" you expected is there.
>
> I posted the updated litmus test below. Additional or other thoughts?
Two problems remaining. One in the litmus test and one in the memory
model itself...
>
>
> C C-viro-2020.09.29a
>
> {
> int a = 1;
> int b = 1;
> int v = 1;
> }
>
>
> P0(int *a, int *b, int *v, spinlock_t *l)
> {
> int r0;
> int r1;
> int r2 = 2;
> int r8;
> int r9a = 2;
> int r9b = 2;
>
> r0 = 0;
> spin_lock(l);
> r9a = READ_ONCE(*v); // Use after free?
> r8 = r9a - r9a; // Restore address dependency
> r8 = b + r8;
> r1 = smp_load_acquire(r8);
> if (r1 == 0)
> r0 = 1;
> r9b = READ_ONCE(*v); // Use after free?
> // WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> *a = r9b - r9b; // Use data dependency
> spin_unlock(l);
> if (r0) {
> r2 = READ_ONCE(*v);
> WRITE_ONCE(*v, 0); /* kfree(). */
> }
> }
>
> P1(int *a, int *b, int *v, spinlock_t *l)
> {
> int r0;
> int r1;
> int r1a;
> int r2 = 2;
> int r8;
> int r9a = 2;
> int r9b = 2;
> int r9c = 2;
>
> r0 = 1;
> r9a = READ_ONCE(*v); // Use after free?
> r8 = r9a - r9a; // Restore address dependency
> r8 = a + r8;
> r1 = READ_ONCE(*r8);
> if (r1) {
> spin_lock(l);
> r9b = READ_ONCE(*v); // Use after free?
> r8 = r9b - r9b; // Restore address dependency
> r8 = a + r8;
> // r1a = READ_ONCE(*r8);
> r1a = *r8;
> if (r1a)
> r0 = 0;
> r9c = READ_ONCE(*v); // Use after free?
> smp_store_release(b, r9c - rc9); // Use data dependency
---^^^
Typo: this should be r9c. Too bad herd7 doesn't warn about undeclared
local variables.
> spin_unlock(l);
> }
> if (r0) {
> r2 = READ_ONCE(*v);
> WRITE_ONCE(*v, 0); /* kfree(). */
> }
> }
>
> locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
> exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
> v=1 \/ (* Neither did kfree, redundant check. *)
> 0:r2=0 \/ 1:r2=0 \/ (* Both did kfree, redundant check. *)
> 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
> 1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)
When you fix the typo, the test still fails. But now it all makes
sense. The reason for the failure is because of the way we don't model
control dependencies.
In short, suppose P1 reads 0 for V->A. Then it does:
if (READ_ONCE(V->A)) {
... skipped ...
}
WRITE_ONCE(V, 0); /* actually kfree(to_free); */
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > Hello!
> >
> > Al Viro posted the following query:
> >
> >
> >
> > fun question regarding barriers, if you have time for that
> > V->A = V->B = 1;
> >
> > CPU1:
> > to_free = NULL
> > spin_lock(&LOCK)
> > if (!smp_load_acquire(&V->B))
> > to_free = V
> > V->A = 0
> > spin_unlock(&LOCK)
> > kfree(to_free)
> >
> > CPU2:
> > to_free = V;
> > if (READ_ONCE(V->A)) {
> > spin_lock(&LOCK)
> > if (V->A)
> > to_free = NULL
> > smp_store_release(&V->B, 0);
> > spin_unlock(&LOCK)
> > }
> > kfree(to_free);
> > 1) is it guaranteed that V will be freed exactly once and that
> > no accesses to *V will happen after freeing it?
> > 2) do we need smp_store_release() there? I.e. will anything
> > break if it's replaced with plain V->B = 0?
>
> Here are my answers to Al's questions:
>
> 1) It is guaranteed that V will be freed exactly once. It is not
> guaranteed that no accesses to *V will occur after it is freed, because
> the test contains a data race. CPU1's plain "V->A = 0" write races with
> CPU2's READ_ONCE; if the plain write were replaced with
> "WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
> CPU1's smp_load_acquire could be replaced with a plain read while the
> plain write is replaced with smp_store_release.
>
> 2) The smp_store_release in CPU2 is not needed. Replacing it with a
> plain V->B = 0 will not break anything.
>
> Analysis: Apart from the kfree calls themselves, the only access to a
> shared variable outside of a critical section is CPU2's READ_ONCE of
> V->A. So let's consider two possibilities:
>
> 1: The READ_ONCE returns 0. Then CPU2 doesn't execute its critical
> section and does kfree(V). However, the fact that the READ_ONCE got 0
> means that CPU1 has already entered its critical section, has already
> written to V->A (but with a plain write!) and therefore has already seen
> V->B = 1 (because of the smp_load_acquire), and therefore will not free
> V. This case shows that the ordering we require is for CPU1 to read
> V->B before it writes V->A. The ordering can be enforced by using
> either a load-acquire (as in the litmus test) or a store-release.
>
> 2: The READ_ONCE returns 1. Then CPU2 does execute its critical
> section, and we can simply treat this case the same as if the critical
> section was executed unconditionally. Whichever CPU runs its critical
> section second will free V, and the other CPU won't try to access V
> after leaving its own critical section (and thus won't access V after it
> has been freed).
>
> >
> >
> > Of course herd7 supports neither structures nor arrays, but I was
> > crazy enough to try individual variables with made-up address and data
> > dependencies. This litmus test must also detect use-after-free bugs,
> > but a simple variable should be able to do that. So here is a
> > prototype:
> >
> >
> >
> > C C-viro-2020.09.29a
> >
> > {
> > int a = 1;
> > int b = 1;
> > int v = 1;
> > }
>
> Not the way I would have done it, but okay. I would have modeled the
> kfree by setting a and b both to some sentinel value.
Might be well worth pursuing! But how would you model the address
dependencies in that approach?
> > P0(int *a, int *b, int *v, spinlock_t *l)
> > {
> > int r0;
> > int r1;
> > int r2 = 2;
> > int r8;
> > int r9a = 2;
> > int r9b = 2;
> >
> > r0 = 0;
> > spin_lock(l);
> > r9a = READ_ONCE(*v); // Use after free?
> > r8 = r9a - r9a; // Restore address dependency
> > r8 = b + r8;
> > r1 = smp_load_acquire(r8);
> > if (r1 == 0)
> > r0 = 1;
> > r9b = READ_ONCE(*v); // Use after free?
> > WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> > spin_unlock(l);
> > if (r0) {
> > r2 = READ_ONCE(*v);
> > WRITE_ONCE(*v, 0); /* kfree(). */
> > }
> > }
> >
> > P1(int *a, int *b, int *v, spinlock_t *l)
> > {
> > int r0;
> > int r1;
> > int r1a;
> > int r2 = 2;
> > int r8;
> > int r9a = 2;
> > int r9b = 2;
> > int r9c = 2;
> >
> > r0 = READ_ONCE(*v);
> > r9a = r0; // Use after free?
>
> Wrong. This should be:
>
> r0 = 1;
> r9a = READ_ONCE(*v);
Thank you! I was definitely suffering from a severe case of Programmer's
Blindness. Fixed!
> > r8 = r9a - r9a; // Restore address dependency
> > r8 = a + r8;
> > r1 = READ_ONCE(*r8);
> > if (r1) {
>
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 02:39:25PM -0400, Alan Stern wrote:
> The problem with a plain write is that it isn't guaranteed to be atomic
> in any sense. In principle, the compiler could generate code for CPU1
> which would write 0 to V->A more than once.
>
> Although I strongly doubt that any real compiler would actually do this,
> the memory model does allow for it, out of an overabundance of caution.
Point... OK, not a problem - actually there will be WRITE_ONCE() for other
reasons; the real-life (pseudo-)code is
spin_lock(&file->f_lock);
to_free = NULL;
head = file->f_ep;
if (head->first == &epitem->fllink && epitem->fllink.next == NULL) {
/* the set will go empty */
file->f_ep = NULL;
if (!is_file_epoll(file)) {
/*
* not embedded into struct eventpoll; we want it
* freed unless it's on the check list, in which
* case we leave it for reverse path check to free.
*/
v = container_of(head, struct ep_head, epitems);
if (!smp_load_acquire(&v->next))
to_free = v;
}
}
hlist_del_rcu(&epitem->fllink);
spin_unlock(file->f_lock);
kfree(to_free);
and hlist_del_rcu() will use WRITE_ONCE() to store the updated forward links.
That goes into ep_remove() and CPU1 side of that thing is the final
(set-emptying)
call. CPU2 side is the list traversal step in reverse_path_check() and
in clear_tfile_check_list():
// under rcu_read_lock()
to_free = head;
epitem = rcu_dereference(hlist_first_rcu(&head->epitems));
if (epitem) {
spin_lock(&epitem->file->f_lock);
if (!hlist_empty(&head->epitems))
to_free = NULL;
head->next = NULL;
spin_unlock(&epitem->file->f_lock);
}
kfree(to_free);
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 05:36:46PM +0100, Al Viro wrote:
> On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > > CPU1:
> > > to_free = NULL
> > > spin_lock(&LOCK)
> > > if (!smp_load_acquire(&V->B))
> > > to_free = V
> > > V->A = 0
> > > spin_unlock(&LOCK)
> > > kfree(to_free)
> > >
> > > CPU2:
> > > to_free = V;
> > > if (READ_ONCE(V->A)) {
> > > spin_lock(&LOCK)
> > > if (V->A)
> > > to_free = NULL
> > > smp_store_release(&V->B, 0);
> > > spin_unlock(&LOCK)
> > > }
> > > kfree(to_free);
> > > 1) is it guaranteed that V will be freed exactly once and that
> > > no accesses to *V will happen after freeing it?
> > > 2) do we need smp_store_release() there? I.e. will anything
> > > break if it's replaced with plain V->B = 0?
> >
> > Here are my answers to Al's questions:
> >
> > 1) It is guaranteed that V will be freed exactly once. It is not
> > guaranteed that no accesses to *V will occur after it is freed, because
> > the test contains a data race. CPU1's plain "V->A = 0" write races with
> > CPU2's READ_ONCE;
>
> What will that READ_ONCE() yield in that case? If it's non-zero, we should
> be fine - we won't get to kfree() until after we are done with the spinlock.
> And if it's zero... What will CPU1 do with *V accesses _after_ it has issued
> the store to V->A?
>
> Confused...
Presumably CPU2's READ_ONCE will yield either 0 or 1. For the sake of
argument, suppose it yields 0. But that's not the problem.
The problem with a plain write is that it isn't guaranteed to be atomic
in any sense. In principle, the compiler could generate code for CPU1
which would write 0 to V->A more than once.
Although I strongly doubt that any real compiler would actually do this,
the memory model does allow for it, out of an overabundance of caution.
So what could happen is:
CPU1CPU2
Writes 0 to V->A a first time
READ_ONCE(V->A) returns 0
Skips the critical section
Does kfree(V)
Tries to write 0 to V->A a
second time
> > if the plain write were replaced with
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
> > CPU1's smp_load_acquire could be replaced with a plain read while the
> > plain write is replaced with smp_store_release.
>
> Er... Do you mean the write to ->A on CPU1?
Yes; that's the only plain write in the litmus test.
Alan
Re: Litmus test for question from Al Viro
On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > CPU1:
> > to_free = NULL
> > spin_lock(&LOCK)
> > if (!smp_load_acquire(&V->B))
> > to_free = V
> > V->A = 0
> > spin_unlock(&LOCK)
> > kfree(to_free)
> >
> > CPU2:
> > to_free = V;
> > if (READ_ONCE(V->A)) {
> > spin_lock(&LOCK)
> > if (V->A)
> > to_free = NULL
> > smp_store_release(&V->B, 0);
> > spin_unlock(&LOCK)
> > }
> > kfree(to_free);
> > 1) is it guaranteed that V will be freed exactly once and that
> > no accesses to *V will happen after freeing it?
> > 2) do we need smp_store_release() there? I.e. will anything
> > break if it's replaced with plain V->B = 0?
>
> Here are my answers to Al's questions:
>
> 1) It is guaranteed that V will be freed exactly once. It is not
> guaranteed that no accesses to *V will occur after it is freed, because
> the test contains a data race. CPU1's plain "V->A = 0" write races with
> CPU2's READ_ONCE;
What will that READ_ONCE() yield in that case? If it's non-zero, we should
be fine - we won't get to kfree() until after we are done with the spinlock.
And if it's zero... What will CPU1 do with *V accesses _after_ it has issued
the store to V->A?
Confused...
> if the plain write were replaced with
> "WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
> CPU1's smp_load_acquire could be replaced with a plain read while the
> plain write is replaced with smp_store_release.
Er... Do you mean the write to ->A on CPU1?
Re: Litmus test for question from Al Viro
On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> Hello!
>
> Al Viro posted the following query:
>
>
>
> fun question regarding barriers, if you have time for that
> V->A = V->B = 1;
>
> CPU1:
> to_free = NULL
> spin_lock(&LOCK)
> if (!smp_load_acquire(&V->B))
> to_free = V
> V->A = 0
> spin_unlock(&LOCK)
> kfree(to_free)
>
> CPU2:
> to_free = V;
> if (READ_ONCE(V->A)) {
> spin_lock(&LOCK)
> if (V->A)
> to_free = NULL
> smp_store_release(&V->B, 0);
> spin_unlock(&LOCK)
> }
> kfree(to_free);
> 1) is it guaranteed that V will be freed exactly once and that
> no accesses to *V will happen after freeing it?
> 2) do we need smp_store_release() there? I.e. will anything
> break if it's replaced with plain V->B = 0?
Here are my answers to Al's questions:
1) It is guaranteed that V will be freed exactly once. It is not
guaranteed that no accesses to *V will occur after it is freed, because
the test contains a data race. CPU1's plain "V->A = 0" write races with
CPU2's READ_ONCE; if the plain write were replaced with
"WRITE_ONCE(V->A, 0)" then the guarantee would hold. Equally well,
CPU1's smp_load_acquire could be replaced with a plain read while the
plain write is replaced with smp_store_release.
2) The smp_store_release in CPU2 is not needed. Replacing it with a
plain V->B = 0 will not break anything.
Analysis: Apart from the kfree calls themselves, the only access to a
shared variable outside of a critical section is CPU2's READ_ONCE of
V->A. So let's consider two possibilities:
1: The READ_ONCE returns 0. Then CPU2 doesn't execute its critical
section and does kfree(V). However, the fact that the READ_ONCE got 0
means that CPU1 has already entered its critical section, has already
written to V->A (but with a plain write!) and therefore has already seen
V->B = 1 (because of the smp_load_acquire), and therefore will not free
V. This case shows that the ordering we require is for CPU1 to read
V->B before it writes V->A. The ordering can be enforced by using
either a load-acquire (as in the litmus test) or a store-release.
2: The READ_ONCE returns 1. Then CPU2 does execute its critical
section, and we can simply treat this case the same as if the critical
section was executed unconditionally. Whichever CPU runs its critical
section second will free V, and the other CPU won't try to access V
after leaving its own critical section (and thus won't access V after it
has been freed).
>
>
> Of course herd7 supports neither structures nor arrays, but I was
> crazy enough to try individual variables with made-up address and data
> dependencies. This litmus test must also detect use-after-free bugs,
> but a simple variable should be able to do that. So here is a
> prototype:
>
>
>
> C C-viro-2020.09.29a
>
> {
> int a = 1;
> int b = 1;
> int v = 1;
> }
Not the way I would have done it, but okay. I would have modeled the
kfree by setting a and b both to some sentinel value.
> P0(int *a, int *b, int *v, spinlock_t *l)
> {
> int r0;
> int r1;
> int r2 = 2;
> int r8;
> int r9a = 2;
> int r9b = 2;
>
> r0 = 0;
> spin_lock(l);
> r9a = READ_ONCE(*v); // Use after free?
> r8 = r9a - r9a; // Restore address dependency
> r8 = b + r8;
> r1 = smp_load_acquire(r8);
> if (r1 == 0)
> r0 = 1;
> r9b = READ_ONCE(*v); // Use after free?
> WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> spin_unlock(l);
> if (r0) {
> r2 = READ_ONCE(*v);
> WRITE_ONCE(*v, 0); /* kfree(). */
> }
> }
>
> P1(int *a, int *b, int *v, spinlock_t *l)
> {
> int r0;
> int r1;
> int r1a;
> int r2 = 2;
> int r8;
> int r9a = 2;
> int r9b = 2;
> int r9c = 2;
>
> r0 = READ_ONCE(*v);
> r9a = r0; // Use after free?
Wrong. This should be:
r0 = 1;
r9a = READ_ONCE(*v);
> r8 = r9a - r9a; // Restore address dependency
> r8 = a + r8;
> r1 = READ_ONCE(*r8);
> if (r1) {
> spin_lock(l);
> r9b = READ_ONCE(*v); // Use after free?
> r8 = r9b - r9b; // Restore address dependency
> r8 = a + r8;
> r1a = READ_ONCE(*r8);
> if (r1a)
> r0 = 0;
> r9c = READ_ONCE(*v); // Use after free?
> smp_store_release(b, r9c - rc9); // Use data dependency
> spin_unlock(l);
> }
Litmus test for question from Al Viro
Hello!
Al Viro posted the following query:
fun question regarding barriers, if you have time for that
V->A = V->B = 1;
CPU1:
to_free = NULL
spin_lock(&LOCK)
if (!smp_load_acquire(&V->B))
to_free = V
V->A = 0
spin_unlock(&LOCK)
kfree(to_free)
CPU2:
to_free = V;
if (READ_ONCE(V->A)) {
spin_lock(&LOCK)
if (V->A)
to_free = NULL
smp_store_release(&V->B, 0);
spin_unlock(&LOCK)
}
kfree(to_free);
1) is it guaranteed that V will be freed exactly once and that
no accesses to *V will happen after freeing it?
2) do we need smp_store_release() there? I.e. will anything
break if it's replaced with plain V->B = 0?
Of course herd7 supports neither structures nor arrays, but I was
crazy enough to try individual variables with made-up address and data
dependencies. This litmus test must also detect use-after-free bugs,
but a simple variable should be able to do that. So here is a
prototype:
C C-viro-2020.09.29a
{
int a = 1;
int b = 1;
int v = 1;
}
P0(int *a, int *b, int *v, spinlock_t *l)
{
int r0;
int r1;
int r2 = 2;
int r8;
int r9a = 2;
int r9b = 2;
r0 = 0;
spin_lock(l);
r9a = READ_ONCE(*v); // Use after free?
r8 = r9a - r9a; // Restore address dependency
r8 = b + r8;
r1 = smp_load_acquire(r8);
if (r1 == 0)
r0 = 1;
r9b = READ_ONCE(*v); // Use after free?
WRITE_ONCE(*a, r9b - r9b); // Use data dependency
spin_unlock(l);
if (r0) {
r2 = READ_ONCE(*v);
WRITE_ONCE(*v, 0); /* kfree(). */
}
}
P1(int *a, int *b, int *v, spinlock_t *l)
{
int r0;
int r1;
int r1a;
int r2 = 2;
int r8;
int r9a = 2;
int r9b = 2;
int r9c = 2;
r0 = READ_ONCE(*v);
r9a = r0; // Use after free?
r8 = r9a - r9a; // Restore address dependency
r8 = a + r8;
r1 = READ_ONCE(*r8);
if (r1) {
spin_lock(l);
r9b = READ_ONCE(*v); // Use after free?
r8 = r9b - r9b; // Restore address dependency
r8 = a + r8;
r1a = READ_ONCE(*r8);
if (r1a)
r0 = 0;
r9c = READ_ONCE(*v); // Use after free?
smp_store_release(b, r9c - rc9); // Use data dependency
spin_unlock(l);
}
if (r0) {
r2 = READ_ONCE(*v);
WRITE_ONCE(*v, 0); /* kfree(). */
}
}
locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
v=1 \/ (* Neither did kfree, redundant check. *)
0:r2=0 \/ 1:r2=0 \/ (* Both did kfree, redundant check. *)
0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)
This "exists" clause is satisfied:
$ herd7 -conf linux-kernel.cfg
~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
Test C-viro-2020.09.29a Allowed
States 5
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1;
1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1;
1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2;
1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1;
1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1;
1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
Ok
Witnesses
Positive: 3 Negative: 2
Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/
1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
Observation C-viro-2020.09.29a Sometimes 3 2
Time C-viro-2020.09.29a 14.33
Hash=89f74abff4de682ee0bea8ee6dd53134
So did we end up with herd7 not respecting "fake" dependencies like
those shown above, or have I just messed up the translation from Al's
example to the litmus test? (Given one thing and another over the past
couple of days, my guess would be that I just messed up the translation,
especially given that I don't see a reference to fake depe
