diff options
Diffstat (limited to 'tools/memory-model/README')
| -rw-r--r-- | tools/memory-model/README | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/tools/memory-model/README b/tools/memory-model/README index ee987ce20aae..acf9077cffaa 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README | |||
| @@ -171,6 +171,12 @@ The Linux-kernel memory model has the following limitations: | |||
| 171 | particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" | 171 | particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" |
| 172 | and "A WARNING" sections). | 172 | and "A WARNING" sections). |
| 173 | 173 | ||
| 174 | Note that this limitation in turn limits LKMM's ability to | ||
| 175 | accurately model address, control, and data dependencies. | ||
| 176 | For example, if the compiler can deduce the value of some variable | ||
| 177 | carrying a dependency, then the compiler can break that dependency | ||
| 178 | by substituting a constant of that value. | ||
| 179 | |||
| 174 | 2. Multiple access sizes for a single variable are not supported, | 180 | 2. Multiple access sizes for a single variable are not supported, |
| 175 | and neither are misaligned or partially overlapping accesses. | 181 | and neither are misaligned or partially overlapping accesses. |
| 176 | 182 | ||
| @@ -190,6 +196,36 @@ The Linux-kernel memory model has the following limitations: | |||
| 190 | However, a substantial amount of support is provided for these | 196 | However, a substantial amount of support is provided for these |
| 191 | operations, as shown in the linux-kernel.def file. | 197 | operations, as shown in the linux-kernel.def file. |
| 192 | 198 | ||
| 199 | a. When rcu_assign_pointer() is passed NULL, the Linux | ||
| 200 | kernel provides no ordering, but LKMM models this | ||
| 201 | case as a store release. | ||
| 202 | |||
| 203 | b. The "unless" RMW operations are not currently modeled: | ||
| 204 | atomic_long_add_unless(), atomic_add_unless(), | ||
| 205 | atomic_inc_unless_negative(), and | ||
| 206 | atomic_dec_unless_positive(). These can be emulated | ||
| 207 | in litmus tests, for example, by using atomic_cmpxchg(). | ||
| 208 | |||
| 209 | c. The call_rcu() function is not modeled. It can be | ||
| 210 | emulated in litmus tests by adding another process that | ||
| 211 | invokes synchronize_rcu() and the body of the callback | ||
| 212 | function, with (for example) a release-acquire from | ||
| 213 | the site of the emulated call_rcu() to the beginning | ||
| 214 | of the additional process. | ||
| 215 | |||
| 216 | d. The rcu_barrier() function is not modeled. It can be | ||
| 217 | emulated in litmus tests emulating call_rcu() via | ||
| 218 | (for example) a release-acquire from the end of each | ||
| 219 | additional call_rcu() process to the site of the | ||
| 220 | emulated rcu-barrier(). | ||
| 221 | |||
| 222 | e. Sleepable RCU (SRCU) is not modeled. It can be | ||
| 223 | emulated, but perhaps not simply. | ||
| 224 | |||
| 225 | f. Reader-writer locking is not modeled. It can be | ||
| 226 | emulated in litmus tests using atomic read-modify-write | ||
| 227 | operations. | ||
| 228 | |||
| 193 | The "herd7" tool has some additional limitations of its own, apart from | 229 | The "herd7" tool has some additional limitations of its own, apart from |
| 194 | the memory model: | 230 | the memory model: |
| 195 | 231 | ||
| @@ -204,3 +240,6 @@ the memory model: | |||
| 204 | Some of these limitations may be overcome in the future, but others are | 240 | Some of these limitations may be overcome in the future, but others are |
| 205 | more likely to be addressed by incorporating the Linux-kernel memory model | 241 | more likely to be addressed by incorporating the Linux-kernel memory model |
| 206 | into other tools. | 242 | into other tools. |
| 243 | |||
| 244 | Finally, please note that LKMM is subject to change as hardware, use cases, | ||
| 245 | and compilers evolve. | ||
