lkml.org 
[lkml]   [2023]   [Feb]   [24]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    Patch in this message
    /
    From
    Subject[PATCH v3] tools/memory-model: Make ppo a subrelation of po
    Date
    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
    --
    2.17.1
    \
     
     \ /
      Last update: 2023-03-27 00:34    [W:3.738 / U:0.108 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site