On Sat, Nov 21, 2020 at 01:14:59PM +0900, Akira Yokosawa wrote:
> On Fri, 20 Nov 2020 19:47:14 -0800, Paul E. McKenney wrote:
> > On Sat, Nov 21, 2020 at 11:51:11AM +0900, Akira Yokosawa wrote:
> >> On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote:
> >>> 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?
> >>
> >> You are right!
> >>
> >> Thanks, Akira
> >>
> >> PS.
> >>
> >> I'm preparing a patch series to add an index framework in perfbook.
> >> My plan is to add a specific make target for the time being to have such
> >> index pages printed.
> >> As you should know, the hard part is to embed a *lot* of index annotations
> >> in .tex source files.
> >
> > Quite right, it is a big job!
> >
> >> I'm thinking of splitting indexes into a general one and API index.
> >> By API, I mean functions such as smp_mb(), READ_ONCE(), etc.
> >>
> >> API index can have kernel API, perfbook specific API, C11 API, and GCC API.
> >
> > The upside is that the individual indexes are smaller and perhaps
> > more manageable. The downside is that a reader who has no idea
> > what the function call is might have to look it up in four (or maybe
> > even five) indexes. Especially if the API is a historic API that
> > is no longer used.
> >
> > I have no idea what the right answer is. One approach would be to
> > have all of the APIs appear both in their respective categories and
> > in the general index. Not sure that this would be any better, though.
>
> My idea is to merge all the APIs into a single API Index.
> Category of each API can be shown there like:
>
> __atomic_load() (GCC), <pages>
> ACCESS_ONCE() (kernel, historic), <pages>
> atomic_inc() (kernel), <pages>
> atomic_load() (C11), <pages>
> fork() (POSIX), <pages>
> smp_mb() (kernel), <pages>
> smp_read_barrier_depends() (kernel, historic), <pages>
>
> Give or take the appearance of annotations. For example we can use
> "G" for "GCC", "C" for "C11", "k" for "kernel", "k,h" for "kernel, historic",
> etc.
Ah, that does make more sense, thank you for clarifying!
> >> As for words/terms, if you can provide me a wish list you'd like to see in
> >> the general index, I'm willing to add such annotations.
> >> My starting point of the general index is the Glossary.
> >
> > The glossary is a good starting point. People mentioned in the text is
> > another. Not sure whether or not those quoted in the epigraphs should
> > be included or not.
>
> Ah, I missed people's names.
>
> > Names of algorithms should be included, also names
> > of data structures and of famous problems (for example, the Dining
> > Philosopher's problem, mazes, and so on).
> >
> > I am sure that I am missing quite a few categories, but at least a
> > start! ;-)
>
> Let me see how it can be done.
>
> I'll submit a [NOT PULL] request when it is ready as PoC.
Sounds very good!
Thanx, Paul
> Thanks, Akira
>
> >
> > Thanx, Paul
> >
> >> Thoughts?
> >>
> >>>
> >>> 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
> >>>>
> >>
> >> [...]
