0001 ============
0002 LITMUS TESTS
0003 ============
0004
0005 CoRR+poonceonce+Once.litmus
0006 Test of read-read coherence, that is, whether or not two
0007 successive reads from the same variable are ordered.
0008
0009 CoRW+poonceonce+Once.litmus
0010 Test of read-write coherence, that is, whether or not a read
0011 from a given variable followed by a write to that same variable
0012 are ordered.
0013
0014 CoWR+poonceonce+Once.litmus
0015 Test of write-read coherence, that is, whether or not a write
0016 to a given variable followed by a read from that same variable
0017 are ordered.
0018
0019 CoWW+poonceonce.litmus
0020 Test of write-write coherence, that is, whether or not two
0021 successive writes to the same variable are ordered.
0022
0023 IRIW+fencembonceonces+OnceOnce.litmus
0024 Test of independent reads from independent writes with smp_mb()
0025 between each pairs of reads. In other words, is smp_mb()
0026 sufficient to cause two different reading processes to agree on
0027 the order of a pair of writes, where each write is to a different
0028 variable by a different process? This litmus test is forbidden
0029 by LKMM's propagation rule.
0030
0031 IRIW+poonceonces+OnceOnce.litmus
0032 Test of independent reads from independent writes with nothing
0033 between each pairs of reads. In other words, is anything at all
0034 needed to cause two different reading processes to agree on the
0035 order of a pair of writes, where each write is to a different
0036 variable by a different process?
0037
0038 ISA2+pooncelock+pooncelock+pombonce.litmus
0039 Tests whether the ordering provided by a lock-protected S
0040 litmus test is visible to an external process whose accesses are
0041 separated by smp_mb(). This addition of an external process to
0042 S is otherwise known as ISA2.
0043
0044 ISA2+poonceonces.litmus
0045 As below, but with store-release replaced with WRITE_ONCE()
0046 and load-acquire replaced with READ_ONCE().
0047
0048 ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
0049 Can a release-acquire chain order a prior store against
0050 a later load?
0051
0052 LB+fencembonceonce+ctrlonceonce.litmus
0053 Does a control dependency and an smp_mb() suffice for the
0054 load-buffering litmus test, where each process reads from one
0055 of two variables then writes to the other?
0056
0057 LB+poacquireonce+pooncerelease.litmus
0058 Does a release-acquire pair suffice for the load-buffering
0059 litmus test, where each process reads from one of two variables then
0060 writes to the other?
0061
0062 LB+poonceonces.litmus
0063 As above, but with store-release replaced with WRITE_ONCE()
0064 and load-acquire replaced with READ_ONCE().
0065
0066 LB+unlocklockonceonce+poacquireonce.litmus
0067 Does a unlock+lock pair provides ordering guarantee between a
0068 load and a store?
0069
0070 MP+onceassign+derefonce.litmus
0071 As below, but with rcu_assign_pointer() and an rcu_dereference().
0072
0073 MP+polockmbonce+poacquiresilsil.litmus
0074 Protect the access with a lock and an smp_mb__after_spinlock()
0075 in one process, and use an acquire load followed by a pair of
0076 spin_is_locked() calls in the other process.
0077
0078 MP+polockonce+poacquiresilsil.litmus
0079 Protect the access with a lock in one process, and use an
0080 acquire load followed by a pair of spin_is_locked() calls
0081 in the other process.
0082
0083 MP+polocks.litmus
0084 As below, but with the second access of the writer process
0085 and the first access of reader process protected by a lock.
0086
0087 MP+poonceonces.litmus
0088 As below, but without the smp_rmb() and smp_wmb().
0089
0090 MP+pooncerelease+poacquireonce.litmus
0091 As below, but with a release-acquire chain.
0092
0093 MP+porevlocks.litmus
0094 As below, but with the first access of the writer process
0095 and the second access of reader process protected by a lock.
0096
0097 MP+unlocklockonceonce+fencermbonceonce.litmus
0098 Does a unlock+lock pair provides ordering guarantee between a
0099 store and another store?
0100
0101 MP+fencewmbonceonce+fencermbonceonce.litmus
0102 Does a smp_wmb() (between the stores) and an smp_rmb() (between
0103 the loads) suffice for the message-passing litmus test, where one
0104 process writes data and then a flag, and the other process reads
0105 the flag and then the data. (This is similar to the ISA2 tests,
0106 but with two processes instead of three.)
0107
0108 R+fencembonceonces.litmus
0109 This is the fully ordered (via smp_mb()) version of one of
0110 the classic counterintuitive litmus tests that illustrates the
0111 effects of store propagation delays.
0112
0113 R+poonceonces.litmus
0114 As above, but without the smp_mb() invocations.
0115
0116 SB+fencembonceonces.litmus
0117 This is the fully ordered (again, via smp_mb() version of store
0118 buffering, which forms the core of Dekker's mutual-exclusion
0119 algorithm.
0120
0121 SB+poonceonces.litmus
0122 As above, but without the smp_mb() invocations.
0123
0124 SB+rfionceonce-poonceonces.litmus
0125 This litmus test demonstrates that LKMM is not fully multicopy
0126 atomic. (Neither is it other multicopy atomic.) This litmus test
0127 also demonstrates the "locations" debugging aid, which designates
0128 additional registers and locations to be printed out in the dump
0129 of final states in the herd7 output. Without the "locations"
0130 statement, only those registers and locations mentioned in the
0131 "exists" clause will be printed.
0132
0133 S+poonceonces.litmus
0134 As below, but without the smp_wmb() and acquire load.
0135
0136 S+fencewmbonceonce+poacquireonce.litmus
0137 Can a smp_wmb(), instead of a release, and an acquire order
0138 a prior store against a subsequent store?
0139
0140 WRC+poonceonces+Once.litmus
0141 WRC+pooncerelease+fencermbonceonce+Once.litmus
0142 These two are members of an extension of the MP litmus-test
0143 class in which the first write is moved to a separate process.
0144 The second is forbidden because smp_store_release() is
0145 A-cumulative in LKMM.
0146
0147 Z6.0+pooncelock+pooncelock+pombonce.litmus
0148 Is the ordering provided by a spin_unlock() and a subsequent
0149 spin_lock() sufficient to make ordering apparent to accesses
0150 by a process not holding the lock?
0151
0152 Z6.0+pooncelock+poonceLock+pombonce.litmus
0153 As above, but with smp_mb__after_spinlock() immediately
0154 following the spin_lock().
0155
0156 Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
0157 Is the ordering provided by a release-acquire chain sufficient
0158 to make ordering apparent to accesses by a process that does
0159 not participate in that release-acquire chain?
0160
0161 A great many more litmus tests are available here:
0162
0163 https://github.com/paulmckrcu/litmus
0164
0165 ==================
0166 LITMUS TEST NAMING
0167 ==================
0168
0169 Litmus tests are usually named based on their contents, which means that
0170 looking at the name tells you what the litmus test does. The naming
0171 scheme covers litmus tests having a single cycle that passes through
0172 each process exactly once, so litmus tests not fitting this description
0173 are named on an ad-hoc basis.
0174
0175 The structure of a litmus-test name is the litmus-test class, a plus
0176 sign ("+"), and one string for each process, separated by plus signs.
0177 The end of the name is ".litmus".
0178
0179 The litmus-test classes may be found in the infamous test6.pdf:
0180 https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test6.pdf
0181 Each class defines the pattern of accesses and of the variables accessed.
0182 For example, if the one process writes to a pair of variables, and
0183 the other process reads from these same variables, the corresponding
0184 litmus-test class is "MP" (message passing), which may be found on the
0185 left-hand end of the second row of tests on page one of test6.pdf.
0186
0187 The strings used to identify the actions carried out by each process are
0188 complex due to a desire to have short(er) names. Thus, there is a tool to
0189 generate these strings from a given litmus test's actions. For example,
0190 consider the processes from SB+rfionceonce-poonceonces.litmus:
0191
0192 P0(int *x, int *y)
0193 {
0194 int r1;
0195 int r2;
0196
0197 WRITE_ONCE(*x, 1);
0198 r1 = READ_ONCE(*x);
0199 r2 = READ_ONCE(*y);
0200 }
0201
0202 P1(int *x, int *y)
0203 {
0204 int r3;
0205 int r4;
0206
0207 WRITE_ONCE(*y, 1);
0208 r3 = READ_ONCE(*y);
0209 r4 = READ_ONCE(*x);
0210 }
0211
0212 The next step is to construct a space-separated list of descriptors,
0213 interleaving descriptions of the relation between a pair of consecutive
0214 accesses with descriptions of the second access in the pair.
0215
0216 P0()'s WRITE_ONCE() is read by its first READ_ONCE(), which is a
0217 reads-from link (rf) and internal to the P0() process. This is
0218 "rfi", which is an abbreviation for "reads-from internal". Because
0219 some of the tools string these abbreviations together with space
0220 characters separating processes, the first character is capitalized,
0221 resulting in "Rfi".
0222
0223 P0()'s second access is a READ_ONCE(), as opposed to (for example)
0224 smp_load_acquire(), so next is "Once". Thus far, we have "Rfi Once".
0225
0226 P0()'s third access is also a READ_ONCE(), but to y rather than x.
0227 This is related to P0()'s second access by program order ("po"),
0228 to a different variable ("d"), and both accesses are reads ("RR").
0229 The resulting descriptor is "PodRR". Because P0()'s third access is
0230 READ_ONCE(), we add another "Once" descriptor.
0231
0232 A from-read ("fre") relation links P0()'s third to P1()'s first
0233 access, and the resulting descriptor is "Fre". P1()'s first access is
0234 WRITE_ONCE(), which as before gives the descriptor "Once". The string
0235 thus far is thus "Rfi Once PodRR Once Fre Once".
0236
0237 The remainder of P1() is similar to P0(), which means we add
0238 "Rfi Once PodRR Once". Another fre links P1()'s last access to
0239 P0()'s first access, which is WRITE_ONCE(), so we add "Fre Once".
0240 The full string is thus:
0241
0242 Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once
0243
0244 This string can be given to the "norm7" and "classify7" tools to
0245 produce the name:
0246
0247 $ norm7 -bell linux-kernel.bell \
0248 Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | \
0249 sed -e 's/:.*//g'
0250 SB+rfionceonce-poonceonces
0251
0252 Adding the ".litmus" suffix: SB+rfionceonce-poonceonces.litmus
0253
0254 The descriptors that describe connections between consecutive accesses
0255 within the cycle through a given litmus test can be provided by the herd7
0256 tool (Rfi, Po, Fre, and so on) or by the linux-kernel.bell file (Once,
0257 Release, Acquire, and so on).
0258
0259 To see the full list of descriptors, execute the following command:
0260
0261 $ diyone7 -bell linux-kernel.bell -show edges
