diff options
Diffstat (limited to 'tools/memory-model')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 6 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 102 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.def | 1 | ||||
| -rw-r--r-- | tools/memory-model/litmus-tests/MP+poonceonces.litmus | 2 | ||||
| -rw-r--r-- | tools/memory-model/litmus-tests/README | 2 | ||||
| -rw-r--r-- | tools/memory-model/lock.cat | 2 | ||||
| -rw-r--r-- | tools/memory-model/scripts/README | 4 | ||||
| -rwxr-xr-x | tools/memory-model/scripts/checkalllitmus.sh | 2 | ||||
| -rwxr-xr-x | tools/memory-model/scripts/checklitmus.sh | 2 | ||||
| -rw-r--r-- | tools/memory-model/scripts/parseargs.sh | 2 | ||||
| -rw-r--r-- | tools/memory-model/scripts/runlitmushist.sh | 2 |
11 files changed, 96 insertions, 31 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index def9131d3d8e..5be86b1025e8 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -24,6 +24,7 @@ instructions RMW[{'once,'acquire,'release}] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || 'mb (*smp_mb*) || + 'barrier (*barrier*) || 'rcu-lock (*rcu_read_lock*) || 'rcu-unlock (*rcu_read_unlock*) || 'sync-rcu (*synchronize_rcu*) || @@ -76,3 +77,8 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep (* Validate SRCU dynamic match *) flag ~empty different-values(srcu-rscs) as srcu-bad-nesting + +(* Compute marked and plain memory accesses *) +let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | + LKR | LKW | UL | LF | RL | RU +let Plain = M \ Marked diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 8dcb37835b61..ea2ff4b94074 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -24,8 +24,14 @@ include "lock.cat" (* Basic relations *) (*******************) +(* Release Acquire *) +let acq-po = [Acquire] ; po ; [M] +let po-rel = [M] ; po ; [Release] +let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po + (* Fences *) -let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn] +let R4rmb = R \ Noreturn (* Reads for which rmb works *) +let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] let wmb = [W] ; fencerel(Wmb) ; [W] let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | @@ -34,13 +40,14 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; po ; [UL] ; (co | po) ; [LKW] ; fencerel(After-unlock-lock) ; [M]) let gp = po ; [Sync-rcu | Sync-srcu] ; po? - let strong-fence = mb | gp -(* Release Acquire *) -let acq-po = [Acquire] ; po ; [M] -let po-rel = [M] ; po ; [Release] -let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po +let nonrw-fence = strong-fence | po-rel | acq-po +let fence = nonrw-fence | wmb | rmb +let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | + Before-atomic | After-atomic | Acquire | Release | + Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | + (po ; [Release]) | ([Acquire] ; po) (**********************************) (* Fundamental coherence ordering *) @@ -61,21 +68,22 @@ empty rmw & (fre ; coe) as atomic let dep = addr | data let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr -let to-w = rwdep | (overwrite & int) -let to-r = addr | (dep ; rfi) -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) +let to-r = addr | (dep ; [Marked] ; rfi) let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) -let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po -let prop = (overwrite & ext)? ; cumul-fence* ; rfe? +let A-cumul(r) = (rfe ; [Marked])? ; r +let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | + po-unlock-rf-lock-po) ; [Marked] +let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; + [Marked] ; rfe? ; [Marked] (* * Happens Before: Ordering from the passage of time. * No fences needed here for prop because relation confined to one process. *) -let hb = ppo | rfe | ((prop \ id) & int) +let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] acyclic hb as happens-before (****************************************) @@ -83,7 +91,7 @@ acyclic hb as happens-before (****************************************) (* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* +let pb = prop ; strong-fence ; hb* ; [Marked] acyclic pb as propagation (*******) @@ -114,24 +122,28 @@ let rcu-link = po? ; hb* ; pb* ; prop ; po (* * Any sequence containing at least as many grace periods as RCU read-side - * critical sections (joined by rcu-link) acts as a generalized strong fence. + * critical sections (joined by rcu-link) induces order like a generalized + * inter-CPU strong fence. * Likewise for SRCU grace periods and read-side critical sections, provided * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same * struct srcu_struct location. *) -let rec rcu-fence = rcu-gp | srcu-gp | +let rec rcu-order = rcu-gp | srcu-gp | (rcu-gp ; rcu-link ; rcu-rscsi) | ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | (rcu-rscsi ; rcu-link ; rcu-gp) | ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) | - (rcu-fence ; rcu-link ; rcu-fence) + (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | + ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | + (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | + ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | + (rcu-order ; rcu-link ; rcu-order) +let rcu-fence = po ; rcu-order ; po? +let fence = fence | rcu-fence +let strong-fence = strong-fence | rcu-fence (* rb orders instructions just as pb does *) -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* +let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] irreflexive rb as rcu @@ -143,3 +155,49 @@ irreflexive rb as rcu * let xb = hb | pb | rb * acyclic xb as executes-before *) + +(*********************************) +(* Plain accesses and data races *) +(*********************************) + +(* Warn about plain writes and marked accesses in the same region *) +let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | + ([Marked] ; (po-loc \ barrier) ; [Plain & W]) +flag ~empty mixed-accesses as mixed-accesses + +(* Executes-before and visibility *) +let xbstar = (hb | pb | rb)* +let vis = cumul-fence* ; rfe? ; [Marked] ; + ((strong-fence ; [Marked] ; xbstar) | (xbstar & int)) + +(* Boundaries for lifetimes of plain accesses *) +let w-pre-bounded = [Marked] ; (addr | fence)? +let r-pre-bounded = [Marked] ; (addr | nonrw-fence | + ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? +let w-post-bounded = fence? ; [Marked] +let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; + [Marked] + +(* Visibility and executes-before for plain accesses *) +let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) | + (w-post-bounded ; vis ; w-pre-bounded) +let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) | + (w-post-bounded ; vis ; r-pre-bounded) +let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded) + +(* Potential races *) +let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) + +(* Coherence requirements for plain accesses *) +let wr-incoh = pre-race & rf & rw-xbstar^-1 +let rw-incoh = pre-race & fr & wr-vis^-1 +let ww-incoh = pre-race & co & ww-vis^-1 +empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence + +(* Actual races *) +let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) +let ww-race = (pre-race & co) \ ww-nonrace +let wr-race = (pre-race & (co? ; rf)) \ wr-vis +let rw-race = (pre-race & fr) \ rw-xbstar + +flag ~empty (ww-race | wr-race | rw-race) as data-race diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index 551eeaa389d4..ef0f3c1850de 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -24,6 +24,7 @@ smp_mb__before_atomic() { __fence{before-atomic}; } smp_mb__after_atomic() { __fence{after-atomic}; } smp_mb__after_spinlock() { __fence{after-spinlock}; } smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; } +barrier() { __fence{barrier}; } // Exchange xchg(X,V) __xchg{mb}(X,V) diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus index b2b60b84fb9d..172f0145301c 100644 --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus @@ -1,7 +1,7 @@ C MP+poonceonces (* - * Result: Maybe + * Result: Sometimes * * Can the counter-intuitive message-passing outcome be prevented with * no ordering at all? diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README index 5ee08f129094..681f9067fa9e 100644 --- a/tools/memory-model/litmus-tests/README +++ b/tools/memory-model/litmus-tests/README @@ -244,7 +244,7 @@ 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 +within the cycle through a given litmus test can be provided by the herd7 tool (Rfi, Po, Fre, and so on) or by the linux-kernel.bell file (Once, Release, Acquire, and so on). diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index a059d1a6d8a2..6b52f365d73a 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -11,7 +11,7 @@ include "cross.cat" (* - * The lock-related events generated by herd are as follows: + * The lock-related events generated by herd7 are as follows: * * LKR Lock-Read: the read part of a spin_lock() or successful * spin_trylock() read-modify-write event pair diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 29375a1fbbfa..095c7eb36f9f 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -22,7 +22,7 @@ checklitmushist.sh Run all litmus tests having .litmus.out files from previous initlitmushist.sh or newlitmushist.sh runs, comparing the - herd output to that of the original runs. + herd7 output to that of the original runs. checklitmus.sh @@ -43,7 +43,7 @@ initlitmushist.sh judgelitmus.sh - Given a .litmus file and its .litmus.out herd output, check the + Given a .litmus file and its .litmus.out herd7 output, check the .litmus.out file against the .litmus file's "Result:" comment to judge whether the test ran correctly. Not normally run manually, provided instead for use by other scripts. diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index b35fcd61ecf6..3c0c7fbbd223 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -1,7 +1,7 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Run herd tests on all .litmus files in the litmus-tests directory +# Run herd7 tests on all .litmus files in the litmus-tests directory # and check each file's result against a "Result:" comment within that # litmus test. If the verification result does not match that specified # in the litmus test, this script prints an error message prefixed with diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh index dd08801a30b0..11461ed40b5e 100755 --- a/tools/memory-model/scripts/checklitmus.sh +++ b/tools/memory-model/scripts/checklitmus.sh @@ -1,7 +1,7 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Run a herd test and invokes judgelitmus.sh to check the result against +# Run a herd7 test and invokes judgelitmus.sh to check the result against # a "Result:" comment within the litmus test. It also outputs verification # results to a file whose name is that of the specified litmus test, but # with ".out" appended. diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 859e1d581e05..40f52080fdbd 100644 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -91,7 +91,7 @@ do shift ;; --herdopts|--herdopt) - checkarg --destdir "(herd options)" "$#" "$2" '.*' '^--' + checkarg --destdir "(herd7 options)" "$#" "$2" '.*' '^--' LKMM_HERD_OPTIONS="$2" shift ;; diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh index e507f5f933d5..6ed376f495bb 100644 --- a/tools/memory-model/scripts/runlitmushist.sh +++ b/tools/memory-model/scripts/runlitmushist.sh @@ -79,7 +79,7 @@ then echo ' ---' Summary: 1>&2 grep '!!!' $T/*.sh.out 1>&2 nfail="`grep '!!!' $T/*.sh.out | wc -l`" - echo 'Number of failed herd runs (e.g., timeout): ' $nfail 1>&2 + echo 'Number of failed herd7 runs (e.g., timeout): ' $nfail 1>&2 exit 1 else echo All runs completed successfully. 1>&2 |