lkml.org 
[lkml]   [2022]   [Nov]   [14]   [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 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 <jonas.oberhauser@huawei.com>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>

Reviewed-by: Boqun Feng <boqun.feng@gmail.com>

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

\
 
 \ /
  Last update: 2022-11-14 21:56    [W:0.065 / U:0.276 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site