From be4a37973cb078fc64d541f396b7d4d80e45fbe2 Mon Sep 17 00:00:00 2001 From: "Joel Fernandes (Google)" Date: Sun, 22 Mar 2020 21:57:33 -0400 Subject: Documentation: LKMM: Add litmus test for RCU GP guarantee where updater frees object This adds an example for the important RCU grace period guarantee, which shows an RCU reader can never span a grace period. Acked-by: Andrea Parri Signed-off-by: Joel Fernandes (Google) Signed-off-by: Paul E. McKenney --- .../litmus-tests/rcu/RCU+sync+free.litmus | 42 ++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 Documentation/litmus-tests/rcu/RCU+sync+free.litmus (limited to 'Documentation') diff --git a/Documentation/litmus-tests/rcu/RCU+sync+free.litmus b/Documentation/litmus-tests/rcu/RCU+sync+free.litmus new file mode 100644 index 000000000000..4ee67e12f513 --- /dev/null +++ b/Documentation/litmus-tests/rcu/RCU+sync+free.litmus @@ -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) -- cgit v1.3.1 From a591890c4e91f37ce858a3090b16e0eef2511575 Mon Sep 17 00:00:00 2001 From: "Joel Fernandes (Google)" Date: Sun, 22 Mar 2020 21:57:34 -0400 Subject: Documentation: LKMM: Add litmus test for RCU GP guarantee where reader stores This adds an example for the important RCU grace period guarantee, which shows an RCU reader can never span a grace period. Acked-by: Andrea Parri Signed-off-by: Joel Fernandes (Google) Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/README | 11 +++++++ .../litmus-tests/rcu/RCU+sync+read.litmus | 37 ++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 Documentation/litmus-tests/README create mode 100644 Documentation/litmus-tests/rcu/RCU+sync+read.litmus (limited to 'Documentation') diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README new file mode 100644 index 000000000000..c4307ea9f996 --- /dev/null +++ b/Documentation/litmus-tests/README @@ -0,0 +1,11 @@ +============ +LITMUS TESTS +============ + +RCU (/rcu directory) +-------------------- + +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. diff --git a/Documentation/litmus-tests/rcu/RCU+sync+read.litmus b/Documentation/litmus-tests/rcu/RCU+sync+read.litmus new file mode 100644 index 000000000000..f34176720231 --- /dev/null +++ b/Documentation/litmus-tests/rcu/RCU+sync+read.litmus @@ -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) -- cgit v1.3.1 From efff6150209694a78c8af8c2a7557af682086220 Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Thu, 26 Mar 2020 10:40:20 +0800 Subject: Documentation/litmus-tests: Introduce atomic directory Although we have atomic_t.txt and its friends to describe the semantics of atomic APIs and lib/atomic64_test.c for build testing and testing in UP mode, the tests for our atomic APIs in real SMP mode are still missing. Since now we have the LKMM tool in kernel and litmus tests can be used to generate kernel modules for testing purpose with "klitmus" (a tool from the LKMM toolset), it makes sense to put a few typical litmus tests into kernel so that 1) they are the examples to describe the conceptual mode of the semantics of atomic APIs, and 2) they can be used to generate kernel test modules for anyone who is interested to test the atomic APIs implementation (in most cases, is the one who implements the APIs for a new arch) Therefore, introduce the atomic directory for this purpose. The directory is maintained by the LKMM group to make sure the litmus tests are always aligned with our memory model. Acked-by: Alan Stern Acked-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Signed-off-by: Boqun Feng Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/atomic/README | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 Documentation/litmus-tests/atomic/README (limited to 'Documentation') diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README new file mode 100644 index 000000000000..ae61201a4271 --- /dev/null +++ b/Documentation/litmus-tests/atomic/README @@ -0,0 +1,4 @@ +This directory contains litmus tests that are typical to describe the semantics +of our atomic 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. -- cgit v1.3.1 From 4dcd4d36ddb1fa7fa7257ffe9e711608119b9785 Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Thu, 26 Mar 2020 10:40:21 +0800 Subject: Documentation/litmus-tests/atomic: Add a test for atomic_set() We already use a litmus test in atomic_t.txt to describe the behavior of an atomic_set() with the an atomic RMW, so add it into atomic-tests directory to make it easily accessible for anyone who cares about the semantics of our atomic APIs. Besides currently the litmus test "atomic-set" in atomic_t.txt has a few things to be improved: 1) The CPU/Processor numbers "P1,P2" are not only inconsistent with the rest of the document, which uses "CPU0" and "CPU1", but also unacceptable by the herd tool, which requires processors start at "P0". 2) The initialization block uses a "atomic_set()", which is OK, but it's better to use ATOMIC_INIT() to make clear this is an initialization. 3) The return value of atomic_add_unless() is discarded inexplicitly, which is OK for C language, but it will be helpful to the herd tool if we use a void cast to make the discard explicit. 4) The name and the paragraph describing the test need to be more accurate and aligned with our wording in LKMM. Therefore fix these in both atomic_t.txt and the new added litmus test. Acked-by: Andrea Parri Acked-by: Alan Stern Signed-off-by: Boqun Feng Reviewed-by: Joel Fernandes (Google) Signed-off-by: Paul E. McKenney --- Documentation/atomic_t.txt | 14 ++++++------- ...Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus | 24 ++++++++++++++++++++++ Documentation/litmus-tests/atomic/README | 7 +++++++ 3 files changed, 38 insertions(+), 7 deletions(-) create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus (limited to 'Documentation') diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt index 0ab747e0d5ac..67d1d99f8589 100644 --- a/Documentation/atomic_t.txt +++ b/Documentation/atomic_t.txt @@ -85,21 +85,21 @@ smp_store_release() respectively. Therefore, if you find yourself only using the Non-RMW operations of atomic_t, you do not in fact need atomic_t at all and are doing it wrong. -A subtle detail of atomic_set{}() is that it should be observable to the RMW -ops. That is: +A note for the implementation of atomic_set{}() is that it must not break the +atomicity of the RMW ops. That is: - C atomic-set + C Atomic-RMW-ops-are-atomic-WRT-atomic_set { - atomic_set(v, 1); + atomic_t v = ATOMIC_INIT(1); } - P1(atomic_t *v) + P0(atomic_t *v) { - atomic_add_unless(v, 1, 0); + (void)atomic_add_unless(v, 1, 0); } - P2(atomic_t *v) + P1(atomic_t *v) { atomic_set(v, 0); } diff --git a/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus new file mode 100644 index 000000000000..49385314d911 --- /dev/null +++ b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus @@ -0,0 +1,24 @@ +C Atomic-RMW-ops-are-atomic-WRT-atomic_set + +(* + * Result: Never + * + * Test that atomic_set() cannot break the atomicity of atomic RMWs. + *) + +{ + 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) diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README index ae61201a4271..a1b72410b539 100644 --- a/Documentation/litmus-tests/atomic/README +++ b/Documentation/litmus-tests/atomic/README @@ -2,3 +2,10 @@ This directory contains litmus tests that are typical to describe the semantics of our atomic 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. + +============ +LITMUS TESTS +============ + +Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus + Test that atomic_set() cannot break the atomicity of atomic RMWs. -- cgit v1.3.1 From e30d02355536e9678ab8a4dfcd6e90a86479b10f Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Thu, 26 Mar 2020 10:40:22 +0800 Subject: Documentation/litmus-tests/atomic: Add a test for smp_mb__after_atomic() We already use a litmus test in atomic_t.txt to describe atomic RMW + smp_mb__after_atomic() is stronger than acquire (both the read and the write parts are ordered). So make it a litmus test in atomic-tests directory, so that people can access the litmus easily. Additionally, change the processor numbers "P1, P2" to "P0, P1" in atomic_t.txt for the consistency with the processor numbers in the litmus test, which herd can handle. Acked-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Boqun Feng Reviewed-by: Joel Fernandes (Google) Signed-off-by: Paul E. McKenney --- Documentation/atomic_t.txt | 10 +++---- ...b__after_atomic-is-stronger-than-acquire.litmus | 32 ++++++++++++++++++++++ Documentation/litmus-tests/atomic/README | 5 ++++ 3 files changed, 42 insertions(+), 5 deletions(-) create mode 100644 Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus (limited to 'Documentation') diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt index 67d1d99f8589..0f1fdedf36bb 100644 --- a/Documentation/atomic_t.txt +++ b/Documentation/atomic_t.txt @@ -233,19 +233,19 @@ as well. Similarly, something like: is an ACQUIRE pattern (though very much not typical), but again the barrier is strictly stronger than ACQUIRE. As illustrated: - C strong-acquire + C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire { } - P1(int *x, atomic_t *y) + P0(int *x, atomic_t *y) { r0 = READ_ONCE(*x); smp_rmb(); r1 = atomic_read(y); } - P2(int *x, atomic_t *y) + P1(int *x, atomic_t *y) { atomic_inc(y); smp_mb__after_atomic(); @@ -253,14 +253,14 @@ strictly stronger than ACQUIRE. As illustrated: } exists - (r0=1 /\ r1=0) + (0:r0=1 /\ 0:r1=0) This should not happen; but a hypothetical atomic_inc_acquire() -- (void)atomic_fetch_inc_acquire() for instance -- would allow the outcome, because it would not order the W part of the RMW against the following WRITE_ONCE. Thus: - P1 P2 + P0 P1 t = LL.acq *y (0) t++; diff --git a/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus b/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus new file mode 100644 index 000000000000..9a8e31a44b28 --- /dev/null +++ b/Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus @@ -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) diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README index a1b72410b539..714cf93816ea 100644 --- a/Documentation/litmus-tests/atomic/README +++ b/Documentation/litmus-tests/atomic/README @@ -7,5 +7,10 @@ tools/memory-model/README. LITMUS TESTS ============ +Atomic-RMW+mb__after_atomic-is-stronger-than-acquire + 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. -- cgit v1.3.1 From cdaac9d6d23d7a7f9edbb568191d05f2b660fff0 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Sun, 10 May 2020 15:12:57 +0900 Subject: Documentation/litmus-tests: Merge atomic's README into top-level one Where Documentation/litmus-tests/README lists RCU litmus tests, Documentation/litmus-tests/atomic/README lists atomic litmus tests. For symmetry, merge the latter into former, with some context adjustment in the introduction. Acked-by: Andrea Parri Acked-by: Joel Fernandes (Google) Acked-by: Boqun Feng Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/README | 19 +++++++++++++++++++ Documentation/litmus-tests/atomic/README | 16 ---------------- 2 files changed, 19 insertions(+), 16 deletions(-) delete mode 100644 Documentation/litmus-tests/atomic/README (limited to 'Documentation') diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README index c4307ea9f996..ac0b270b456c 100644 --- a/Documentation/litmus-tests/README +++ b/Documentation/litmus-tests/README @@ -2,6 +2,25 @@ 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. + + RCU (/rcu directory) -------------------- diff --git a/Documentation/litmus-tests/atomic/README b/Documentation/litmus-tests/atomic/README deleted file mode 100644 index 714cf93816ea..000000000000 --- a/Documentation/litmus-tests/atomic/README +++ /dev/null @@ -1,16 +0,0 @@ -This directory contains litmus tests that are typical to describe the semantics -of our atomic 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. - -============ -LITMUS TESTS -============ - -Atomic-RMW+mb__after_atomic-is-stronger-than-acquire - 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. -- cgit v1.3.1 From c425fb5f8d2c8d22e7baad6dc077703c2b329d2d Mon Sep 17 00:00:00 2001 From: "Joel Fernandes (Google)" Date: Mon, 11 May 2020 22:06:46 -0400 Subject: Documentation/litmus-tests: Cite an RCU litmus test This commit cites a pertinent RCU-related litmus test. Co-developed-by: Joel Fernandes (Google) Co-developed-by: Akira Yokosawa [Alan: grammar nit] [ paulmck: Update commit log and title per Akira feedback. ] Suggested-by: Alan Stern Signed-off-by: Joel Fernandes (Google) Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/README | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Documentation') diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README index ac0b270b456c..b79e640214b9 100644 --- a/Documentation/litmus-tests/README +++ b/Documentation/litmus-tests/README @@ -24,6 +24,10 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus 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 -- cgit v1.3.1 From 5ef0a07a7928539d46fdb163acfad28c6d877a89 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Wed, 24 Jun 2020 06:59:26 +0900 Subject: Documentation/litmus-tests: Add note on herd7 7.56 in atomic litmus test herdtools 7.56 has enhanced herd7's C parser so that the "(void)expr" construct in Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus is accepted. This is independent of LKMM's cat model, so mention the required version in the header of the litmus test and its entry in README. CC: Boqun Feng Reported-by: Andrea Parri Acked-by: Andrea Parri Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/README | 1 + .../litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus | 1 + 2 files changed, 2 insertions(+) (limited to 'Documentation') diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README index b79e640214b9..7f5c6c3ed6c3 100644 --- a/Documentation/litmus-tests/README +++ b/Documentation/litmus-tests/README @@ -19,6 +19,7 @@ Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus 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) diff --git a/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus index 49385314d911..ffd4d3e79c4a 100644 --- a/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus +++ b/Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus @@ -4,6 +4,7 @@ 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". *) { -- cgit v1.3.1