diff options
| author | Linus Torvalds <torvalds@linux-foundation.org> | 2022-01-11 09:38:03 -0800 |
|---|---|---|
| committer | Linus Torvalds <torvalds@linux-foundation.org> | 2022-01-11 09:38:03 -0800 |
| commit | 1c824bf768d69fce36de748c60c7197a2b838944 (patch) | |
| tree | 4220c2d4a65d7876913dcb9bad9f4aadf3250557 /tools/memory-model/linux-kernel.cat | |
| parent | e7d38f16c20bf2a9b2502bb1d7407360d09a836a (diff) | |
| parent | c438b7d860b4c1acb4ebff6d8d946d593ca5fe1e (diff) | |
Merge tag 'lkmm.2022.01.09a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu
Pull memory model documentation updates from Paul McKenney:
"This series contains documentation and litmus tests for locking,
courtesy of Boqun Feng"
* tag 'lkmm.2022.01.09a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu:
tools/memory-model: litmus: Add two tests for unlock(A)+lock(B) ordering
tools/memory-model: doc: Describe the requirement of the litmus-tests directory
tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU
Diffstat (limited to 'tools/memory-model/linux-kernel.cat')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 2a9b4fe4a84e..d70315fddef6 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -27,7 +27,7 @@ include "lock.cat" (* 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 po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po (* Fences *) let R4rmb = R \ Noreturn (* Reads for which rmb works *) @@ -70,12 +70,12 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr 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) +let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = (rfe ; [Marked])? ; r let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-rf-lock-po) ; [Marked] + po-unlock-lock-po) ; [Marked] let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] |