diff options
author | Joel Fernandes (Google) <joel@joelfernandes.org> | 2020-03-23 04:57:33 +0300 |
---|---|---|
committer | Paul E. McKenney <paulmck@kernel.org> | 2020-06-29 22:05:17 +0300 |
commit | be4a37973cb078fc64d541f396b7d4d80e45fbe2 (patch) | |
tree | 7a52b04df502a82a61e23acb10b03cd64029541b /Documentation | |
parent | c1b14609013a6b4c4b2d73583bde645540ebd9b7 (diff) | |
download | linux-be4a37973cb078fc64d541f396b7d4d80e45fbe2.tar.xz |
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 <parri.andrea@gmail.com>
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'Documentation')
-rw-r--r-- | Documentation/litmus-tests/rcu/RCU+sync+free.litmus | 42 |
1 files changed, 42 insertions, 0 deletions
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) |