-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'lkmm' of git://git.kernel.org/pub/scm/linux/kernel/git/…
…paulmck/linux-rcu into locking/core Pull v5.9 LKMM changes from Paul E. McKenney. Mostly documentation changes, but also some new litmus tests for atomic ops. Signed-off-by: Ingo Molnar <mingo@kernel.org>
- Loading branch information
Showing
11 changed files
with
285 additions
and
58 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
============ | ||
LITMUS TESTS | ||
============ | ||
|
||
Each subdirectory contains litmus tests that are typical to describe the | ||
semantics of respective kernel APIs. | ||
For more information about how to "run" a litmus test or how to generate | ||
a kernel test module based on a litmus test, please see | ||
tools/memory-model/README. | ||
|
||
|
||
atomic (/atomic derectory) | ||
-------------------------- | ||
|
||
Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus | ||
Test that an atomic RMW followed by a smp_mb__after_atomic() is | ||
stronger than a normal acquire: both the read and write parts of | ||
the RMW are ordered before the subsequential memory accesses. | ||
|
||
Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus | ||
Test that atomic_set() cannot break the atomicity of atomic RMWs. | ||
NOTE: Require herd7 7.56 or later which supports "(void)expr". | ||
|
||
|
||
RCU (/rcu directory) | ||
-------------------- | ||
|
||
MP+onceassign+derefonce.litmus (under tools/memory-model/litmus-tests/) | ||
Demonstrates the use of rcu_assign_pointer() and rcu_dereference() to | ||
ensure that an RCU reader will not see pre-initialization garbage. | ||
|
||
RCU+sync+read.litmus | ||
RCU+sync+free.litmus | ||
Both the above litmus tests demonstrate the RCU grace period guarantee | ||
that an RCU read-side critical section can never span a grace period. |
32 changes: 32 additions & 0 deletions
32
...mentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire | ||
|
||
(* | ||
* Result: Never | ||
* | ||
* Test that an atomic RMW followed by a smp_mb__after_atomic() is | ||
* stronger than a normal acquire: both the read and write parts of | ||
* the RMW are ordered before the subsequential memory accesses. | ||
*) | ||
|
||
{ | ||
} | ||
|
||
P0(int *x, atomic_t *y) | ||
{ | ||
int r0; | ||
int r1; | ||
|
||
r0 = READ_ONCE(*x); | ||
smp_rmb(); | ||
r1 = atomic_read(y); | ||
} | ||
|
||
P1(int *x, atomic_t *y) | ||
{ | ||
atomic_inc(y); | ||
smp_mb__after_atomic(); | ||
WRITE_ONCE(*x, 1); | ||
} | ||
|
||
exists | ||
(0:r0=1 /\ 0:r1=0) |
25 changes: 25 additions & 0 deletions
25
Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
C Atomic-RMW-ops-are-atomic-WRT-atomic_set | ||
|
||
(* | ||
* Result: Never | ||
* | ||
* Test that atomic_set() cannot break the atomicity of atomic RMWs. | ||
* NOTE: This requires herd7 7.56 or later which supports "(void)expr". | ||
*) | ||
|
||
{ | ||
atomic_t v = ATOMIC_INIT(1); | ||
} | ||
|
||
P0(atomic_t *v) | ||
{ | ||
(void)atomic_add_unless(v, 1, 0); | ||
} | ||
|
||
P1(atomic_t *v) | ||
{ | ||
atomic_set(v, 0); | ||
} | ||
|
||
exists | ||
(v=2) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
C RCU+sync+free | ||
|
||
(* | ||
* Result: Never | ||
* | ||
* This litmus test demonstrates that an RCU reader can never see a write that | ||
* follows a grace period, if it did not see writes that precede that grace | ||
* period. | ||
* | ||
* This is a typical pattern of RCU usage, where the write before the grace | ||
* period assigns a pointer, and the writes following the grace period destroy | ||
* the object that the pointer used to point to. | ||
* | ||
* This is one implication of the RCU grace-period guarantee, which says (among | ||
* other things) that an RCU read-side critical section cannot span a grace period. | ||
*) | ||
|
||
{ | ||
int x = 1; | ||
int *y = &x; | ||
int z = 1; | ||
} | ||
|
||
P0(int *x, int *z, int **y) | ||
{ | ||
int *r0; | ||
int r1; | ||
|
||
rcu_read_lock(); | ||
r0 = rcu_dereference(*y); | ||
r1 = READ_ONCE(*r0); | ||
rcu_read_unlock(); | ||
} | ||
|
||
P1(int *x, int *z, int **y) | ||
{ | ||
rcu_assign_pointer(*y, z); | ||
synchronize_rcu(); | ||
WRITE_ONCE(*x, 0); | ||
} | ||
|
||
exists (0:r0=x /\ 0:r1=0) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
C RCU+sync+read | ||
|
||
(* | ||
* Result: Never | ||
* | ||
* This litmus test demonstrates that after a grace period, an RCU updater always | ||
* sees all stores done in prior RCU read-side critical sections. Such | ||
* read-side critical sections would have ended before the grace period ended. | ||
* | ||
* This is one implication of the RCU grace-period guarantee, which says (among | ||
* other things) that an RCU read-side critical section cannot span a grace period. | ||
*) | ||
|
||
{ | ||
int x = 0; | ||
int y = 0; | ||
} | ||
|
||
P0(int *x, int *y) | ||
{ | ||
rcu_read_lock(); | ||
WRITE_ONCE(*x, 1); | ||
WRITE_ONCE(*y, 1); | ||
rcu_read_unlock(); | ||
} | ||
|
||
P1(int *x, int *y) | ||
{ | ||
int r0; | ||
int r1; | ||
|
||
r0 = READ_ONCE(*x); | ||
synchronize_rcu(); | ||
r1 = READ_ONCE(*y); | ||
} | ||
|
||
exists (1:r0=1 /\ 1:r1=0) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.