Messages in this thread | | | Date | Mon, 27 Feb 2023 20:35:11 +0100 | From | Andrea Parri <> | 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; > }
nit: for readability if not for other, s/int *x/spinlock_t *x/.
> 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>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Andrea
> --- > 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 > -- > 2.17.1 >
| |