Message-ID: <Y3O6mJz4wXJlzLh2@rowland.harvard.edu>
Date:   Tue, 15 Nov 2022 11:13:12 -0500
From:   Alan Stern <stern@...land.harvard.edu>
To:     Jonas Oberhauser <jonas.oberhauser@...wei.com>
Cc:     "Paul E. McKenney" <paulmck@...nel.org>,
        "parri.andrea@...il.com" <parri.andrea@...il.com>,
        "will@...nel.org" <will@...nel.org>,
        "peterz@...radead.org" <peterz@...radead.org>,
        "boqun.feng@...il.com" <boqun.feng@...il.com>,
        "npiggin@...il.com" <npiggin@...il.com>,
        "dhowells@...hat.com" <dhowells@...hat.com>,
        "j.alglave@....ac.uk" <j.alglave@....ac.uk>,
        "luc.maranget@...ia.fr" <luc.maranget@...ia.fr>,
        "akiyks@...il.com" <akiyks@...il.com>,
        "dlustig@...dia.com" <dlustig@...dia.com>,
        "joel@...lfernandes.org" <joel@...lfernandes.org>,
        "urezki@...il.com" <urezki@...il.com>,
        "quic_neeraju@...cinc.com" <quic_neeraju@...cinc.com>,
        "frederic@...nel.org" <frederic@...nel.org>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: [PATCH] tools: memory-model: Add rmw-sequences to the LKMM

On Tue, Nov 15, 2022 at 02:05:39PM +0000, Jonas Oberhauser wrote:
> 
> 
> 
> 	
> > -----Original Message-----
> > From: Alan Stern [mailto:stern@...land.harvard.edu] 
> > Sent: Monday, November 14, 2022 6:26 PM
> 
> Hi Alan,
> thanks for preparing this!
> 
> > Jonas has pointed out a weakness in the Linux Kernel Memory Model.
> > Namely, the memory ordering properties of atomic operations are not
> > monotonic: An atomic op with full-barrier semantics does not always provide ordering as strong as one with release-barrier semantics.
> 
> Note that I believe it was Viktor who originally pointed out this weakness to me
> in private communication. My contribution (besides chatting with you) is to
> check that the solution does indeed restore the monotonicity (not just on some
> litmus tests but in general).
> 
> So I would change the wording to "Viktor has pointed out a weakness in the Linux
> Kernel Memory Model."

People will wonder who Viktor is.  I don't have his full name or email 
address.  In fact, shouldn't he have been CC'ed during this entire 
discussion?

> > +let rmw-sequence = (rf ; rmw)*
> 
> I would perhaps suggest to only consider external read-from in rmw-sequences, as
> below:
> +let rmw-sequence = (rfe ; rmw)*

We discussed the matter earlier, and I don't recall any mention of this 
objection.

> The reason I (slightly) prefer this is that this is sufficient to imply
> monotonicity.
> Also there is some minor concern that the patch that results in the stricter
> model (i.e., rmw-sequence = (rf ; rmw)*) might be incorrect on some hypothetical
> future architecture in which RMWs can be merged in the store coalescing queue
> with earlier stores to the same location. This is exemplified in the following
> litmus test:
> 
> C atomics-not-monotonic-2
> 
> {}
> 
> P0(int *x, atomic_t *y)
> {
>     int r1;
> 	WRITE_ONCE(*x, 1);
> 	smp_store_release(y, 0);
> 	r1 = atomic_inc_return_relaxed(y);
> }
> 
> P1(atomic_t *y)
> {
> 	int r1;
> 
> 	r1 = atomic_inc_return(y);
> }
> 
> P2(int *x, atomic_t *y)
> {
> 	int r2;
> 	int r3;
> 
> 	r2 = atomic_read(y);
> 	smp_rmb();
> 	r3 = READ_ONCE(*x);
> }
> 
> exists (2:r2=2 /\ 2:r3=0)
> 
> Here such a hypothetical future architecture could merge the operations to *y by
> P0 into a single store, effectively turning the code of P0 into
> 
> P0(int *x, atomic_t *y)
> {
>     int r1;
> 	WRITE_ONCE(*x, 1);
> 	WRITE_ONCE(*y, 1);
> 	r1 = 0;
> }
> 
> The stricter patch would not be sound with this hypothetical architecture, while
> the more relaxed patch should be.
> 
> I don't think such a future architecture is likely since I don't expect there to
> be any practical performance impact. At the same time I also don't currently see
> any advantage of the stricter model.
> 
> For this reason I would slightly prefer the more relaxed model.

I don't see any point in worrying about hypothetical future 
architectures that might use a questionable design.

Also, given that this test is forbidden:

P0				P1		P2
-------------------------	--------------	----------------------------
WRITE_ONCE(*x, 1);		atomic_inc(y);	r1 = atomic_read_acquire(y);
atomic_set_release(y, 1);			r2 = READ_ONCE(*x);
exists (2:r1=2 /\ 2:r2=0)

shouldn't the following also be forbidden?

P0				P1		P2
-------------------------	--------------	----------------------------
WRITE_ONCE(*x, 1);		atomic_inc(y);	r1 = atomic_read_acquire(y);
atomic_set_release(y, 1);	atomic_inc(y);	r2 = READ_ONCE(*x);
exists (2:r1=3 /\ 2:r2=0)

> > +Rmw sequences have a special property in the LKMM: They can extend the 
> > +cumul-fence relation.  That is, if we have:
> > +
> > +	U ->cumul-fence X -> rmw-sequence Y
> > +
> > +then also U ->cumul-fence Y.  Thinking about this in terms of the 
> > +operational model, U ->cumul-fence X says that the store U propagates 
> > +to each CPU before the store X does.  Then the fact that X and Y are 
> > +linked by an rmw sequence means that U also propagates to each CPU 
> > +before Y does.
> > +
> 
> Here I would add that the rmw sequences also play a similar role in the
> w-post-bounded relation. For example as follows:
> 
> +Rmw sequences have a special property in the LKMM: They can extend the 
> +cumul-fence and w-post-bounded relations.  That is, if we have:
> +
> +	U ->cumul-fence X -> rmw-sequence Y
> +
> +then also U ->cumul-fence Y, and analogously if we have
> +
> +	U ->w-post-bounded X -> rmw-sequence Y
> +
> +then also U ->w-post-bounded Y. Thinking about this in terms of the 
> +operational model, U ->cumul-fence X says that the store U propagates 
> +to each CPU before the store X does.  Then the fact that X and Y are 
> +linked by an rmw sequence means that U also propagates to each CPU 
> +before Y does.
> +

I considered this and specifically decided against it, because the 
w-post-bounded relation has not yet been introduced at this point in the 
document.  It doesn't show up until much later.  (Also, there didn't 
seem to be any graceful way of mentioning this fact at the point where 
w-post-bounded does get introduced, and on the whole the matter didn't 
seem to be all that important.)

Instead of your suggested change, I suppose it would be okay to say, at 
the end of the paragraph:

	(In an analogous way, rmw sequences can extend the 
	w-post-bounded relation defined below in the PLAIN ACCESSES
	AND DATA RACES section.)

Or something like this could be added to the ODDS AND ENDS section at 
the end of the document.

Alan

Powered by blists - more mailing lists