lkml.org 
[lkml]   [2022]   [Nov]   [15]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH] tools: memory-model: Add rmw-sequences to the LKMM
On Tue, Nov 15, 2022 at 11:13:12AM -0500, Alan Stern wrote:
> On Tue, Nov 15, 2022 at 02:05:39PM +0000, Jonas Oberhauser wrote:
> >
> >
> >
> >
> > > -----Original Message-----
> > > From: Alan Stern [mailto:stern@rowland.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?

Viktor Vafeiadis <viktor@mpi-sws.org>

But I defer to Jonas on CCing, just in case Viktor needs to be provided
context on this discussion.

Thanx, Paul

> > > +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

\
 
 \ /
  Last update: 2022-11-16 05:59    [W:0.061 / U:1.040 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site