Messages in this thread | | | Date | Fri, 24 Feb 2023 10:37:58 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po |
| |
On Fri, Feb 24, 2023 at 10:32:43AM -0500, Alan Stern wrote: > On Fri, Feb 24, 2023 at 02:52:51PM +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/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 letting fence contribute > > to ppo only in case the fence links events of the same thread. > > > > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > > --- > > tools/memory-model/linux-kernel.cat | 2 +- > > 1 file changed, 1 insertion(+), 1 deletion(-) > > > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > > index cfc1b8fd46da..adf3c4f41229 100644 > > --- a/tools/memory-model/linux-kernel.cat > > +++ b/tools/memory-model/linux-kernel.cat > > @@ -82,7 +82,7 @@ let rwdep = (dep | ctrl) ; [W] > > let overwrite = co | fr > > let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) > > let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) > > -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) > > +let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int) > > > > (* Propagation: Ordering from release operations and strong fences. *) > > let A-cumul(r) = (rfe ; [Marked])? ; r > > Acked-by: Alan Stern <stern@rowland.harvard.edu>
Queued for the v6.4 merge window (not the current one), thank you both!
Thanx, Paul
| |