On Fri, Sep 10, 2021 at 07:12:21PM +0200, Peter Zijlstra wrote: > On Fri, Sep 10, 2021 at 12:36:32PM -0400, Alan Stern wrote: > > +Here the second spin_lock() is po-after the first spin_unlock(), and > > +therefore the load of x must execute before the load of y, even tbough > > I think that's commonly spelled: though, right? ^^^^^^ Oops, yes, I missed that. Good eye! > > --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt > > +++ usb-devel/tools/memory-model/Documentation/explanation.txt > > @@ -1813,15 +1813,16 @@ spin_trylock() -- we can call these thin > > lock-acquires -- have two properties beyond those of ordinary releases > > and acquires. > > > > +First, when a lock-acquire reads from or is po-after a lock-release, > > +the LKMM requires that every instruction po-before the lock-release > > +must execute before any instruction po-after the lock-acquire. This > > +would naturally hold if the release and acquire operations were on > > +different CPUs and accessed the same lock variable, but the LKMM says > > +it also holds when they are on the same CPU, even if they access > > +different lock variables. For example: > > Could be I don't understand this right, but the way I'm reading it, it > seems to imply RCsc. Which I don't think we're actually asking at this > time. No, it doesn't imply RCsc. This document makes a distinction between when a store executes and when it becomes visible to (or propagates to) other CPUs. Thus, even though write 1 executes before write 2, write 2 might become visible to a different CPU before write 1 does. In fact, on non-other-multicopy-atomic systems, two writes might become visible to different CPUs in different orders (think of the IRIW litmus pattern.) Or to consider a more relevant example, a write can execute before a read even though the write doesn't become visible to other CPUs until after the read is complete. If you want, you can read this as saying "execute as seen from its own CPU" (although even that isn't entirely right, since a write can be visible to a po-later read which nevertheless executes before the write does). Or think of a write as executing when its value gets put into the local store buffer, rather than when it gets put into the cache line. Alan
|