Add litmus-test naming scheme
RFC PATCH 1/1 Add litmus-test naming scheme
This commit documents the scheme used to generate the names for the litmus tests.
--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)
tools/memory-model/litmus-tests/README +135 -1
@@ -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,135 @@ 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 finite-length 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 | classify7 -bell linux-kernel.bell -diyone | 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: + +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 rrote 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. Example: ??? + Comparison to PosWR??? +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: ???
Quoted 28 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)tools/memory-model/litmus-tests/README +7
-1@@ -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,135 @@ Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus A great many more litmus tests are available here: https://github.com/paulmckrcu/litmus + +================== +LITMUS TEST NAMING +==================
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 169
Quoted 10 lines
tools/memory-model/litmus-tests/README +10
-0+ +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".
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...).
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
Quoted 11 lines
tools/memory-model/litmus-tests/README +11
-0+ +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 finite-length names.
I'm not sure what you mean here: can you elaborate/rephrase?
Quoted 51 lines
Thus, there is a
tools/memory-model/litmus-tests/README +50
-0+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
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 240
Quoted 10 lines
tools/memory-model/litmus-tests/README +10
-0+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 | classify7 -bell linux-kernel.bell -diyone | sed -e 's/:.*//g' +SB+rfionceonce-poonceonces
We should check for the required version of herdtools7; a quick search here pointed out:
ad5681da10fafb ("gen: add the tool 'norm' that normalise and name one cycle given as command line arguments.")
(so after v7.49), but I do remember a 'norm7' tool during my 'Parisian days', mmh...
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'
but we might want to list other commands for backward compatibility.
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 249
Quoted 9 lines
tools/memory-model/litmus-tests/README +9
-0+ +Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus + + +======================= +LITMUS TEST DESCRIPTORS +======================= + +These descriptors cover connections between consecutive accesses:
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 ;-)
Quoted 18 lines
tools/memory-model/litmus-tests/README +18
-0+ +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.
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 277
Quoted 10 lines
tools/memory-model/litmus-tests/README +10
-0+ 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 rrote that same variable.
s/rrote/wrote
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 283
Quoted 6 lines
tools/memory-model/litmus-tests/README +6
-0+ 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. Example: ??? + Comparison to PosWR???
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)tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 287
Quoted 4 lines
tools/memory-model/litmus-tests/README +4
-0+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: ???
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.")
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).
Andrea
Quoted 1 line
Quoted 43 lines · Andrea Parri
Quoted 28 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)tools/memory-model/litmus-tests/README +7
-1@@ -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,135 @@ Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus A great many more litmus tests are available here: https://github.com/paulmckrcu/litmus + +================== +LITMUS TEST NAMING +==================tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 169
Quoted 10 lines
tools/memory-model/litmus-tests/README +10
-0+ +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".We used to distinguigh between the test name and the test filename; we currently have only one test whose name ends with .litmus:
Quoted 3 lines
ISA2+pooncelock+pooncelock+pombonce.litmus
(that I missed until now...).
I queued a commit to fix this with your Reported-by, good catch!
Quoted 5 lines
Quoted 5 lines
tools/memory-model/litmus-tests/README +5
-0+ +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
Quoted 8 lines
tools/memory-model/litmus-tests/README Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus · line 180
Quoted 6 lines
tools/memory-model/litmus-tests/README +6
-0+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 finite-length names.I'm not sure what you mean here: can you elaborate/rephrase?
If we used Rfi, PodRW, and so on, the names would be even longer than they are now. This sentence now reads as follows:
The strings used to identify the actions carried out by each process are complex due to a desire to have short(er) names.
Quoted 67 lines
Quoted 51 lines
Thus, there is a
tools/memory-model/litmus-tests/README +50
-0+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 totools/memory-model/litmus-tests/README
Quoted 10 lines
tools/memory-model/litmus-tests/README +10
-0+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 | classify7 -bell linux-kernel.bell -diyone | sed -e 's/:.*//g' +SB+rfionceonce-poonceoncesWe should check for the required version of herdtools7; a quick search here pointed out:
ad5681da10fafb("gen: add the tool 'norm' that normalise and name one cycle given as command line arguments.")
Quoted 7 lines
(so after v7.49), but I do remember a 'norm7' tool during my 'Parisian days', mmh...
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?
Quoted 1 line
but we might want to list other commands for backward compatibility.
By the time this hits mainline, I bet there will be another herdtools release, and the version number can be updated when that happens. ;-)
Quoted 5 lines
Quoted 5 lines
tools/memory-model/litmus-tests/README +5
-0+ +Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus + + +=======================
Quoted 8 lines
tools/memory-model/litmus-tests/README
Quoted 4 lines
tools/memory-model/litmus-tests/README +4
-0+LITMUS TEST DESCRIPTORS +======================= + +These descriptors cover connections between consecutive accesses: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?
These descriptors cover connections between consecutive accesses within the cycle through a given litmus test:
Quoted 22 lines
Quoted 22 lines
tools/memory-model/litmus-tests/README +22
-0+ +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.
Quoted 8 lines
tools/memory-model/litmus-tests/README
Quoted 6 lines
tools/memory-model/litmus-tests/README +6
-0+ 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 rrote that same variable.s/rrote/wrote
Good catch, fixed.
Quoted 26 lines
tools/memory-model/litmus-tests/README
Quoted 6 lines
tools/memory-model/litmus-tests/README +6
-0+ 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. Example: ??? + Comparison to PosWR???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)
Quoted 15 lines
$ 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. However, there are subtle
but very real differences between them in other contexts.
Example: ???
Quoted 7 lines
tools/memory-model/litmus-tests/README
Quoted 4 lines
tools/memory-model/litmus-tests/README +4
-0+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: ???The list of descriptors is incomplete; the command:
Quoted 6 lines
$ diyone7 -bell linux-kernel.bell -show edgesshows 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 Fe nceRcu-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* Fenc eWmbsRR 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
Quoted 8 lines
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+fencermbonceoncewhile we use 'MP+wmbonceonce+rmbonceonce' (that is, we omit the 'fence' prefixes).
Would you be willing to send me a patch fixing them up?
Please see below for updated patch.
Thanx, Paul
------------------------------------------------------------------------
commit 04a897a8e202e8d79dd47910321f0e8efb081854
Author: Paul E. McKenney <[email protected]> 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.
tools/memory-model/litmus-tests/README +143 -1
@@ -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
[...]
Quoted 8 lines
Quoted 6 lines
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.
Quoted 6 lines
Quoted 4 lines
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 "\"?
Quoted 7 lines
Quoted 3 lines
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.
Quoted 35 lines
Quoted 19 lines
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)Quoted 15 lines
$ 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)
Quoted 5 lines
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...
Quoted 2 lines
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. ;-)
Quoted 11 lines
Quoted 8 lines
The list of descriptors is incomplete; the command:
$ diyone7 -bell linux-kernel.bell -show edgesshows 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!!!
Quoted 8 lines
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.
Quoted 11 lines
Quoted 9 lines
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+fencermbonceoncewhile 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
Quoted 176 lines
Please see below for updated patch.
Thanx, Paul
------------------------------------------------------------------------
commit
04a897a8e202e8d79dd47910321f0e8efb081854Author: Paul E. McKenney <[email protected]> Date: Fri May 25 12:02:53 2018 -0700EXP
tools/memory-model: Add litmus-test naming schemeThis commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>[ paulmck: Apply feedback from Andrea Parri. ]tools/memory-model/litmus-tests/README +143
-1@@ -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
Quoted 16 lines · Andrea Parri
[...]
Quoted 8 lines
Quoted 6 lines
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.
Quoted 3 lines
Quoted 3 lines
I also notice that, with the current version, the above command can be simplified to:
Quoted 6 lines
Quoted 3 lines
Quoted 1 line
$ 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 "\"?
We could, but combined with your later request for indentation, we end up with something like this:
$ norm7 -bell linux-kernel.bell \ Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | \ sed -e 's/:.*//g' SB+rfionceonce-poonceonces
In the immortal words of MSDOS, are you sure? ;-)
Quoted 45 lines
Quoted 7 lines
Quoted 3 lines
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.
Quoted 35 lines
Quoted 34 lines
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)
Quoted 7 lines
Quoted 5 lines
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...
Right you are! How about this, then?
Rfi: Read-from internal. The current process wrote a variable and then
immediately read the value back from it. For the purposes of litmus-test code generation, Rfi acts identically to PosWR. However, they differ for purposes of naming, and they also result in different "exists" clauses.
Example: ???
Quoted 4 lines
Quoted 2 lines
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. ;-)
If you didn't know better, you might even think that I was a native English speaker! ;-)
Quoted 4 lines
Quoted 4 lines
Quoted 4 lines
The list of descriptors is incomplete; the command:
$ diyone7 -bell linux-kernel.bell -show edges
Quoted 8 lines
Quoted 8 lines
Quoted 4 lines
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-ato
mic 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
Quoted 10 lines
Quoted 7 lines
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 edgesThanks. One more nit: I'd indent this and the above "norm7" commands as we do in our "main" README.
Done!
Quoted 6 lines
Quoted 6 lines
Quoted 6 lines
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
Quoted 6 lines
Quoted 4 lines
Quoted 2 lines
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.
Thanks in advance!
Thanx, Paul
Quoted 180 lines
Andrea
Quoted 176 lines
Please see below for updated patch.
Thanx, Paul
------------------------------------------------------------------------
commit
04a897a8e202e8d79dd47910321f0e8efb081854Author: Paul E. McKenney <[email protected]> Date: Fri May 25 12:02:53 2018 -0700EXP
tools/memory-model: Add litmus-test naming schemeThis commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>[ paulmck: Apply feedback from Andrea Parri. ]tools/memory-model/litmus-tests/README +143
-1@@ -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
[...]
Quoted 6 lines
Quoted 2 lines
Right, thanks. Ah, maybe we should strive to meet the 80-chars bound by splitting the command with "\"?
We could, but combined with your later request for indentation, we end up with something like this:
Quoted 6 lines
$ norm7 -bell linux-kernel.bell \ Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | \ sed -e 's/:.*//g' SB+rfionceonce-poonceoncesIn the immortal words of MSDOS, are you sure? ;-)
I find it more readable, but it's just taste ;-) Commands are indented with 2 spaces in the other README.
Quoted 10 lines
Quoted 1 line
Well, "Rfi" produces "rfi" while "PosWR" produces "pos" for a name...
Right you are! How about this, then?
Rfi: Read-from internal. The current process wrote a variable and then
immediately read the value back from it. For the purposes of litmus-test code generation, Rfi acts identically to PosWR. However, they differ for purposes of naming, and they also result in different "exists" clauses.
Example: ???
LGTM, thanks.
Andrea
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)
Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
Cheers,
Will
Quoted 16 lines · Will Deacon
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Quoted 4 lines
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
We would still need at least a pointer from the Linux kernel to that documentation, but I am happy either way. We probably need examples of the common cases, but probably not a full exposition of all the available herd7 edges.
Should this be in the herdtools7 documentation, or as added detail from a variation on the "diyone7 -bell linux-kernel.bell -show edges" command? If the latter, I suppose that the ones coming from the .bell file might simply be labelled as such.
Thanx, Paul
Quoted 22 lines · Paul E. McKenney
Quoted 16 lines · Will Deacon
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Quoted 4 lines
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
Quoted 4 lines
We would still need at least a pointer from the Linux kernel to that documentation, but I am happy either way. We probably need examples of the common cases, but probably not a full exposition of all the available herd7 edges.
Completely agreed.
Quoted 4 lines
Should this be in the herdtools7 documentation, or as added detail from a variation on the "diyone7 -bell linux-kernel.bell -show edges" command? If the latter, I suppose that the ones coming from the .bell file might simply be labelled as such.
Many of the edges aren't specific to the Linux kernel, so I think they should be part of the diyone7 documentation. We could then describe only the additional edges added by the kernel memory model (e.g. "Once") in the kernel documentation.
Will
Quoted 35 lines · Will Deacon
Quoted 22 lines · Paul E. McKenney
Quoted 16 lines · Will Deacon
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Quoted 4 lines
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
Quoted 4 lines
We would still need at least a pointer from the Linux kernel to that documentation, but I am happy either way. We probably need examples of the common cases, but probably not a full exposition of all the available herd7 edges.
Completely agreed.
Quoted 4 lines
Should this be in the herdtools7 documentation, or as added detail from a variation on the "diyone7 -bell linux-kernel.bell -show edges" command? If the latter, I suppose that the ones coming from the .bell file might simply be labelled as such.
Quoted 4 lines
Many of the edges aren't specific to the Linux kernel, so I think they should be part of the diyone7 documentation. We could then describe only the additional edges added by the kernel memory model (e.g. "Once") in the kernel documentation.
And there are a -lot- of them, and they are likely to change going forward, both in herd7 and in linux-kernel.bell. How about if I give examples and say where they are from and how to get a list, as in the following --squash commit to be merged with the orginal?
Thanx, Paul
------------------------------------------------------------------------
commit e366b8cd832535894c55265c112355c4de9a3247
Author: Paul E. McKenney <[email protected]> Date: Wed Sep 5 15:38:00 2018 -0700
squash! EXP tools/memory-model: Add litmus-test naming scheme
tools/memory-model/litmus-tests/README +5 -50
@@ -243,56 +243,11 @@ produce the name: Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus +The descriptors that describe connections between consecutive accesses +within the cycle through a given litmus test can be provided by the herd +tool (Rfi, Po, Fre, and so on) or by the linux-kernel.bell file (Once, +Release, Acquire, and so on). -======================= -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 litmus-test code generation, Rfi acts identically to PosWR. - However, they differ for purposes of naming, and they also result - in different "exists" clauses. - 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: +To see the full list of descriptors, execute the following command: $ diyone7 -bell linux-kernel.bell -show edges
Will Deacon
Acked-byQuoted 41 lines · Paul E. McKenney
Quoted 35 lines · Will Deacon
Quoted 22 lines · Paul E. McKenney
Quoted 16 lines · Will Deacon
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Quoted 4 lines
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
Quoted 4 lines
We would still need at least a pointer from the Linux kernel to that documentation, but I am happy either way. We probably need examples of the common cases, but probably not a full exposition of all the available herd7 edges.
Completely agreed.
Quoted 4 lines
Should this be in the herdtools7 documentation, or as added detail from a variation on the "diyone7 -bell linux-kernel.bell -show edges" command? If the latter, I suppose that the ones coming from the .bell file might simply be labelled as such.
Quoted 4 lines
Many of the edges aren't specific to the Linux kernel, so I think they should be part of the diyone7 documentation. We could then describe only the additional edges added by the kernel memory model (e.g. "Once") in the kernel documentation.
Quoted 4 lines
And there are a -lot- of them, and they are likely to change going forward, both in herd7 and in linux-kernel.bell. How about if I give examples and say where they are from and how to get a list, as in the following --squash commit to be merged with the orginal?
Sure, that looks much easier to maintain. With that, you can add my ack:
Cheers,
Will
Quoted 78 lines
------------------------------------------------------------------------
commit
e366b8cd832535894c55265c112355c4de9a3247Author: Paul E. McKenney <[email protected]> Date: Wed Sep 5 15:38:00 2018 -0700squash! EXP
tools/memory-model: Add litmus-test naming schemeSigned-off-by Paul E. McKenney <[email protected]>[ paulmck: Apply feedback from Will Deacon. ]tools/memory-model/litmus-tests/README +5
-50@@ -243,56 +243,11 @@ produce the name: Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus +The descriptors that describe connections between consecutive accesses +within the cycle through a given litmus test can be provided by the herd +tool (Rfi, Po, Fre, and so on) or by the linux-kernel.bell file (Once, +Release, Acquire, and so on). -======================= -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 litmus-test code generation, Rfi acts identically to PosWR. - However, they differ for purposes of naming, and they also result - in different "exists" clauses. - 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: +To see the full list of descriptors, execute the following command: $ diyone7 -bell linux-kernel.bell -show edges
Paul E. McKenney
AppliedQuoted 42 lines · Will Deacon
Quoted 41 lines · Paul E. McKenney
Quoted 39 lines · Will Deacon
Quoted 22 lines · Paul E. McKenney
Quoted 16 lines · Will Deacon
Hi Paul,
Quoted 7 lines · Paul E. McKenney
This commit documents the scheme used to generate the names for the litmus tests.
Signed-off-by Paul E. McKenney <[email protected]>--- README | 136 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-)Whilst I think documentation like this is extremely important for users, this feels like it's documenting how to drive parts of diy and I'm not convinced that it belongs in the kernel source tree as long as the projects remain separate.
Quoted 4 lines
Why not contribute this to the herdtools7 documentation, then just reference that from here? That would also be helpful for other people interested in memory models, but perhaps not interested in Linux (assuming such people exist ;).
Quoted 4 lines
We would still need at least a pointer from the Linux kernel to that documentation, but I am happy either way. We probably need examples of the common cases, but probably not a full exposition of all the available herd7 edges.
Completely agreed.
Quoted 4 lines
Should this be in the herdtools7 documentation, or as added detail from a variation on the "diyone7 -bell linux-kernel.bell -show edges" command? If the latter, I suppose that the ones coming from the .bell file might simply be labelled as such.
Many of the edges aren't specific to the Linux kernel, so I think they should be part of the diyone7 documentation. We could then describe only the additional edges added by the kernel memory model (e.g. "Once") in the kernel documentation.
Quoted 8 lines
Quoted 4 lines
And there are a -lot- of them, and they are likely to change going forward, both in herd7 and in linux-kernel.bell. How about if I give examples and say where they are from and how to get a list, as in the following --squash commit to be merged with the orginal?
Sure, that looks much easier to maintain. With that, you can add my ack:
Acked-by Will Deacon <[email protected]>
Applied, thank you!
And the lkmm branch has finally been updated to indicate the three commits that have acks/reviews and thus that appear ready for the next merge window, give or take the ongoing discussions.
Thanx, Paul