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 <stern@xxxxxxxxxxxxxxxxxxx> > > > > 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 <stern@xxxxxxxxxxxxxxxxxxx> 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 <stern@xxxxxxxxxxxxxxxxxxx> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx> diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus new file mode 100644 index 0000000..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)