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.
The following litmus test illustrates the problem:
--------------------------------------------------
C atomics-not-monotonic
{}
P0(int *x, atomic_t *y)
{
WRITE_ONCE(*x, 1);
smp_wmb();
atomic_set(y, 1);
}
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)
--------------------------------------------------
The litmus test is allowed as shown with atomic_inc_return(), which
has full-barrier semantics. But if the operation is changed to
atomic_inc_return_release(), which only has release-barrier semantics,
the litmus test is forbidden. Clearly this violates monotonicity.
The reason is because the LKMM treats full-barrier atomic ops as if
they were written:
mb();
load();
store();
mb();
(where the load() and store() are the two parts of an atomic RMW op),
whereas it treats release-barrier atomic ops as if they were written:
load();
release_barrier();
store();
The difference is that here the release barrier orders the load part
of the atomic op before the store part with A-cumulativity, whereas
the mb()'s above do not. This means that release-barrier atomics can
effectively extend the cumul-fence relation but full-barrier atomics
cannot.
To resolve this problem we introduce the rmw-sequence relation,
representing an arbitrarily long sequence of atomic RMW operations in
which each operation reads from the previous one, and explicitly allow
it to extend cumul-fence. This modification of the memory model is
sound; it holds for PPC because of B-cumulativity, it holds for TSO
and ARM64 because of other-multicopy atomicity, and we can assume that
atomic ops on all other architectures will be implemented so as to
make it hold for them.
For similar reasons we also allow rmw-sequence to extend the
w-post-bounded relation, which is analogous to cumul-fence in some
ways.
Suggested-by: Jonas Oberhauser <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
---
tools/memory-model/Documentation/explanation.txt | 28 +++++++++++++++++++++++
tools/memory-model/linux-kernel.cat | 5 ++--
2 files changed, 31 insertions(+), 2 deletions(-)
Index: usb-devel/tools/memory-model/linux-kernel.cat
===================================================================
--- usb-devel.orig/tools/memory-model/linux-kernel.cat
+++ usb-devel/tools/memory-model/linux-kernel.cat
@@ -74,8 +74,9 @@ let ppo = to-r | to-w | fence | (po-unlo
(* Propagation: Ordering from release operations and strong fences. *)
let A-cumul(r) = (rfe ; [Marked])? ; r
+let rmw-sequence = (rf ; rmw)*
let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
- po-unlock-lock-po) ; [Marked]
+ po-unlock-lock-po) ; [Marked] ; rmw-sequence
let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
[Marked] ; rfe? ; [Marked]
@@ -174,7 +175,7 @@ let vis = cumul-fence* ; rfe? ; [Marked]
let w-pre-bounded = [Marked] ; (addr | fence)?
let r-pre-bounded = [Marked] ; (addr | nonrw-fence |
([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))?
-let w-post-bounded = fence? ; [Marked]
+let w-post-bounded = fence? ; [Marked] ; rmw-sequence
let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
[Marked]
Index: usb-devel/tools/memory-model/Documentation/explanation.txt
===================================================================
--- usb-devel.orig/tools/memory-model/Documentation/explanation.txt
+++ usb-devel/tools/memory-model/Documentation/explanation.txt
@@ -1006,6 +1006,34 @@ order. Equivalently,
where the rmw relation links the read and write events making up each
atomic update. This is what the LKMM's "atomic" axiom says.
+Atomic rmw updates play one more role in the LKMM: They can form "rmw
+sequences". An rmw sequence is simply a bunch of atomic updates where
+each update reads from the previous one. Written using events, it
+looks like this:
+
+ Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn,
+
+where Z0 is some store event and n can be any number (even 0, in the
+degenerate case). We write this relation as: Z0 ->rmw-sequence Zn.
+Note that this implies Z0 and Zn are stores to the same variable.
+
+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.
+
+(The notion of rmw sequences in the LKMM is similar to, but not quite
+the same as, that of release sequences in the C11 memory model. They
+were added to the LKMM to fix an obscure bug; without them, atomic
+updates with full-barrier semantics did not always guarantee ordering
+at least as strong as atomic updates with release-barrier semantics.)
+
THE PRESERVED PROGRAM ORDER RELATION: ppo
-----------------------------------------
On Mon, Nov 14, 2022 at 12:26:23PM -0500, Alan Stern wrote:
> 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.
>
> The following litmus test illustrates the problem:
>
> --------------------------------------------------
> C atomics-not-monotonic
>
> {}
>
> P0(int *x, atomic_t *y)
> {
> WRITE_ONCE(*x, 1);
> smp_wmb();
> atomic_set(y, 1);
> }
>
> 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)
> --------------------------------------------------
>
> The litmus test is allowed as shown with atomic_inc_return(), which
> has full-barrier semantics. But if the operation is changed to
> atomic_inc_return_release(), which only has release-barrier semantics,
> the litmus test is forbidden. Clearly this violates monotonicity.
>
> The reason is because the LKMM treats full-barrier atomic ops as if
> they were written:
>
> mb();
> load();
> store();
> mb();
>
> (where the load() and store() are the two parts of an atomic RMW op),
> whereas it treats release-barrier atomic ops as if they were written:
>
> load();
> release_barrier();
> store();
>
> The difference is that here the release barrier orders the load part
> of the atomic op before the store part with A-cumulativity, whereas
> the mb()'s above do not. This means that release-barrier atomics can
> effectively extend the cumul-fence relation but full-barrier atomics
> cannot.
>
> To resolve this problem we introduce the rmw-sequence relation,
> representing an arbitrarily long sequence of atomic RMW operations in
> which each operation reads from the previous one, and explicitly allow
> it to extend cumul-fence. This modification of the memory model is
> sound; it holds for PPC because of B-cumulativity, it holds for TSO
> and ARM64 because of other-multicopy atomicity, and we can assume that
> atomic ops on all other architectures will be implemented so as to
> make it hold for them.
>
> For similar reasons we also allow rmw-sequence to extend the
> w-post-bounded relation, which is analogous to cumul-fence in some
> ways.
>
> Suggested-by: Jonas Oberhauser <[email protected]>
> Signed-off-by: Alan Stern <[email protected]>
>
Reviewed-by: Boqun Feng <[email protected]>
Thanks!
Regards,
Boqun
> ---
>
> tools/memory-model/Documentation/explanation.txt | 28 +++++++++++++++++++++++
> tools/memory-model/linux-kernel.cat | 5 ++--
> 2 files changed, 31 insertions(+), 2 deletions(-)
>
> Index: usb-devel/tools/memory-model/linux-kernel.cat
> ===================================================================
> --- usb-devel.orig/tools/memory-model/linux-kernel.cat
> +++ usb-devel/tools/memory-model/linux-kernel.cat
> @@ -74,8 +74,9 @@ let ppo = to-r | to-w | fence | (po-unlo
>
> (* Propagation: Ordering from release operations and strong fences. *)
> let A-cumul(r) = (rfe ; [Marked])? ; r
> +let rmw-sequence = (rf ; rmw)*
> let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
> - po-unlock-lock-po) ; [Marked]
> + po-unlock-lock-po) ; [Marked] ; rmw-sequence
> let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
> [Marked] ; rfe? ; [Marked]
>
> @@ -174,7 +175,7 @@ let vis = cumul-fence* ; rfe? ; [Marked]
> let w-pre-bounded = [Marked] ; (addr | fence)?
> let r-pre-bounded = [Marked] ; (addr | nonrw-fence |
> ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))?
> -let w-post-bounded = fence? ; [Marked]
> +let w-post-bounded = fence? ; [Marked] ; rmw-sequence
> let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
> [Marked]
>
> Index: usb-devel/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-devel/tools/memory-model/Documentation/explanation.txt
> @@ -1006,6 +1006,34 @@ order. Equivalently,
> where the rmw relation links the read and write events making up each
> atomic update. This is what the LKMM's "atomic" axiom says.
>
> +Atomic rmw updates play one more role in the LKMM: They can form "rmw
> +sequences". An rmw sequence is simply a bunch of atomic updates where
> +each update reads from the previous one. Written using events, it
> +looks like this:
> +
> + Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn,
> +
> +where Z0 is some store event and n can be any number (even 0, in the
> +degenerate case). We write this relation as: Z0 ->rmw-sequence Zn.
> +Note that this implies Z0 and Zn are stores to the same variable.
> +
> +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.
> +
> +(The notion of rmw sequences in the LKMM is similar to, but not quite
> +the same as, that of release sequences in the C11 memory model. They
> +were added to the LKMM to fix an obscure bug; without them, atomic
> +updates with full-barrier semantics did not always guarantee ordering
> +at least as strong as atomic updates with release-barrier semantics.)
> +
>
> THE PRESERVED PROGRAM ORDER RELATION: ppo
> -----------------------------------------
>
On Tue, Nov 15, 2022 at 02:05:39PM +0000, Jonas Oberhauser wrote:
>
>
>
>
> > -----Original Message-----
> > From: Alan Stern [mailto:[email protected]]
> > 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
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:[email protected]]
> > > 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 <[email protected]>
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