| Message ID | a788e08d-eccb-0aec-6aa5-944e5321e5c6@gmail.com |
|---|---|
| State | New |
| Headers | show |
| Series | [v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") | expand |
On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: > >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 > From: Akira Yokosawa <akiyks@gmail.com> > Date: Fri, 9 Feb 2018 04:51:05 -0800 > Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") > > As of herd7 7.47, these '-'s are not permitted and end up in > errors such as: > > File "./linux-kernel.def", line 44, characters 29-30: > unexpected '-' (in macros) > > Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU > identifiers match ASPLOS paper") in the repository at > https://github.com/aparri/memory-model can restore the compatibility > with herd7 7.47. > > Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> > Suggested-by: Andrea Parri <parri.andrea@gmail.com> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com> > --- > Paul, > > FWIW, this is a squashed version relative to patch 07/10 in the RFC series. Thank you, Akira! I am going to hold off on this for a bit to see if we can instead get a new release of herd7, but if we can't. this might well be a very good way to go. Thanx, Paul > Thanks, Akira > -- > tools/memory-model/linux-kernel.bell | 14 +++++++------- > tools/memory-model/linux-kernel.cat | 2 +- > tools/memory-model/linux-kernel.def | 8 ++++---- > 3 files changed, 12 insertions(+), 12 deletions(-) > > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell > index b984bbd..436791b 100644 > --- a/tools/memory-model/linux-kernel.bell > +++ b/tools/memory-model/linux-kernel.bell > @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) || > 'rmb (*smp_rmb*) || > 'mb (*smp_mb*) || > 'rb_dep (*smp_read_barrier_depends*) || > - 'rcu-lock (*rcu_read_lock*) || > - 'rcu-unlock (*rcu_read_unlock*) || > - 'sync-rcu (*synchronize_rcu*) || > + 'rcu_lock (*rcu_read_lock*) || > + 'rcu_unlock (*rcu_read_unlock*) || > + 'sync_rcu (*synchronize_rcu*) || > 'before_atomic (*smp_mb__before_atomic*) || > 'after_atomic (*smp_mb__after_atomic*) || > 'after_spinlock (*smp_mb__after_spinlock*) > @@ -35,8 +35,8 @@ instructions F[Barriers] > > (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) > let matched = let rec > - unmatched-locks = Rcu-lock \ domain(matched) > - and unmatched-unlocks = Rcu-unlock \ range(matched) > + unmatched-locks = Rcu_lock \ domain(matched) > + and unmatched-unlocks = Rcu_unlock \ range(matched) > and unmatched = unmatched-locks | unmatched-unlocks > and unmatched-po = [unmatched] ; po ; [unmatched] > and unmatched-locks-to-unlocks = > @@ -46,8 +46,8 @@ let matched = let rec > in matched > > (* Validate nesting *) > -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking > -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking > +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking > +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking > > (* Outermost level of nesting only *) > let crit = matched \ (po^-1 ; matched ; po^-1) > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > index babe2b3..d0085d5 100644 > --- a/tools/memory-model/linux-kernel.cat > +++ b/tools/memory-model/linux-kernel.cat > @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | > ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) | > ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) | > ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M]) > -let gp = po ; [Sync-rcu] ; po? > +let gp = po ; [Sync_rcu] ; po? > > let strong-fence = mb | gp > > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def > index a397387..fc08371 100644 > --- a/tools/memory-model/linux-kernel.def > +++ b/tools/memory-model/linux-kernel.def > @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; } > spin_trylock(X) __trylock(X) > > // RCU > -rcu_read_lock() { __fence{rcu-lock}; } > -rcu_read_unlock() { __fence{rcu-unlock};} > -synchronize_rcu() { __fence{sync-rcu}; } > -synchronize_rcu_expedited() { __fence{sync-rcu}; } > +rcu_read_lock() { __fence{rcu_lock}; } > +rcu_read_unlock() { __fence{rcu_unlock};} > +synchronize_rcu() { __fence{sync_rcu}; } > +synchronize_rcu_expedited() { __fence{sync_rcu}; } > > // Atomic > atomic_read(X) READ_ONCE(*X) > -- > 2.7.4 > >
On 2018/02/10 10:07, Paul E. McKenney wrote: > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: >> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 >> From: Akira Yokosawa <akiyks@gmail.com> >> Date: Fri, 9 Feb 2018 04:51:05 -0800 >> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") >> >> As of herd7 7.47, these '-'s are not permitted and end up in >> errors such as: >> >> File "./linux-kernel.def", line 44, characters 29-30: >> unexpected '-' (in macros) >> >> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU >> identifiers match ASPLOS paper") in the repository at >> https://github.com/aparri/memory-model can restore the compatibility >> with herd7 7.47. >> >> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> >> Suggested-by: Andrea Parri <parri.andrea@gmail.com> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> >> --- >> Paul, >> >> FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > > Thank you, Akira! > > I am going to hold off on this for a bit to see if we can instead get > a new release of herd7, but if we can't. this might well be a very good > way to go. Fair enough. Thanks, Akira > > Thanx, Paul > >> Thanks, Akira >> -- >> tools/memory-model/linux-kernel.bell | 14 +++++++------- >> tools/memory-model/linux-kernel.cat | 2 +- >> tools/memory-model/linux-kernel.def | 8 ++++---- >> 3 files changed, 12 insertions(+), 12 deletions(-) >> >> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell >> index b984bbd..436791b 100644 >> --- a/tools/memory-model/linux-kernel.bell >> +++ b/tools/memory-model/linux-kernel.bell >> @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) || >> 'rmb (*smp_rmb*) || >> 'mb (*smp_mb*) || >> 'rb_dep (*smp_read_barrier_depends*) || >> - 'rcu-lock (*rcu_read_lock*) || >> - 'rcu-unlock (*rcu_read_unlock*) || >> - 'sync-rcu (*synchronize_rcu*) || >> + 'rcu_lock (*rcu_read_lock*) || >> + 'rcu_unlock (*rcu_read_unlock*) || >> + 'sync_rcu (*synchronize_rcu*) || >> 'before_atomic (*smp_mb__before_atomic*) || >> 'after_atomic (*smp_mb__after_atomic*) || >> 'after_spinlock (*smp_mb__after_spinlock*) >> @@ -35,8 +35,8 @@ instructions F[Barriers] >> >> (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) >> let matched = let rec >> - unmatched-locks = Rcu-lock \ domain(matched) >> - and unmatched-unlocks = Rcu-unlock \ range(matched) >> + unmatched-locks = Rcu_lock \ domain(matched) >> + and unmatched-unlocks = Rcu_unlock \ range(matched) >> and unmatched = unmatched-locks | unmatched-unlocks >> and unmatched-po = [unmatched] ; po ; [unmatched] >> and unmatched-locks-to-unlocks = >> @@ -46,8 +46,8 @@ let matched = let rec >> in matched >> >> (* Validate nesting *) >> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking >> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking >> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking >> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking >> >> (* Outermost level of nesting only *) >> let crit = matched \ (po^-1 ; matched ; po^-1) >> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat >> index babe2b3..d0085d5 100644 >> --- a/tools/memory-model/linux-kernel.cat >> +++ b/tools/memory-model/linux-kernel.cat >> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | >> ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) | >> ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) | >> ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M]) >> -let gp = po ; [Sync-rcu] ; po? >> +let gp = po ; [Sync_rcu] ; po? >> >> let strong-fence = mb | gp >> >> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def >> index a397387..fc08371 100644 >> --- a/tools/memory-model/linux-kernel.def >> +++ b/tools/memory-model/linux-kernel.def >> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; } >> spin_trylock(X) __trylock(X) >> >> // RCU >> -rcu_read_lock() { __fence{rcu-lock}; } >> -rcu_read_unlock() { __fence{rcu-unlock};} >> -synchronize_rcu() { __fence{sync-rcu}; } >> -synchronize_rcu_expedited() { __fence{sync-rcu}; } >> +rcu_read_lock() { __fence{rcu_lock}; } >> +rcu_read_unlock() { __fence{rcu_unlock};} >> +synchronize_rcu() { __fence{sync_rcu}; } >> +synchronize_rcu_expedited() { __fence{sync_rcu}; } >> >> // Atomic >> atomic_read(X) READ_ONCE(*X) >> -- >> 2.7.4 >> >> >
* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote: > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: > > >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 > > From: Akira Yokosawa <akiyks@gmail.com> > > Date: Fri, 9 Feb 2018 04:51:05 -0800 > > Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") > > > > As of herd7 7.47, these '-'s are not permitted and end up in > > errors such as: > > > > File "./linux-kernel.def", line 44, characters 29-30: > > unexpected '-' (in macros) > > > > Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU > > identifiers match ASPLOS paper") in the repository at > > https://github.com/aparri/memory-model can restore the compatibility > > with herd7 7.47. > > > > Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> > > Suggested-by: Andrea Parri <parri.andrea@gmail.com> > > Signed-off-by: Akira Yokosawa <akiyks@gmail.com> > > --- > > Paul, > > > > FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > > Thank you, Akira! > > I am going to hold off on this for a bit to see if we can instead get > a new release of herd7, but if we can't. this might well be a very good > way to go. I'm wondering: > > // RCU > > -rcu_read_lock() { __fence{rcu-lock}; } > > -rcu_read_unlock() { __fence{rcu-unlock};} > > -synchronize_rcu() { __fence{sync-rcu}; } > > -synchronize_rcu_expedited() { __fence{sync-rcu}; } > > +rcu_read_lock() { __fence{rcu_lock}; } > > +rcu_read_unlock() { __fence{rcu_unlock};} > > +synchronize_rcu() { __fence{sync_rcu}; } > > +synchronize_rcu_expedited() { __fence{sync_rcu}; } What's the point of using '-' instead of '_'? In a program language syntax environment it's easy to confuse it with a '-' operator, and it also looks slightly sloppy and inconsistent if we sometimes have '_' and sometimes '-'. If it used on purpose, to separate namespaces from kernel internal API names, then that's rather obscure IMHO and then I'd rather suggest proper prefixes instead. Thanks, Ingo
On Sun, Feb 11, 2018 at 12:51:48PM +0100, Ingo Molnar wrote: > > * Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote: > > > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: > > > >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 > > > From: Akira Yokosawa <akiyks@gmail.com> > > > Date: Fri, 9 Feb 2018 04:51:05 -0800 > > > Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") > > > > > > As of herd7 7.47, these '-'s are not permitted and end up in > > > errors such as: > > > > > > File "./linux-kernel.def", line 44, characters 29-30: > > > unexpected '-' (in macros) > > > > > > Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU > > > identifiers match ASPLOS paper") in the repository at > > > https://github.com/aparri/memory-model can restore the compatibility > > > with herd7 7.47. > > > > > > Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> > > > Suggested-by: Andrea Parri <parri.andrea@gmail.com> > > > Signed-off-by: Akira Yokosawa <akiyks@gmail.com> > > > --- > > > Paul, > > > > > > FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > > > > Thank you, Akira! > > > > I am going to hold off on this for a bit to see if we can instead get > > a new release of herd7, but if we can't. this might well be a very good > > way to go. > > I'm wondering: > > > > // RCU > > > -rcu_read_lock() { __fence{rcu-lock}; } > > > -rcu_read_unlock() { __fence{rcu-unlock};} > > > -synchronize_rcu() { __fence{sync-rcu}; } > > > -synchronize_rcu_expedited() { __fence{sync-rcu}; } > > > +rcu_read_lock() { __fence{rcu_lock}; } > > > +rcu_read_unlock() { __fence{rcu_unlock};} > > > +synchronize_rcu() { __fence{sync_rcu}; } > > > +synchronize_rcu_expedited() { __fence{sync_rcu}; } > > What's the point of using '-' instead of '_'? In a program language syntax > environment it's easy to confuse it with a '-' operator, and it also looks > slightly sloppy and inconsistent if we sometimes have '_' and sometimes '-'. > > If it used on purpose, to separate namespaces from kernel internal API names, > then that's rather obscure IMHO and then I'd rather suggest proper prefixes > instead. These lines are connecting Linux-kernel names to cat-language names. The cat language can be thought of as a set-based constraint language, which doesn't have subtraction (the closest analog being set difference, which is denoted by "\"). Cat-language code has used "-" as a word separator in names, and the model had previously had an odd mixture of "-" and "_". Hence, the switch to the cat-language convention. Of course, if underscore is strongly preferred, underscore does work, and it should be possible to move in that direction. Thanx, Paul
* Paul E. McKenney <paulmck@linux.vnet.ibm.com> wrote: > Cat-language code has used "-" as a word > separator in names, and the model had previously had an odd mixture of > "-" and "_". Hence, the switch to the cat-language convention. > > Of course, if underscore is strongly preferred, underscore does work, > and it should be possible to move in that direction. I'm fine with either of these variants, as long as it's consistent: the idiosynchratic seeming mixture of both '-' and '_' convention looked odd to me. If '_' is also more compatible with installed versions of the language, then I'd go for that - but it's your call. Thanks, Ingo
On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote: > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: >> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 >> From: Akira Yokosawa <akiyks@gmail.com> >> Date: Fri, 9 Feb 2018 04:51:05 -0800 >> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") >> >> As of herd7 7.47, these '-'s are not permitted and end up in >> errors such as: >> >> File "./linux-kernel.def", line 44, characters 29-30: >> unexpected '-' (in macros) >> >> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU >> identifiers match ASPLOS paper") in the repository at >> https://github.com/aparri/memory-model can restore the compatibility >> with herd7 7.47. >> >> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> >> Suggested-by: Andrea Parri <parri.andrea@gmail.com> >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> >> --- >> Paul, >> >> FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > > Thank you, Akira! > > I am going to hold off on this for a bit to see if we can instead get > a new release of herd7, but if we can't. this might well be a very good > way to go. So, herdtools7.7.48 is now available by "opam update; opam upgrade". Maybe mentioning the required version of herdtools7 in README would help. One glitch I'm aware of is one of the output of klitmus7 fails to compile on kernels prior to 4.14, because of smp_mb__after_spinlock() used in Z6.0+pooncelock+poonceLock+pombonce.litmus. And there is a question I want to ask. Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have smp_mb__after_spinlock(), has a comment of: (* * Result: Never * * This example demonstrates that a pair of accesses made by different * processes each while holding a given lock will not necessarily be * seen as ordered by a third process not holding that lock. *) The result was changed from "Sometimes" to "Never" in response to Alan's feedback the other day, but the following comment indicates the result should be "Sometimes". And the current model gives the result of "Sometimes". As I have no idea of the pending patches, I'd like to know once the pending patches are applied, would Z6.0+pooncelock+pooncelock+pombonce.litmus and Z6.0+pooncelock+poonceLock+pombonce.litmus become identical? Thanks, Akira > > Thanx, Paul [...] d_lock*) || >> + 'rcu_unlock (*rcu_read_unlock*) || >> + 'sync_rcu (*synchronize_rcu*) || >> 'before_atomic (*smp_mb__before_atomic*) || >> 'after_atomic (*smp_mb__after_atomic*) || >> 'after_spinlock (*smp_mb__after_spinlock*) >> @@ -35,8 +35,8 @@ instructions F[Barriers] >> >> (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) >> let matched = let rec >> - unmatched-locks = Rcu-lock \ domain(matched) >> - and unmatched-unlocks = Rcu-unlock \ range(matched) >> + unmatched-locks = Rcu_lock \ domain(matched) >> + and unmatched-unlocks = Rcu_unlock \ range(matched) >> and unmatched = unmatched-locks | unmatched-unlocks >> and unmatched-po = [unmatched] ; po ; [unmatched] >> and unmatched-locks-to-unlocks = >> @@ -46,8 +46,8 @@ let matched = let rec >> in matched >> >> (* Validate nesting *) >> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking >> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking >> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking >> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking >> >> (* Outermost level of nesting only *) >> let crit = matched \ (po^-1 ; matched ; po^-1) >> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat >> index babe2b3..d0085d5 100644 >> --- a/tools/memory-model/linux-kernel.cat >> +++ b/tools/memory-model/linux-kernel.cat >> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | >> ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) | >> ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) | >> ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M]) >> -let gp = po ; [Sync-rcu] ; po? >> +let gp = po ; [Sync_rcu] ; po? >> >> let strong-fence = mb | gp >> >> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def >> index a397387..fc08371 100644 >> --- a/tools/memory-model/linux-kernel.def >> +++ b/tools/memory-model/linux-kernel.def >> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; } >> spin_trylock(X) __trylock(X) >> >> // RCU >> -rcu_read_lock() { __fence{rcu-lock}; } >> -rcu_read_unlock() { __fence{rcu-unlock};} >> -synchronize_rcu() { __fence{sync-rcu}; } >> -synchronize_rcu_expedited() { __fence{sync-rcu}; } >> +rcu_read_lock() { __fence{rcu_lock}; } >> +rcu_read_unlock() { __fence{rcu_unlock};} >> +synchronize_rcu() { __fence{sync_rcu}; } >> +synchronize_rcu_expedited() { __fence{sync_rcu}; } >> >> // Atomic >> atomic_read(X) READ_ONCE(*X) >> -- >> 2.7.4 >> >> >
On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote: > On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote: > > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: > >> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 > >> From: Akira Yokosawa <akiyks@gmail.com> > >> Date: Fri, 9 Feb 2018 04:51:05 -0800 > >> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") > >> > >> As of herd7 7.47, these '-'s are not permitted and end up in > >> errors such as: > >> > >> File "./linux-kernel.def", line 44, characters 29-30: > >> unexpected '-' (in macros) > >> > >> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU > >> identifiers match ASPLOS paper") in the repository at > >> https://github.com/aparri/memory-model can restore the compatibility > >> with herd7 7.47. > >> > >> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> > >> Suggested-by: Andrea Parri <parri.andrea@gmail.com> > >> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> > >> --- > >> Paul, > >> > >> FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > > > > Thank you, Akira! > > > > I am going to hold off on this for a bit to see if we can instead get > > a new release of herd7, but if we can't. this might well be a very good > > way to go. > > So, herdtools7.7.48 is now available by "opam update; opam upgrade". > Maybe mentioning the required version of herdtools7 in README would help. Or have some way for the memory model's .cat files to state what version they need, but in the meantime please see the patch below. But even with such version specification, we probably want to have the version in the README... > One glitch I'm aware of is one of the output of klitmus7 fails to > compile on kernels prior to 4.14, because of smp_mb__after_spinlock() > used in Z6.0+pooncelock+poonceLock+pombonce.litmus. This is one advantage of having the memory model in the kernel source itself -- the versions match. And people can always fire up a different kernel version (for example, within a VM) to run the output of klitmus7. > And there is a question I want to ask. > > Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have > smp_mb__after_spinlock(), has a comment of: > > (* > * Result: Never > * > * This example demonstrates that a pair of accesses made by different > * processes each while holding a given lock will not necessarily be > * seen as ordered by a third process not holding that lock. > *) > > The result was changed from "Sometimes" to "Never" in response to > Alan's feedback the other day, but the following comment indicates > the result should be "Sometimes". And the current model gives the > result of "Sometimes". > > As I have no idea of the pending patches, I'd like to know once > the pending patches are applied, would > Z6.0+pooncelock+pooncelock+pombonce.litmus and > Z6.0+pooncelock+poonceLock+pombonce.litmus become identical? Let's see, examining the Z6 litmus tests and running on herd7 version 7.48: Z6.0+pooncelock+pooncelock+pombonce Sometimes 1 7 Z6.0+pooncelock+poonceLock+pombonce Never 0 7 Z6.0+pooncerelease+poacquirerelease+mbonceonce Sometimes 1 7 But Alan stated that the result of the test would be changed by one of the patches in our "pending" list. I ran with all the patches currently applied, so I am guessing that Alan was refering to one of the changes that we have discussed but not yet created. Alan, enlightenment? Thanx, Paul ------------------------------------------------------------------------ commit dad94d8dc78e50bab91b313a67232e85ee22a733 Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Date: Wed Feb 14 14:37:22 2018 -0800 tools/memory-model: Add required herd7 version to README file LKMM and the herd7 tool are co-evolving, and out-of-date herd7 tools produce inaccurate results, often with no obvious error messages. This commit therefore adds the required herd7 version to the LKMM README file. Longer term, it would be good if .cat files could specify the required version in a manner allowing herd7 to produce clear diagnostics. Suggested-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> diff --git a/tools/memory-model/README b/tools/memory-model/README index 91414a49fac5..ea950c566ffd 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,7 +20,8 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -The "herd7" and "klitmus7" tools must be downloaded separately: +Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded +separately: https://github.com/herd/herdtools7
On Wed, 14 Feb 2018, Paul E. McKenney wrote: > Let's see, examining the Z6 litmus tests and running on herd7 version 7.48: > > Z6.0+pooncelock+pooncelock+pombonce Sometimes 1 7 > Z6.0+pooncelock+poonceLock+pombonce Never 0 7 > Z6.0+pooncerelease+poacquirerelease+mbonceonce Sometimes 1 7 > > But Alan stated that the result of the test would be changed by one of > the patches in our "pending" list. I ran with all the patches currently > applied, so I am guessing that Alan was refering to one of the changes > that we have discussed but not yet created. > > Alan, enlightenment? Here's the relevant patch. It may need some manual adjustment, because it was not made against the files currently in the repository. Alan diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat Index: memory-model/linux-kernel-hardware.cat =================================================================== --- memory-model.orig/linux-kernel-hardware.cat +++ memory-model/linux-kernel-hardware.cat @@ -31,7 +31,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -57,13 +57,13 @@ let to-w = rwdep | addrpo | (overwrite & let rdw = po-loc & (fre ; rfe) let detour = po-loc & (coe ; rfe) let rrdep = addr | (dep ; rfi) -let to-r = rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = to-r | to-w | fence | rdw | detour (* Happens Before *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let rec prop = (overwrite & ext)? ; cumul-fence ; hb* and hb = ppo | rfe | ((hb* ; prop) & int) Index: memory-model/linux-kernel.cat =================================================================== --- memory-model.orig/linux-kernel.cat +++ memory-model/linux-kernel.cat @@ -31,7 +31,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -54,13 +54,13 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) let rrdep = addr | (dep ; rfi) -let to-r = rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = to-r | to-w | fence (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let prop = (overwrite & ext)? ; cumul-fence* ; rfe? (*
On 2018/02/14 14:52:38 -0800, Paul E. McKenney wrote: > On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote: >> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote: >>> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: >>>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 >>>> From: Akira Yokosawa <akiyks@gmail.com> >>>> Date: Fri, 9 Feb 2018 04:51:05 -0800 >>>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") >>>> >>>> As of herd7 7.47, these '-'s are not permitted and end up in >>>> errors such as: >>>> >>>> File "./linux-kernel.def", line 44, characters 29-30: >>>> unexpected '-' (in macros) >>>> >>>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU >>>> identifiers match ASPLOS paper") in the repository at >>>> https://github.com/aparri/memory-model can restore the compatibility >>>> with herd7 7.47. >>>> >>>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> >>>> Suggested-by: Andrea Parri <parri.andrea@gmail.com> >>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> >>>> --- >>>> Paul, >>>> >>>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series. >>> >>> Thank you, Akira! >>> >>> I am going to hold off on this for a bit to see if we can instead get >>> a new release of herd7, but if we can't. this might well be a very good >>> way to go. >> >> So, herdtools7.7.48 is now available by "opam update; opam upgrade". >> Maybe mentioning the required version of herdtools7 in README would help. > > Or have some way for the memory model's .cat files to state what version > they need, but in the meantime please see the patch below. But even with > such version specification, we probably want to have the version in the > README... > >> One glitch I'm aware of is one of the output of klitmus7 fails to >> compile on kernels prior to 4.14, because of smp_mb__after_spinlock() >> used in Z6.0+pooncelock+poonceLock+pombonce.litmus. > > This is one advantage of having the memory model in the kernel source > itself -- the versions match. And people can always fire up a different > kernel version (for example, within a VM) to run the output of klitmus7. > There is another unfortunate mismatch in kernel and herdtools7 updates. klitmus7 in herdtools7 7.48 requires definition of ACCESS_ONCE() in kernel headers, but it has been removed in Linux 4.15. This means klitmus7 of herdtools7 7.48 works only on Linux 4.14. In the repository of herdtools7, with the suggestion of Andrea, commit e87d7f9287d1 ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE in "user" synchronization barrier") has addressed the issue. This series is intended to be merged in Linux 4.17 merge window, and hopefully we can have another update of herdtools7 by the time the merge window opens... Dependency to out-of-tree tools looks quite tricky. We need some neat way to manage things. Umm... Thanks, Akira [...]
On Mon, Feb 19, 2018 at 12:46:51AM +0900, Akira Yokosawa wrote: > On 2018/02/14 14:52:38 -0800, Paul E. McKenney wrote: > > On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote: > >> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote: > >>> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote: > >>>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 > >>>> From: Akira Yokosawa <akiyks@gmail.com> > >>>> Date: Fri, 9 Feb 2018 04:51:05 -0800 > >>>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") > >>>> > >>>> As of herd7 7.47, these '-'s are not permitted and end up in > >>>> errors such as: > >>>> > >>>> File "./linux-kernel.def", line 44, characters 29-30: > >>>> unexpected '-' (in macros) > >>>> > >>>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU > >>>> identifiers match ASPLOS paper") in the repository at > >>>> https://github.com/aparri/memory-model can restore the compatibility > >>>> with herd7 7.47. > >>>> > >>>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com> > >>>> Suggested-by: Andrea Parri <parri.andrea@gmail.com> > >>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com> > >>>> --- > >>>> Paul, > >>>> > >>>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series. > >>> > >>> Thank you, Akira! > >>> > >>> I am going to hold off on this for a bit to see if we can instead get > >>> a new release of herd7, but if we can't. this might well be a very good > >>> way to go. > >> > >> So, herdtools7.7.48 is now available by "opam update; opam upgrade". > >> Maybe mentioning the required version of herdtools7 in README would help. > > > > Or have some way for the memory model's .cat files to state what version > > they need, but in the meantime please see the patch below. But even with > > such version specification, we probably want to have the version in the > > README... > > > >> One glitch I'm aware of is one of the output of klitmus7 fails to > >> compile on kernels prior to 4.14, because of smp_mb__after_spinlock() > >> used in Z6.0+pooncelock+poonceLock+pombonce.litmus. > > > > This is one advantage of having the memory model in the kernel source > > itself -- the versions match. And people can always fire up a different > > kernel version (for example, within a VM) to run the output of klitmus7. > > > > There is another unfortunate mismatch in kernel and herdtools7 updates. > > klitmus7 in herdtools7 7.48 requires definition of ACCESS_ONCE() in kernel > headers, but it has been removed in Linux 4.15. This means klitmus7 of > herdtools7 7.48 works only on Linux 4.14. > > In the repository of herdtools7, with the suggestion of Andrea, commit > e87d7f9287d1 ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated > ACCESS_ONCE in "user" synchronization barrier") has addressed the issue. > > This series is intended to be merged in Linux 4.17 merge window, > and hopefully we can have another update of herdtools7 by the time the merge > window opens... > > Dependency to out-of-tree tools looks quite tricky. We need some neat way to > manage things. > > Umm... Yes, dependencies on out-of-tree tools is quite tricky, witness the "fun and excitement" provided even by GCC from time to time. I agree that another herdtools7 release is required, and I do very much thank you for testing this and finding this issue! Thanx, Paul
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index b984bbd..436791b 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || 'mb (*smp_mb*) || 'rb_dep (*smp_read_barrier_depends*) || - 'rcu-lock (*rcu_read_lock*) || - 'rcu-unlock (*rcu_read_unlock*) || - 'sync-rcu (*synchronize_rcu*) || + 'rcu_lock (*rcu_read_lock*) || + 'rcu_unlock (*rcu_read_unlock*) || + 'sync_rcu (*synchronize_rcu*) || 'before_atomic (*smp_mb__before_atomic*) || 'after_atomic (*smp_mb__after_atomic*) || 'after_spinlock (*smp_mb__after_spinlock*) @@ -35,8 +35,8 @@ instructions F[Barriers] (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) let matched = let rec - unmatched-locks = Rcu-lock \ domain(matched) - and unmatched-unlocks = Rcu-unlock \ range(matched) + unmatched-locks = Rcu_lock \ domain(matched) + and unmatched-unlocks = Rcu_unlock \ range(matched) and unmatched = unmatched-locks | unmatched-unlocks and unmatched-po = [unmatched] ; po ; [unmatched] and unmatched-locks-to-unlocks = @@ -46,8 +46,8 @@ let matched = let rec in matched (* Validate nesting *) -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking (* Outermost level of nesting only *) let crit = matched \ (po^-1 ; matched ; po^-1) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index babe2b3..d0085d5 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M]) -let gp = po ; [Sync-rcu] ; po? +let gp = po ; [Sync_rcu] ; po? let strong-fence = mb | gp diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index a397387..fc08371 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; } spin_trylock(X) __trylock(X) // RCU -rcu_read_lock() { __fence{rcu-lock}; } -rcu_read_unlock() { __fence{rcu-unlock};} -synchronize_rcu() { __fence{sync-rcu}; } -synchronize_rcu_expedited() { __fence{sync-rcu}; } +rcu_read_lock() { __fence{rcu_lock}; } +rcu_read_unlock() { __fence{rcu_unlock};} +synchronize_rcu() { __fence{sync_rcu}; } +synchronize_rcu_expedited() { __fence{sync_rcu}; } // Atomic atomic_read(X) READ_ONCE(*X)