• Jonas Oberhauser's avatar
    tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po · dd409de2
    Jonas Oberhauser authored
    LKMM uses two relations for talking about UNLOCK+LOCK pairings:
    
    	1) po-unlock-lock-po, which handles UNLOCK+LOCK pairings
    	   on the same CPU or immediate lock handovers on the same
    	   lock variable
    
    	2) po;[UL];(co|po);[LKW];po, which handles UNLOCK+LOCK pairs
    	   literally as described in rcupdate.h#L1002, i.e., even
    	   after a sequence of handovers on the same lock variable.
    
    The latter relation is used only once, to provide the guarantee
    defined in rcupdate.h#L1002 by smp_mb__after_unlock_lock(), which
    makes any UNLOCK+LOCK pair followed by the fence behave like a full
    barrier.
    
    This patch drops this use in favor of using po-unlock-lock-po
    everywhere, which unifies the way the model talks about UNLOCK+LOCK
    pairings.  At first glance this seems to weaken the guarantee given
    by LKMM: When considering a long sequence of lock handovers
    such as below, where P0 hands the lock to P1, which hands it to P2,
    which finally executes such an after_unlock_lock fence, the mb
    relation currently links any stores in the critical section of P0
    to instructions P2 executes after its fence, but not so after the
    patch.
    
    P0(int *x, int *y, spinlock_t *mylock)
    {
            spin_lock(mylock);
            WRITE_ONCE(*x, 2);
            spin_unlock(mylock);
            WRITE_ONCE(*y, 1);
    }
    
    P1(int *y, int *z, spinlock_t *mylock)
    {
            int r0 = READ_ONCE(*y); // reads 1
            spin_lock(mylock);
            spin_unlock(mylock);
            WRITE_ONCE(*z,1);
    }
    
    P2(int *z, int *d, spinlock_t *mylock)
    {
            int r1 = READ_ONCE(*z); // reads 1
            spin_lock(mylock);
            spin_unlock(mylock);
            smp_mb__after_unlock_lock();
            WRITE_ONCE(*d,1);
    }
    
    P3(int *x, int *d)
    {
            WRITE_ONCE(*d,2);
            smp_mb();
            WRITE_ONCE(*x,1);
    }
    
    exists (1:r0=1 /\ 2:r1=1 /\ x=2 /\ d=2)
    
    Nevertheless, the ordering guarantee given in rcupdate.h is actually
    not weakened.  This is because the unlock operations along the
    sequence of handovers are A-cumulative fences.  They ensure that any
    stores that propagate to the CPU performing the first unlock
    operation in the sequence must also propagate to every CPU that
    performs a subsequent lock operation in the sequence.  Therefore any
    such stores will also be ordered correctly by the fence even if only
    the final handover is considered a full barrier.
    
    Indeed this patch does not affect the behaviors allowed by LKMM at
    all.  The mb relation is used to define ordering through:
    1) mb/.../ppo/hb, where the ordering is subsumed by hb+ where the
       lock-release, rfe, and unlock-acquire orderings each provide hb
    2) mb/strong-fence/cumul-fence/prop, where the rfe and A-cumulative
       lock-release orderings simply add more fine-grained cumul-fence
       edges to substitute a single strong-fence edge provided by a long
       lock handover sequence
    3) mb/strong-fence/pb and various similar uses in the definition of
       data races, where as discussed above any long handover sequence
       can be turned into a sequence of cumul-fence edges that provide
       the same ordering.
    Signed-off-by: default avatarJonas Oberhauser <jonas.oberhauser@huaweicloud.com>
    Reviewed-by: default avatarAlan Stern <stern@rowland.harvard.edu>
    Acked-by: default avatarAndrea Parri <parri.andrea@gmail.com>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
    dd409de2
linux-kernel.cat 7.71 KB