Hi,
Is this patch not destined to the HEAD of Torvalds ?, got that feeling
as this was in flight around merge window & have not yet made there.
On Wed, Nov 15, 2017 at 08:37:49AM -0800, Paul E. McKenney wrote:
> diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt
> +Taking off the training wheels
> +==============================
:
> +Release-acquire chains
> +----------------------
:
> +It is tempting to assume that CPU0()'s store to x is globally ordered
> +before CPU1()'s store to z, but this is not the case:
> +
> + /* See Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus. */
> + void CPU0(void)
> + {
> + WRITE_ONCE(x, 1);
> + smp_store_release(&y, 1);
> + }
> +
> + void CPU1(void)
> + {
> + r1 = smp_load_acquire(y);
> + smp_store_release(&z, 1);
> + }
> +
> + void CPU2(void)
> + {
> + WRITE_ONCE(z, 2);
> + smp_mb();
> + r2 = READ_ONCE(x);
> + }
> +
> +One might hope that if the final value of r1 is 1 and the final value
> +of z is 2, then the final value of r2 must also be 1, but the opposite
> +outcome really is possible.
As there are 3 variables to have the values, perhaps, it might be
clearer to have instead of "the opposite.." - "the final value need
not be 1" or was that a read between the lines left as an exercise to
the idiots ;)
afzal
> The reason, of course, is that in this
> +version, CPU2() is not part of the release-acquire chain. This
> +situation is accounted for in the rules of thumb below.
On Wed, Dec 20, 2017 at 05:01:45PM +0530, afzal mohammed wrote:
> Hi,
>
> Is this patch not destined to the HEAD of Torvalds ?, got that feeling
> as this was in flight around merge window & have not yet made there.
That is the goal, hopefully the next merge window, or if not, the one
after that.
> On Wed, Nov 15, 2017 at 08:37:49AM -0800, Paul E. McKenney wrote:
>
> > diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt
>
> > +Taking off the training wheels
> > +==============================
> :
> > +Release-acquire chains
> > +----------------------
> :
> > +It is tempting to assume that CPU0()'s store to x is globally ordered
> > +before CPU1()'s store to z, but this is not the case:
> > +
> > + /* See Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus. */
> > + void CPU0(void)
> > + {
> > + WRITE_ONCE(x, 1);
> > + smp_store_release(&y, 1);
> > + }
> > +
> > + void CPU1(void)
> > + {
> > + r1 = smp_load_acquire(y);
> > + smp_store_release(&z, 1);
> > + }
> > +
> > + void CPU2(void)
> > + {
> > + WRITE_ONCE(z, 2);
> > + smp_mb();
> > + r2 = READ_ONCE(x);
> > + }
> > +
> > +One might hope that if the final value of r1 is 1 and the final value
> > +of z is 2, then the final value of r2 must also be 1, but the opposite
> > +outcome really is possible.
>
> As there are 3 variables to have the values, perhaps, it might be
> clearer to have instead of "the opposite.." - "the final value need
> not be 1" or was that a read between the lines left as an exercise to
> the idiots ;)
Heh! Good catch, thank you! How about the following for the paragraph
immediately after that litmus test?
One might hope that if the final value of r0 is 1 and the final
value of z is 2, then the final value of r1 must also be 1,
but it really is possible for r1 to have the final value of 0.
The reason, of course, is that in this version, CPU2() is not
part of the release-acquire chain. This situation is accounted
for in the rules of thumb below.
I also fixed r1 and r2 to match the names in the actual litmus test.
Thanx, Paul
> afzal
>
>
> > The reason, of course, is that in this
> > +version, CPU2() is not part of the release-acquire chain. This
> > +situation is accounted for in the rules of thumb below.
>
Hi,
On Wed, Dec 20, 2017 at 08:45:38AM -0800, Paul E. McKenney wrote:
> On Wed, Dec 20, 2017 at 05:01:45PM +0530, afzal mohammed wrote:
> > > +It is tempting to assume that CPU0()'s store to x is globally ordered
> > > +before CPU1()'s store to z, but this is not the case:
> > > +
> > > + /* See Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus. */
> > > + void CPU0(void)
> > > + {
> > > + WRITE_ONCE(x, 1);
> > > + smp_store_release(&y, 1);
> > > + }
> > > +
> > > + void CPU1(void)
> > > + {
> > > + r1 = smp_load_acquire(y);
> > > + smp_store_release(&z, 1);
> > > + }
> > > +
> > > + void CPU2(void)
> > > + {
> > > + WRITE_ONCE(z, 2);
> > > + smp_mb();
> > > + r2 = READ_ONCE(x);
> > > + }
> > > +
> > > +One might hope that if the final value of r1 is 1 and the final value
> > > +of z is 2, then the final value of r2 must also be 1, but the opposite
> > > +outcome really is possible.
> >
> > As there are 3 variables to have the values, perhaps, it might be
> > clearer to have instead of "the opposite.." - "the final value need
> > not be 1" or was that a read between the lines left as an exercise to
> > the idiots ;)
>
> Heh! Good catch, thank you! How about the following for the paragraph
> immediately after that litmus test?
>
> One might hope that if the final value of r0 is 1 and the final
> value of z is 2, then the final value of r1 must also be 1,
> but it really is possible for r1 to have the final value of 0.
> The reason, of course, is that in this version, CPU2() is not
> part of the release-acquire chain. This situation is accounted
> for in the rules of thumb below.
>
> I also fixed r1 and r2 to match the names in the actual litmus test.
Since it is now mentioned that r1 can have final value of 0, though it
is understood, it might make things crystal clear and for the sake of
completeness to also show the non-automatic variable x being
initialized to 0.
Thanks for taking into account my opinion.
afzal
On Thu, Dec 21, 2017 at 09:00:55AM +0530, afzal mohammed wrote:
> Hi,
>
> On Wed, Dec 20, 2017 at 08:45:38AM -0800, Paul E. McKenney wrote:
> > On Wed, Dec 20, 2017 at 05:01:45PM +0530, afzal mohammed wrote:
>
> > > > +It is tempting to assume that CPU0()'s store to x is globally ordered
> > > > +before CPU1()'s store to z, but this is not the case:
> > > > +
> > > > + /* See Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus. */
> > > > + void CPU0(void)
> > > > + {
> > > > + WRITE_ONCE(x, 1);
> > > > + smp_store_release(&y, 1);
> > > > + }
> > > > +
> > > > + void CPU1(void)
> > > > + {
> > > > + r1 = smp_load_acquire(y);
> > > > + smp_store_release(&z, 1);
> > > > + }
> > > > +
> > > > + void CPU2(void)
> > > > + {
> > > > + WRITE_ONCE(z, 2);
> > > > + smp_mb();
> > > > + r2 = READ_ONCE(x);
> > > > + }
> > > > +
> > > > +One might hope that if the final value of r1 is 1 and the final value
> > > > +of z is 2, then the final value of r2 must also be 1, but the opposite
> > > > +outcome really is possible.
> > >
> > > As there are 3 variables to have the values, perhaps, it might be
> > > clearer to have instead of "the opposite.." - "the final value need
> > > not be 1" or was that a read between the lines left as an exercise to
> > > the idiots ;)
> >
> > Heh! Good catch, thank you! How about the following for the paragraph
> > immediately after that litmus test?
> >
> > One might hope that if the final value of r0 is 1 and the final
> > value of z is 2, then the final value of r1 must also be 1,
> > but it really is possible for r1 to have the final value of 0.
> > The reason, of course, is that in this version, CPU2() is not
> > part of the release-acquire chain. This situation is accounted
> > for in the rules of thumb below.
> >
> > I also fixed r1 and r2 to match the names in the actual litmus test.
>
> Since it is now mentioned that r1 can have final value of 0, though it
> is understood, it might make things crystal clear and for the sake of
> completeness to also show the non-automatic variable x being
> initialized to 0.
Here we rely on the C-language and Linux-kernel convention that global
variables that are not explicitly initialized are initialized to zero.
(Also the documented behavior of the litmus tests and the herd tool that
uses them.) So that part should be OK as is.
Nevertheless, thank you for your review and comments!
Have you installed and run the herd tool? Doing so would allow you
to experiment with changes to the litmus tests.
Thanx, Paul
Hi,
On Thu, Dec 21, 2017 at 08:15:02AM -0800, Paul E. McKenney wrote:
> On Thu, Dec 21, 2017 at 09:00:55AM +0530, afzal mohammed wrote:
> > Since it is now mentioned that r1 can have final value of 0, though it
> > is understood, it might make things crystal clear and for the sake of
> > completeness to also show the non-automatic variable x being
> > initialized to 0.
>
> Here we rely on the C-language and Linux-kernel convention that global
> variables that are not explicitly initialized are initialized to zero.
> (Also the documented behavior of the litmus tests and the herd tool that
> uses them.) So that part should be OK as is.
Okay, that was suggested to bring parity with some of the examples in
explanation.txt, where global variables are explicitly initalized to
zero, that unconsciously made me feel that litmus tests also follow
that pattern, but checking again realize that litmus tests are not so.
>
> Nevertheless, thank you for your review and comments!
Thanks for taking the effort to reply.
> Have you installed and run the herd tool? Doing so would allow you
> to experiment with changes to the litmus tests.
Yes, i installed herd tool and then i was at a loss :(, so started
re-reading the documentation, yet to run any of the tests.
afzal
Hi,
On Fri, Dec 22, 2017 at 09:41:32AM +0530, afzal mohammed wrote:
> On Thu, Dec 21, 2017 at 08:15:02AM -0800, Paul E. McKenney wrote:
> > Have you installed and run the herd tool? Doing so would allow you
> > to experiment with changes to the litmus tests.
>
> Yes, i installed herd tool and then i was at a loss :(, so started
> re-reading the documentation, yet to run any of the tests.
Above was referring to "opam install herdtools7" & the pre-requisites,
with the current HEAD of herd, build fails as below, but builds fine
with the latest tag - 7.47.
Could run a couple of tests as well now, thanks.
afzal
herdtools7(master)$ make all
sh ./build.sh $HOME
+ /usr/bin/ocamldep.opt -modules gen/RISCVCompile_gen.ml > gen/RISCVCompile_gen.ml.depends
File "gen/RISCVCompile_gen.ml", line 94, characters 8-9:
Error: Syntax error
Command exited with code 2.
Compilation unsuccessful after building 1439 targets (0 cached) in 00:00:59.
Makefile:4: recipe for target 'all' failed
make: *** [all] Error 10
On Sat, Dec 23, 2017 at 11:44:18AM +0530, afzal mohammed wrote:
> Hi,
>
> On Fri, Dec 22, 2017 at 09:41:32AM +0530, afzal mohammed wrote:
> > On Thu, Dec 21, 2017 at 08:15:02AM -0800, Paul E. McKenney wrote:
>
> > > Have you installed and run the herd tool? Doing so would allow you
> > > to experiment with changes to the litmus tests.
> >
> > Yes, i installed herd tool and then i was at a loss :(, so started
> > re-reading the documentation, yet to run any of the tests.
>
> Above was referring to "opam install herdtools7" & the pre-requisites,
> with the current HEAD of herd, build fails as below, but builds fine
> with the latest tag - 7.47.
>
> Could run a couple of tests as well now, thanks.
Very good!
Thanx, Paul
> afzal
>
>
> herdtools7(master)$ make all
> sh ./build.sh $HOME
> + /usr/bin/ocamldep.opt -modules gen/RISCVCompile_gen.ml > gen/RISCVCompile_gen.ml.depends
> File "gen/RISCVCompile_gen.ml", line 94, characters 8-9:
> Error: Syntax error
> Command exited with code 2.
> Compilation unsuccessful after building 1439 targets (0 cached) in 00:00:59.
> Makefile:4: recipe for target 'all' failed
> make: *** [all] Error 10
>