[...]
> > We used to distinguigh between the test name and the test filename; we
> > currently have only one test whose name ends with .litmus:
> >
> > ISA2+pooncelock+pooncelock+pombonce.litmus
> >
> > (that I missed until now...).
>
> I queued a commit to fix this with your Reported-by, good catch!
Thanks for the fix.
> > I also notice that, with the current version, the above command can be
> > simplified to:
> >
> > $ norm7 -bell linux-kernel.bell Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | sed -e 's/:.*//g'
>
> Dropping the "classify7" command, correct?
Right, thanks. Ah, maybe we should strive to meet the 80-chars bound
by splitting the command with "\"?
> > Maybe expand to recall that we're referring to a particular cycle (the
> > cycle referred to in the previous section)? (the term 'consecutive' is
> > overloaded ;-)
>
> Well, it is an English word, so overloading is the common case. ;-)
>
> How about this?
Looks better, thanks.
> > I'm not sure if it is worth commenting on this, but compare, e.g., the
> > 'exists' clauses of the following two tests (thinking at 'coherence'):
> >
> > $ diyone7 -arch LISA PosWR PodRR Fre PosWR PodRR Fre
> > LISA A
> > "PosWR PodRR Fre PosWR PodRR Fre"
> > Generator=diyone7 (version 7.49+02(dev))
> > Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
> > Com=Fr Fr
> > Orig=PosWR PodRR Fre PosWR PodRR Fre
> > {
> > }
> > P0 | P1 ;
> > w[] x 1 | w[] y 1 ;
> > r[] r0 x | r[] r0 y ;
> > r[] r1 y | r[] r1 x ;
> > exists
> > (0:r1=0 /\ 1:r1=0)
> >
> > $ diyone7 -arch LISA Rfi PodRR Fre Rfi PodRR Fre
> > LISA A
> > "Rfi PodRR Fre Rfi PodRR Fre"
> > Generator=diyone7 (version 7.49+02(dev))
> > Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
> > Com=Fr Fr
> > Orig=Rfi PodRR Fre Rfi PodRR Fre
> > {
> > }
> > P0 | P1 ;
> > w[] x 1 | w[] y 1 ;
> > r[] r0 x | r[] r0 y ;
> > r[] r1 y | r[] r1 x ;
> > exists
> > (0:r0=1 /\ 0:r1=0 /\ 1:r0=1 /\ 1:r1=0)
>
> How about this?
>
> fi: Read-from internal. The current process wrote a variable and then
> immediately read the value back from it. For the purposes of
> naming, Rfi acts identically to PosWR.
Well, "Rfi" produces "rfi" while "PosWR" produces "pos" for a name...
> However, there are subtle
> but very real differences between them in other contexts.
I think that you're fascinated by the evocative power of English words. ;-)
> > The list of descriptors is incomplete; the command:
> >
> > $ diyone7 -bell linux-kernel.bell -show edges
> >
> > shows other descriptors (including fences and dependencies). We might
> > want to list this command; searching the commit history, I found:
> >
> > 3c24730ef6c662 ("gen: Add a new command line option -show (edges|fences|annotations) that list various categories of candidate relaxations.")
>
> Yow!!!
>
> CtrldR CtrldW CtrlsR CtrlsW DpAddrdR DpAddrdW DpAddrsR DpAddrsW DpCtrldR DpCtrldW DpCtrlsR DpCtrlsW DpDatadW DpDatasW Dpd* DpdR DpdW Dps* DpsR DpsW FenceAfter-atomic FenceAfter-atomicd** FenceAfter-atomicd*R FenceAfter-atomicd*W FenceAfter-atomicdR* FenceAfter-atomicdRR FenceAfter-atomicdRW FenceAfter-atomicdW* FenceAfter-atomicdWR FenceAfter-atomicdWW FenceAfter-atomics** FenceAfter-atomics*R FenceAfter-atomics*W FenceAfter-atomicsR* FenceAfter-atomicsRR FenceAfter-atomicsRW FenceAfter-atomicsW* FenceAfter-atomicsWR FenceAfter-atomicsWW FenceAfter-spinlock FenceAfter-spinlockd** FenceAfter-spinlockd*R FenceAfter-spinlockd*W FenceAfter-spinlockdR* FenceAfter-spinlockdRR FenceAfter-spinlockdRW FenceAfter-spinlockdW* FenceAfter-spinlockdWR FenceAfter-spinlockdWW FenceAfter-spinlocks** FenceAfter-spinlocks*R FenceAfter-spinlocks*W FenceAfter-spinlocksR* FenceAfter-spinlocksRR FenceAfter-spinlocksRW FenceAfter-spinlocksW* FenceAfter-spinlocksWR FenceAfter-spinlocksWW FenceBefore-atomic FenceBefore-atomicd** FenceBefore-atomicd*R FenceBefore-atomicd*W FenceBefore-atomicdR* FenceBefore-atomicdRR FenceBefore-atomicdRW FenceBefore-atomicdW* FenceBefore-atomicdWR FenceBefore-atomicdWW FenceBefore-atomics** FenceBefore-atomics*R FenceBefore-atomics*W FenceBefore-atomicsR* FenceBefore-atomicsRR FenceBefore-atomicsRW FenceBefore-atomicsW* FenceBefore-atomicsWR FenceBefore-atomicsWW FenceMb FenceMbd** FenceMbd*R FenceMbd*W FenceMbdR* FenceMbdRR FenceMbdRW FenceMbdW* FenceMbdWR FenceMbdWW FenceMbs** FenceMbs*R FenceMbs*W FenceMbsR* FenceMbsRR FenceMbsRW FenceMbsW* FenceMbsWR FenceMbsWW FenceRcu-lock FenceRcu-lockd** FenceRcu-lockd*R FenceRcu-lockd*W FenceRcu-lockdR* FenceRcu-lockdRR FenceRcu-lockdRW FenceRcu-lockdW* FenceRcu-lockdWR FenceRcu-lockdWW FenceRcu-locks** FenceRcu-locks*R FenceRcu-locks*W FenceRcu-locksR* FenceRcu-locksRR FenceRcu-locksRW FenceRcu-locksW* FenceRcu-locksWR FenceRcu-locksWW FenceRcu-unlock FenceRcu-unlockd** FenceRcu-unlockd*R FenceRcu-unlockd*W FenceRcu-unlockdR* FenceRcu-unlockdRR FenceRcu-unlockdRW FenceRcu-unlockdW* FenceRcu-unlockdWR FenceRcu-unlockdWW FenceRcu-unlocks** FenceRcu-unlocks*R FenceRcu-unlocks*W FenceRcu-unlocksR* FenceRcu-unlocksRR FenceRcu-unlocksRW FenceRcu-unlocksW* FenceRcu-unlocksWR FenceRcu-unlocksWW FenceRmb FenceRmbd** FenceRmbd*R FenceRmbd*W FenceRmbdR* FenceRmbdRR FenceRmbdRW FenceRmbdW* FenceRmbdWR FenceRmbdWW FenceRmbs** FenceRmbs*R FenceRmbs*W FenceRmbsR* FenceRmbsRR FenceRmbsRW FenceRmbsW* FenceRmbsWR FenceRmbsWW FenceSync-rcu FenceSync-rcud** FenceSync-rcud*R FenceSync-rcud*W FenceSync-rcudR* FenceSync-rcudRR FenceSync-rcudRW FenceSync-rcudW* FenceSync-rcudWR FenceSync-rcudWW FenceSync-rcus** FenceSync-rcus*R FenceSync-rcus*W FenceSync-rcusR* FenceSync-rcusRR FenceSync-rcusRW FenceSync-rcusW* FenceSync-rcusWR FenceSync-rcusWW FenceWmb FenceWmbd** FenceWmbd*R FenceWmbd*W FenceWmbdR* FenceWmbdRR FenceWmbdRW FenceWmbdW* FenceWmbdWR FenceWmbdWW FenceWmbs** FenceWmbs*R FenceWmbs*W FenceWmbsR* FenceWmbsRR FenceWmbsRW FenceWmbsW* FenceWmbsWR FenceWmbsWW Fenced** Fenced*R Fenced*W FencedR* FencedRR FencedRW FencedW* FencedWR FencedWW Fences** Fences*R Fences*W FencesR* FencesRR FencesRW FencesW* FencesWR FencesWW FrBack FrLeave Fre Fri Hat Na Pod** Pod*R Pod*W PodR* PodRR PodRW PodW* PodWR PodWW Pos** Pos*R Pos*W PosR* PosRR PosRW PosW* PosWR PosWW R Read RfBack RfLeave Rfe Rfi Rmw W Write WsBack WsLeave Wse Wsi
>
> I added the following at the end:
>
> Please note that the above is a partial list. To see the full list of
> descriptors, execute the following command:
>
> $ diyone7 -bell linux-kernel.bell -show edges
Thanks. One more nit: I'd indent this and the above "norm7" commands as
we do in our "main" README.
>
> > I also notice that our current names for tests with fences (and cycle)
> > deviate from the corresponding 'norm7' results; e.g.,
> >
> > $ norm7 -bell linux-kernel.bell FenceWmbdWW Once Rfe Once FenceRmbdRR Once Fre Once | sed -e 's/:.*//g'
> > MP+fencewmbonceonce+fencermbonceonce
> >
> > while we use 'MP+wmbonceonce+rmbonceonce' (that is, we omit the 'fence'
> > prefixes).
>
> Would you be willing to send me a patch fixing them up?
Yes, I'll work this out.
Andrea
>
> Please see below for updated patch.
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit 04a897a8e202e8d79dd47910321f0e8efb081854
> Author: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
> Date: Fri May 25 12:02:53 2018 -0700
>
> EXP tools/memory-model: Add litmus-test naming scheme
>
> This commit documents the scheme used to generate the names for the
> litmus tests.
>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
> [ paulmck: Apply feedback from Andrea Parri. ]
>
> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 00140aaf58b7..9c0ea65c5362 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -1,4 +1,6 @@
> -This directory contains the following litmus tests:
> +============
> +LITMUS TESTS
> +============
>
> CoRR+poonceonce+Once.litmus
> Test of read-read coherence, that is, whether or not two
> @@ -151,3 +153,143 @@ Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
> A great many more litmus tests are available here:
>
> https://github.com/paulmckrcu/litmus
> +
> +==================
> +LITMUS TEST NAMING
> +==================
> +
> +Litmus tests are usually named based on their contents, which means that
> +looking at the name tells you what the litmus test does. The naming
> +scheme covers litmus tests having a single cycle that passes through
> +each process exactly once, so litmus tests not fitting this description
> +are named on an ad-hoc basis.
> +
> +The structure of a litmus-test name is the litmus-test class, a plus
> +sign ("+"), and one string for each process, separated by plus signs.
> +The end of the name is ".litmus".
> +
> +The litmus-test classes may be found in the infamous test6.pdf:
> +https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test6.pdf
> +Each class defines the pattern of accesses and of the variables accessed.
> +For example, if the one process writes to a pair of variables, and
> +the other process reads from these same variables, the corresponding
> +litmus-test class is "MP" (message passing), which may be found on the
> +left-hand end of the second row of tests on page one of test6.pdf.
> +
> +The strings used to identify the actions carried out by each process are
> +complex due to a desire to have short(er) names. Thus, there is a tool to
> +generate these strings from a given litmus test's actions. For example,
> +consider the processes from SB+rfionceonce-poonceonces.litmus:
> +
> + P0(int *x, int *y)
> + {
> + int r1;
> + int r2;
> +
> + WRITE_ONCE(*x, 1);
> + r1 = READ_ONCE(*x);
> + r2 = READ_ONCE(*y);
> + }
> +
> + P1(int *x, int *y)
> + {
> + int r3;
> + int r4;
> +
> + WRITE_ONCE(*y, 1);
> + r3 = READ_ONCE(*y);
> + r4 = READ_ONCE(*x);
> + }
> +
> +The next step is to construct a space-separated list of descriptors,
> +interleaving descriptions of the relation between a pair of consecutive
> +accesses with descriptions of the second access in the pair.
> +
> +P0()'s WRITE_ONCE() is read by its first READ_ONCE(), which is a
> +reads-from link (rf) and internal to the P0() process. This is
> +"rfi", which is an abbreviation for "reads-from internal". Because
> +some of the tools string these abbreviations together with space
> +characters separating processes, the first character is capitalized,
> +resulting in "Rfi".
> +
> +P0()'s second access is a READ_ONCE(), as opposed to (for example)
> +smp_load_acquire(), so next is "Once". Thus far, we have "Rfi Once".
> +
> +P0()'s third access is also a READ_ONCE(), but to y rather than x.
> +This is related to P0()'s second access by program order ("po"),
> +to a different variable ("d"), and both accesses are reads ("RR").
> +The resulting descriptor is "PodRR". Because P0()'s third access is
> +READ_ONCE(), we add another "Once" descriptor.
> +
> +A from-read ("fre") relation links P0()'s third to P1()'s first
> +access, and the resulting descriptor is "Fre". P1()'s first access is
> +WRITE_ONCE(), which as before gives the descriptor "Once". The string
> +thus far is thus "Rfi Once PodRR Once Fre Once".
> +
> +The remainder of P1() is similar to P0(), which means we add
> +"Rfi Once PodRR Once". Another fre links P1()'s last access to
> +P0()'s first access, which is WRITE_ONCE(), so we add "Fre Once".
> +The full string is thus:
> +
> + Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once
> +
> +This string can be given to the "norm7" and "classify7" tools to
> +produce the name:
> +
> +$ norm7 -bell linux-kernel.bell Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | sed -e 's/:.*//g'
> +SB+rfionceonce-poonceonces
> +
> +Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus
> +
> +
> +=======================
> +LITMUS TEST DESCRIPTORS
> +=======================
> +
> +These descriptors cover connections between consecutive accesses within
> +the cycle through a given litmus test:
> +
> +Fre: From-read external. The current process wrote a variable that
> + the previous process read. Example: The SB (store buffering) test.
> +Fri: From-read internal. This process read a variable and then
> + immediately wrote to it. Example: ???
> +PodRR: Program-order different variable, read followed by read.
> + This process read a variable and again read a different variable.
> + Example: The read-side process in the MP (message-passing) test.
> +PodRW: Program-order different variable, read followed by write.
> + This process read a variable and then wrote a different variable.
> + Example: The LB (load buffering) test.
> +PodWR: Program-order different variable, write followed by read.
> + This process wrote a variable and then read a different variable.
> + Example: The SB (store buffering) test.
> +PodWW: Program-order different variable, write followed by write.
> + This process wrote a variable and again wrote a different variable.
> + Example: The write-side process in the MP (message-passing) test.
> +PosRR: Program-order same variable, read followed by read.
> + This process read a variable and again read that same variable.
> + Example: ???
> +PosRW: Program-order same variable, read followed by write.
> + This process read a variable and then wrote that same variable.
> + Example: ???
> +PosWR: Program-order same variable, write followed by read.
> + This process wrote a variable and then read that same variable.
> + Example: ???
> +PosWW: Program-order same variable, write followed by write.
> + This process wrote a variable and again wrote that same variable.
> + Example: ???
> +Rfe: Read-from external. The current process read a variable written
> + by the previous process. Example: The MP (message passing) test.
> +Rfi: Read-from internal. The current process wrote a variable and then
> + immediately read the value back from it. For the purposes of
> + naming, Rfi acts identically to PosWR. However, there are subtle
> + but very real differences between them in other contexts.
> + Example: ???
> +Wse: Write same external. The current process wrote to a variable that
> + was also written to by the previous process. Example: ???
> +Wsi: Write same internal. The current process wrote to a variable and
> + then immediately wrote to it again. Example: ???
> +
> +Please note that the above is a partial list. To see the full list of
> +descriptors, execute the following command:
> +
> +$ diyone7 -bell linux-kernel.bell -show edges
>
