On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
> > On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> This patch set is what I mentioned the other day in response to
> >> your LKMM patch for 5.11.
> >> klitmus7 doesn't need most of type info in litmus-test init blocks.
> >>
> >> While there are some cases where klitmus7 requires type info of variables
> >> to be watched (via the "exists", "locations", or "filter" directive),
> >> as long as the watched variables are of type "int", extra type info
> >> in the init block is not required.
> >>
> >> Litmus tests under CodeSamples/formal/ should keep compatible with
> >> klitmus7 after this patch set is applied.
> >>
> >> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
> >> under CodeSamples/formal/litmus/.
> >>
> >> Patch 2/2 further reduce line counts of litmus tests by using "{}"
> >> as empty init blocks.
> >> It also adds/removes empty lines for those code snippets to have
> >> consistent looks.
> >>
> >> Similar changes to patch 1/2 can be made in the RCU litmus tests
> >> presented in Section 12.3.2. They are not touched in this patch set.
> >>
> >> May be in a follow-up patch.
> >
> > Queued and pushed, thank you very much!
> >
> >> Thanks, Akira
> >>
> >> *NOTE*:
> >>
> >> There are cases where litmus tests for herd7 can not be
> >> made compatible with (current) klitmus7, though.
> >>
> >> One such example is when a variable of a type other than the "int"
> >> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
> >> directive.
> >> Current klitmus7 has no idea of the way to obtain the value of such a
> >> variable.
> >
> > Good to know! Do we have litmus tests that have problems with this?
>
> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
So there is not currently such a litmus test in perfbook, but one could
easily be created, correct?
Or am I still confused? ;-)
Thanx, Paul
> ---
> C Lock1-for-herd7
>
> (*
> * Example test incompatible with klitmus7
> *
> * klitmus7 cannot access spinlock_t variable.
> *)
>
> {}
>
> P0(int *x, spinlock_t *sp)
> {
> spin_lock(sp);
> WRITE_ONCE(*x, 1);
> WRITE_ONCE(*x, 0);
> spin_unlock(sp);
> }
>
> P1(int *x, spinlock_t *sp)
> {
> int r1;
>
> spin_lock(sp);
> r1 = READ_ONCE(*x);
> spin_unlock(sp);
> }
>
> locations [sp] (* incompatible with klitmus7 *)
> exists (1:r1=1)
> ---
>
> klitmus7 can't convert this to a kernel module:
>
> ---
> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
> ---
>
> Actually, herd7/LKMM does complain of this one:
>
> ---
> Test Lock1-for-herd7 Allowed
> States 1
> 1:r1=0; sp=0;
> No
> Witnesses
> Positive: 0 Negative: 2
> Flag lock-final <---
> Condition exists (1:r1=1)
> Observation Lock1-for-herd7 Never 0 2
> Time Lock1-for-herd7 0.01
> Hash=5d10e6c355cec0c36f354abf175adc54
> ---
>
> Comment at line 57 of lock.cat says:
>
> ---
> (* The final value of a spinlock should not be tested *)
> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> ---
>
> Thanks, Akira
>
> >
> >> As for herd7, all the variables are treated as if they were "int" or
> >> "int *" regardless of the type specified in the litmus tests, there
> >> is no such problem.
> >
> > Indeed, herd7 lets you get away with quite a bit. ;-)
> >
> > Thanx, Paul
> >
> >> --
> >> Akira Yokosawa (2):
> >> CodeSamples/formal/litmus: Remove redundant initializations
> >> CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
> >>
> >> CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
> >> CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
> >> ...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
> >> .../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
> >> .../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
> >> .../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> >> .../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
> >> .../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
> >> .../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
> >> .../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
> >> CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
> >> CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
> >> CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
> >> .../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
> >> .../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
> >> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
> >> CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
> >> .../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
> >> .../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
> >> memorder/memorder.tex | 8 ++------
> >> 73 files changed, 124 insertions(+), 217 deletions(-)
> >>
> >> --
> >> 2.17.1
> >>
