17.6 Rules about the Interaction of Locks and Variables

Let T be any thread, let V be any variable, and let L be any lock. There are certain constraints on the actions performed by T with respect to V and L:

• Between an assign action by T on V and a subsequent unlock action by T on L, a store action by T on V must intervene; moreover, the write action corresponding to that store must precede the unlock action, as seen by main memory. (Less formally: if a thread is to perform an unlock action on any lock, it must first copy all assigned values in its working memory back out to main memory.)
• Between a lock action by T on L and a subsequent use or store action by T on a variable V, an assign or load action on V must intervene; moreover, if it is a load action, then the read action corresponding to that load must follow the lock action, as seen by main memory. (Less formally: a lock action acts as if it flushes all variables from the thread's working memory; before use they must be assigned or loaded from main memory .)