On Tue, Jan 24, 2023 at 08:54:56PM -0500, Alan Stern wrote:
On Tue, Jan 24, 2023 at 02:54:49PM -0800, Paul E. McKenney wrote:Sounds good, and let's proceed on that assumption then. We can always
On Tue, Jan 24, 2023 at 05:35:33PM -0500, Alan Stern wrote:The LKMM says pretty much the same thing. In fact, it says the event
Can you be more explicit? Exactly what guarantees does the kernelI doubt that I will be able to articulate it very well, but here goes.
implementation make that can't be expressed in LKMM?
Within the Linux kernel, the rule for a given RCU "domain" is that if
an event follows a grace period in pretty much any sense of the word,
then that event sees the effects of all events in all read-side critical
sections that began prior to the start of that grace period.
Here the senses of the word "follow" include combinations of rf, fr,
and co, combined with the various acyclic and irreflexive relations
defined in LKMM.
sees the effects of all events po-before the unlock of (not just inside)
any read-side critical section that began prior to the start of the
grace period.
Judging from your description, I don't think we have anything to worryAnd are these anything the memory model needs to worry about?Given that several people, yourself included, are starting to use LKMM
to analyze the Linux-kernel RCU implementations, maybe it does.
Me, I am happy either way.
about.
revisit later if need be.
Thanx, Paul