lkml.org 
[lkml]   [2023]   [Jan]   [17]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH] tools/memory-model: Make ppo a subrelation of po
On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:
> As stated in the documentation and implied by its name, the ppo
> (preserved program order) relation is intended to link po-earlier
> to po-later instructions under certain conditions. However, a
> corner case currently allows instructions to be linked by ppo that
> are not executed by the same thread, i.e., instructions are being
> linked that have no po relation.
>
> This happens due to the mb/strong-fence relations, which (as one
> case) provide order when locks are passed between threads followed
> by an smp_mb__after_unlock_lock() fence. This is illustrated in
> the following litmus test (as can be seen when using herd7 with
> `doshow ppo`):
>
> P0(int *x, int *y)
> {
> spin_lock(x);
> spin_unlock(x);
> }
>
> P1(int *x, int *y)
> {
> spin_lock(x);
> smp_mb__after_unlock_lock();
> *y = 1;
> }
>
> The ppo relation will link P0's spin_lock(x) and P1's *y=1,
> because P0 passes a lock to P1 which then uses this fence.
>
> The patch makes ppo a subrelation of po by eliminating this
> possibility from mb and strong-fence, and instead introduces the
> notion of strong ordering operations, which are allowed to link
> events of distinct threads.
>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> ---
> .../Documentation/explanation.txt | 101 +++++++++++-------
> tools/memory-model/linux-kernel.cat | 20 ++--

I've reviewed the cat change part, and it looks good to me. Now going to
catch up with the interesting discussion on rcu-order...

One more thing, do we want something in the cat file to describe our
"internal axioms" as follow?

(* Model internal invariants *)
(* ppo is the subset of po *)
flag ~empty (ppo \ po) as INTERNAL-ERROR-PPO

Maybe it's helpful for people working on other tools to understand LKMM
cat file?

Anyway, with or without it:

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

Regards,
Boqun

> 2 files changed, 76 insertions(+), 45 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index e901b47236c3..4f5f6ac098de 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -865,14 +865,44 @@ propagates stores. When a fence instruction is executed on CPU C:
> propagate to all other CPUs before any instructions po-after
> the strong fence are executed on C.
>
> -The propagation ordering enforced by release fences and strong fences
> -affects stores from other CPUs that propagate to CPU C before the
> -fence is executed, as well as stores that are executed on C before the
> -fence. We describe this property by saying that release fences and
> -strong fences are A-cumulative. By contrast, smp_wmb() fences are not
> -A-cumulative; they only affect the propagation of stores that are
> -executed on C before the fence (i.e., those which precede the fence in
> -program order).
> + Whenever any CPU C' executes an unlock operation U such that
> + CPU C executes a lock operation L followed by a po-later
> + smp_mb__after_unlock_lock() fence, and L is either a later lock
> + operation on the lock released by U or is po-after U, then any
> + store that propagates to C' before U must propagate to all other
> + CPUs before any instructions po-after the fence are executed on C.
> +
> +While smp_wmb() and release fences only force certain earlier stores
> +to propagate to another CPU C' before certain later stores propagate
> +to the same CPU C', strong fences and smp_mb__after_unlock_lock()
> +force those stores to propagate to all other CPUs before any later
> +instruction is executed. We collectively refer to the latter
> +operations as strong ordering operations, as they provide much
> +stronger ordering in two ways:
> +
> + Firstly, strong ordering operations also create order between
> + earlier stores and later reads.
> +
> + Secondly, strong ordering operations create a form of global
> + ordering: When an earlier store W propagates to CPU C and is
> + ordered by a strong ordering operation with a store W' of C,
> + and another CPU C' observes W' and in response issues yet
> + another store W'', then W'' also can not propagate to any CPU
> + before W. By contrast, a release fence or smp_wmb() would only
> + order W and W', but not force any ordering between W and W''.
> + To summarize, the ordering forced by strong ordering operations
> + extends to later stores of all CPUs, while other fences only
> + force ordering with relation to stores on the CPU that executes
> + the fence.
> +
> +The propagation ordering enforced by release fences and strong ordering
> +operations affects stores from other CPUs that propagate to CPU C before
> +the fence is executed, as well as stores that are executed on C before
> +the fence. We describe this property by saying that release fences and
> +strong ordering operations are A-cumulative. By contrast, smp_wmb()
> +fences are not A-cumulative; they only affect the propagation of stores
> +that are executed on C before the fence (i.e., those which precede the
> +fence in program order).
>
> rcu_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> other properties which we discuss later.
> @@ -1425,36 +1455,36 @@ requirement is the content of the LKMM's "happens-before" axiom.
>
> The LKMM defines yet another relation connected to times of
> instruction execution, but it is not included in hb. It relies on the
> -particular properties of strong fences, which we cover in the next
> -section.
> +particular properties of strong ordering operations, which we cover in the
> +next section.
>
>
> THE PROPAGATES-BEFORE RELATION: pb
> ----------------------------------
>
> The propagates-before (pb) relation capitalizes on the special
> -features of strong fences. It links two events E and F whenever some
> -store is coherence-later than E and propagates to every CPU and to RAM
> -before F executes. The formal definition requires that E be linked to
> -F via a coe or fre link, an arbitrary number of cumul-fences, an
> -optional rfe link, a strong fence, and an arbitrary number of hb
> -links. Let's see how this definition works out.
> +features of strong ordering operations. It links two events E and F
> +whenever some store is coherence-later than E and propagates to every
> +CPU and to RAM before F executes. The formal definition requires that
> +E be linked to F via a coe or fre link, an arbitrary number of
> +cumul-fences, an optional rfe link, a strong ordering operation, and an
> +arbitrary number of hb links. Let's see how this definition works out.
>
> Consider first the case where E is a store (implying that the sequence
> of links begins with coe). Then there are events W, X, Y, and Z such
> that:
>
> - E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F,
> + E ->coe W ->cumul-fence* X ->rfe? Y ->strong-order Z ->hb* F,
>
> where the * suffix indicates an arbitrary number of links of the
> specified type, and the ? suffix indicates the link is optional (Y may
> be equal to X). Because of the cumul-fence links, we know that W will
> propagate to Y's CPU before X does, hence before Y executes and hence
> -before the strong fence executes. Because this fence is strong, we
> -know that W will propagate to every CPU and to RAM before Z executes.
> -And because of the hb links, we know that Z will execute before F.
> -Thus W, which comes later than E in the coherence order, will
> -propagate to every CPU and to RAM before F executes.
> +before the strong ordering operation executes. Because of the strong
> +ordering, we know that W will propagate to every CPU and to RAM before
> +Z executes. And because of the hb links, we know that Z will execute
> +before F. Thus W, which comes later than E in the coherence order,
> +will propagate to every CPU and to RAM before F executes.
>
> The case where E is a load is exactly the same, except that the first
> link in the sequence is fre instead of coe.
> @@ -1637,8 +1667,8 @@ does not imply X ->rcu-order V, because the sequence contains only
> one rcu-gp link but two rcu-rscsi links.
>
> The rcu-order relation is important because the Grace Period Guarantee
> -means that rcu-order links act kind of like strong fences. In
> -particular, E ->rcu-order F implies not only that E begins before F
> +means that rcu-order links act kind of like a strong ordering operation.
> +In particular, E ->rcu-order F implies not only that E begins before F
> ends, but also that any write po-before E will propagate to every CPU
> before any instruction po-after F can execute. (However, it does not
> imply that E must execute before F; in fact, each synchronize_rcu()
> @@ -1675,24 +1705,23 @@ The rcu-fence relation is a simple extension of rcu-order. While
> rcu-order only links certain fence events (calls to synchronize_rcu(),
> rcu_read_lock(), or rcu_read_unlock()), rcu-fence links any events
> that are separated by an rcu-order link. This is analogous to the way
> -the strong-fence relation links events that are separated by an
> +the strong-order relation links events that are separated by an
> smp_mb() fence event (as mentioned above, rcu-order links act kind of
> -like strong fences). Written symbolically, X ->rcu-fence Y means
> -there are fence events E and F such that:
> +like strong ordering operations). Written symbolically, X ->rcu-fence Y
> +means there are fence events E and F such that:
>
> X ->po E ->rcu-order F ->po Y.
>
> From the discussion above, we see this implies not only that X
> executes before Y, but also (if X is a store) that X propagates to
> -every CPU before Y executes. Thus rcu-fence is sort of a
> -"super-strong" fence: Unlike the original strong fences (smp_mb() and
> +every CPU before Y executes. Thus unlike strong fences (smp_mb() and
> synchronize_rcu()), rcu-fence is able to link events on different
> CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't
> really a fence at all!)
>
> Finally, the LKMM defines the RCU-before (rb) relation in terms of
> rcu-fence. This is done in essentially the same way as the pb
> -relation was defined in terms of strong-fence. We will omit the
> +relation was defined in terms of strong-order. We will omit the
> details; the end result is that E ->rb F implies E must execute
> before F, just as E ->pb F does (and for much the same reasons).
>
> @@ -2134,7 +2163,7 @@ intermediate event Z such that:
>
> and either:
>
> - Z is connected to Y by a strong-fence link followed by a
> + Z is connected to Y by a strong-order link followed by a
> possibly empty sequence of xb links,
>
> or:
> @@ -2153,10 +2182,10 @@ The motivations behind this definition are straightforward:
> from W, which certainly means that W must have propagated to
> R's CPU before R executed.
>
> - strong-fence memory barriers force stores that are po-before
> - the barrier, or that propagate to the barrier's CPU before the
> - barrier executes, to propagate to all CPUs before any events
> - po-after the barrier can execute.
> + Strong ordering operations force stores that are po-before
> + the operation or that propagate to the CPU that begins the
> + operation before the operation executes, to propagate to all
> + CPUs before any events po-after the operation execute.
>
> To see how this works out in practice, consider our old friend, the MP
> pattern (with fences and statement labels, but without the conditional
> @@ -2485,7 +2514,7 @@ sequence or if W can be linked to R by a
> sequence. For the cases involving a vis link, the LKMM also accepts
> sequences in which W is linked to W' or R by a
>
> - strong-fence ; xb* ; {w and/or r}-pre-bounded
> + strong-order ; xb* ; {w and/or r}-pre-bounded
>
> sequence with no post-bounding, and in every case the LKMM also allows
> the link simply to be a fence with no bounding at all. If no sequence
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 07f884f9b2bf..1d91edbc10fe 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -36,9 +36,7 @@ let wmb = [W] ; fencerel(Wmb) ; [W]
> let mb = ([M] ; fencerel(Mb) ; [M]) |
> ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
> - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> - ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> - fencerel(After-unlock-lock) ; [M])
> + ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
> let gp = po ; [Sync-rcu | Sync-srcu] ; po?
> let strong-fence = mb | gp
>
> @@ -91,8 +89,12 @@ acyclic hb as happens-before
> (* Write and fence propagation ordering *)
> (****************************************)
>
> -(* Propagation: Each non-rf link needs a strong fence. *)
> -let pb = prop ; strong-fence ; hb* ; [Marked]
> +(* Strong ordering operations *)
> +let strong-order = strong-fence | ([M] ; po-unlock-lock-po ;
> + [After-unlock-lock] ; po ; [M])
> +
> +(* Propagation: Each non-rf link needs a strong ordering operation. *)
> +let pb = prop ; strong-order ; hb* ; [Marked]
> acyclic pb as propagation
>
> (*******)
> @@ -141,7 +143,7 @@ let rec rcu-order = rcu-gp | srcu-gp |
> (rcu-order ; rcu-link ; rcu-order)
> let rcu-fence = po ; rcu-order ; po?
> let fence = fence | rcu-fence
> -let strong-fence = strong-fence | rcu-fence
> +let strong-order = strong-order | rcu-fence
>
> (* rb orders instructions just as pb does *)
> let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
> @@ -169,7 +171,7 @@ flag ~empty mixed-accesses as mixed-accesses
> (* Executes-before and visibility *)
> let xbstar = (hb | pb | rb)*
> let vis = cumul-fence* ; rfe? ; [Marked] ;
> - ((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
> + ((strong-order ; [Marked] ; xbstar) | (xbstar & int))
>
> (* Boundaries for lifetimes of plain accesses *)
> let w-pre-bounded = [Marked] ; (addr | fence)?
> @@ -180,9 +182,9 @@ let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
> [Marked]
>
> (* Visibility and executes-before for plain accesses *)
> -let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
> +let ww-vis = fence | (strong-order ; xbstar ; w-pre-bounded) |
> (w-post-bounded ; vis ; w-pre-bounded)
> -let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
> +let wr-vis = fence | (strong-order ; xbstar ; r-pre-bounded) |
> (w-post-bounded ; vis ; r-pre-bounded)
> let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
>
> --
> 2.17.1
>

\
 
 \ /
  Last update: 2023-03-26 23:45    [W:0.744 / U:0.036 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site