On Wed, Jan 25, 2023 at 10:34:40AM -0500, Alan Stern wrote:
On Wed, Jan 25, 2023 at 07:05:20AM -0800, Paul E. McKenney wrote:I am not sure whether or not we are talking about the same thing,
On Wed, Jan 25, 2023 at 02:10:08PM +0100, Jonas Oberhauser wrote:Are we all talking about the same thing? There were two different
In the RCU case, it is because it is far easier to provide this guarantee,
On 1/25/2023 3:20 AM, Paul E. McKenney wrote:
On Tue, Jan 24, 2023 at 08:54:56PM -0500, Alan Stern wrote:FWIW, I currently don't see a need for either RCU nor "base" LKMM to have
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
Within the Linux kernel, the rule for a given RCU "domain" is that ifThe LKMM says pretty much the same thing. In fact, it says the event
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
this kind of guarantee.
even though it is based on hardware and compilers rather than LKMM,
than it would be to explain to some random person why the access that
is intuitively clearly after the grace period can somehow come before it.
But I'm curious for why it doesn't exist in LKMM -- is it because of AlphaBecause to the best of my knowledge, no one has ever come up with a
or some other issues that make it hard to guarantee (like a compiler merging
two threads and optimizing or something?), or is it simply that it seemed
like a complicated guarantee with no discernible upside, or something else?
use for 2+2W and friends that isn't better handled by some much more
straightforward pattern of accesses. So we did not guarantee it in LKMM.
Yes, you could argue that my "ease of explanation" paragraph above is
a valid use case, but I am not sure that this is all that compelling of
an argument. ;-)
guarantees mentioned above:
The RCU guarantee about writes in a read-side critical section
becoming visible to all CPUs before a later grace period ends;
The guarantee about the 2+2W pattern and friends being
forbidden.
The LKMM includes the first of these but not the second (for the reason
Paul stated).
but given this litmus test:
------------------------------------------------------------------------
C C-srcu-observed-4
(*
* Result: Sometimes
*
* The Linux-kernel implementation is suspected to forbid this.
*)
{}
P0(int *x, int *y, int *z, struct srcu_struct *s)
{
int r1;
r1 = srcu_read_lock(s);
WRITE_ONCE(*y, 2);
WRITE_ONCE(*x, 1);
srcu_read_unlock(s, r1);
}
P1(int *x, int *y, int *z, struct srcu_struct *s)
{
int r1;
WRITE_ONCE(*y, 1);
synchronize_srcu(s);
WRITE_ONCE(*z, 2);
}
P2(int *x, int *y, int *z, struct srcu_struct *s)
{
WRITE_ONCE(*z, 1);
smp_store_release(x, 2);
}
exists (x=1 /\ y=1 /\ z=1)
------------------------------------------------------------------------
We get the following from herd7:
------------------------------------------------------------------------
$ herd7 -conf linux-kernel.cfg C-srcu-observed-4.litmus
Test C-srcu-observed-4 Allowed
States 8
x=1; y=1; z=1;
x=1; y=1; z=2;
x=1; y=2; z=1;
x=1; y=2; z=2;
x=2; y=1; z=1;
x=2; y=1; z=2;
x=2; y=2; z=1;
x=2; y=2; z=2;
Ok
Witnesses
Positive: 1 Negative: 7
Condition exists (x=1 /\ y=1 /\ z=1)
Observation C-srcu-observed-4 Sometimes 1 7
Time C-srcu-observed-4 0.02
Hash=8b6020369b73ac19070864a9db00bbf8
------------------------------------------------------------------------
This does not seem to me to be consistent with your "The RCU guarantee
about writes in a read-side critical section becoming visible to all
CPUs before a later grace period ends".
Again, I am OK with LKMM allowing C-srcu-observed-4.litmus, as long as
the actual Linux-kernel implementation forbids it.