Commit 15aa25cb authored by Alan Stern's avatar Alan Stern Committed by Paul E. McKenney
Browse files

tools/memory-model: Change definition of rcu-fence 



The rcu-fence relation in the Linux Kernel Memory Model is not well
named.  It doesn't act like any other fence relation, in that it does
not relate events before a fence to events after that fence.  All it
does is relate certain RCU events to one another (those that are
ordered by the RCU Guarantee); this induces an actual
strong-fence-like relation linking events preceding the first RCU
event to those following the second.

This patch renames rcu-fence, now called rcu-order.  It adds a new
definition of rcu-fence, something which should have been present all
along because it is used in the rb relation.  And it modifies the
fence and strong-fence relations by making them incorporate the new
rcu-fence.

As a result of this change, there is no longer any need to define
full-fence in the section for detecting data races.  It can simply be
replaced by the updated strong-fence relation.

This change should have no effect on the operation of the memory model.

Signed-off-by: default avatarAlan Stern <stern@rowland.harvard.edu>
Acked-by: default avatarAndrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.ibm.com>
parent f9de4171

tools/memory-model/linux-kernel.cat

+13 −10
Original line number Diff line number Diff line
@@ -122,24 +122,28 @@ let rcu-link = po? ; hb* ; pb* ; prop ; po 


(*

 * Any sequence containing at least as many grace periods as RCU read-side

 * critical sections (joined by rcu-link) acts as a generalized strong fence.

 * critical sections (joined by rcu-link) induces order like a generalized

 * inter-CPU strong fence.

 * Likewise for SRCU grace periods and read-side critical sections, provided

 * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same

 * struct srcu_struct location.

 *)

let rec rcu-fence = rcu-gp | srcu-gp |

let rec rcu-order = rcu-gp | srcu-gp |

	(rcu-gp ; rcu-link ; rcu-rscsi) |

	((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |

	(rcu-rscsi ; rcu-link ; rcu-gp) |

	((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |

	(rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) |

	((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) |

	(rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) |

	((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) |

	(rcu-fence ; rcu-link ; rcu-fence)

	(rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) |

	((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) |

	(rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) |

	((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) |

	(rcu-order ; rcu-link ; rcu-order)

let rcu-fence = po ; rcu-order ; po?

let fence = fence | rcu-fence

let strong-fence = strong-fence | rcu-fence



(* rb orders instructions just as pb does *)

let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [Marked]

let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]



irreflexive rb as rcu
@@ -163,9 +167,8 @@ flag ~empty mixed-accesses as mixed-accesses 


(* Executes-before and visibility *)

let xbstar = (hb | pb | rb)*

let full-fence = strong-fence | (po ; rcu-fence ; po?)

let vis = cumul-fence* ; rfe? ; [Marked] ;

	((full-fence ; [Marked] ; xbstar) | (xbstar & int))

	((strong-fence ; [Marked] ; xbstar) | (xbstar & int))



(* Boundaries for lifetimes of plain accesses *)

let w-pre-bounded = [Marked] ; (addr | fence)?

CRA Git | Maintained and supported by SUSTech CRA and CCSE