iv/linux
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

tools/memory-model: Update README for addition of SRCU

Browse Source 
This commit updates the section on LKMM limitations to no longer say
that SRCU is not modeled, but instead describe how LKMM's modeling of
SRCU departs from the Linux-kernel implementation.

TL;DR:  There is no known valid use case that cares about the Linux
kernel's ability to have partially overlapping SRCU read-side critical
sections.

Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
This commit is contained in:
Paul E. McKenney 2018-11-26 14:26:43 -08:00
parent a3f600d92d
commit ad9fd20b6d
1 changed files with 23 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
tools/memory-model/README
View File

@ -221,8 +221,29 @@ The Linux-kernel memory model has the following limitations:
additional call_rcu() process to the site of the additional call_rcu() process to the site of the
emulated rcu-barrier(). emulated rcu-barrier().
e. Sleepable RCU (SRCU) is not modeled. It can be e. Although sleepable RCU (SRCU) is now modeled, there
emulated, but perhaps not simply. are some subtle differences between its semantics and
those in the Linux kernel. For example, the kernel
might interpret the following sequence as two partially
overlapping SRCU read-side critical sections:
1 r1 = srcu_read_lock(&my_srcu);
2 do_something_1();
3 r2 = srcu_read_lock(&my_srcu);
4 do_something_2();
5 srcu_read_unlock(&my_srcu, r1);
6 do_something_3();
7 srcu_read_unlock(&my_srcu, r2);
In contrast, LKMM will interpret this as a nested pair of
SRCU read-side critical sections, with the outer critical
section spanning lines 1-7 and the inner critical section
spanning lines 3-5.
This difference would be more of a concern had anyone
identified a reasonable use case for partially overlapping
SRCU read-side critical sections. For more information,
please see: https://paulmck.livejournal.com/40593.html
f. Reader-writer locking is not modeled. It can be f. Reader-writer locking is not modeled. It can be
emulated in litmus tests using atomic read-modify-write emulated in litmus tests using atomic read-modify-write