Messages in this thread Patch in this message | | | Date | Sun, 26 Feb 2023 16:23:42 +0000 | From | Joel Fernandes <> | Subject | Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po |
| |
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)
Alternatively can be the following appended diff? Requires only single 'int' in ->ppo then and prevents future similar issues caused by sub relations. Also makes clear that ->ppo can only be CPU-internal.
Or would that not work for some reason? For the test you shared at least, the graphs are the same.
Either way:
Tested-by: Joel Fernandes (Google) <joel@joelfernandes.org> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>
---8<-----------------------
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 07f884f9b2bf..63052d1628e9 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -70,7 +70,7 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) let to-r = addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) +let ppo = (to-r | to-w | fence | po-unlock-lock-po) & int (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = (rfe ; [Marked])? ; r
| |