tools/memory-model: Refactor some RCU relations
authorAlan Stern <stern@rowland.harvard.edu>
Thu, 15 Nov 2018 16:19:58 +0000 (11:19 -0500)
committerPaul E. McKenney <paulmck@linux.ibm.com>
Mon, 18 Mar 2019 17:27:52 +0000 (10:27 -0700)
commit284749b0aebbf3ab26ff92198545aea36165f6bf
tree0ed5262e2703aab997e81b5649bc1f7c78a2871e
parent0172d9e322035bf7bb66a7dfdd795c38d71dbba9
tools/memory-model: Refactor some RCU relations

In preparation for adding support for SRCU, refactor the definitions
of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po?
terms from the first two to the second two.  An rcu-gp relation is
added; it is equivalent to gp with the po and po? terms removed.

This is necessary because for SRCU, we will have to use the loc
relation to check that the terms at the start and end of each disjunct
in the definition of rcu-fence refer to the same srcu_struct
location.  If these terms are hidden behind po and po?, there's no way
to carry out this check.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Tested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
tools/memory-model/linux-kernel.cat