Subj : Formal Mutex Semantics To : comp.programming.threads From : Joe Seigh Date : Sat Aug 13 2005 10:23 am Here's some stuff I was doing a while back on defining thread semantics. It's based on earlier work to define mutex semantics. It's not complete. I only reworked in the mutex semantics and the other sections are blank for now. I haven't worked on it for over a year and it's currently inactive. It's based on observable semantics and there is no memory model to speak of except for a couple of parts. Basically stores are visible or not visible. You prove assertions about programs by proving certain value(s) are either visible or not visible. The semantic rules are basically arbitrary. You want rules that are sufficient and necessary to prove the typical assertions you might make about a program. Examples I used in developing the mutex rules were a program that spawns 10 threads that under guard of a mutex increment by 1 an integer that was initially 0. Prove the intedger is 10 after the threads complete. Another is spawn 2 threads which store a different value into an integer guarded by a mutex. Prove that the final value has to be one of the values. Assume the integer isn't atomic in this case. Some interesting points. Lock actions have no observable actions. Lock critical regions don't have to be temporally exclusive unless you want to define them that way. Locks don't guarantee forward progress though some peope assume this. You can only infer a lock was acquired after another thread released it by observing some action by the other thread before it released the lock. I was thinking of tying forward progress in with signaling. Volatile would have been nice to use as a forward progress hint except giving volatile a clean semantic definition would probably confuse everyone at this point. Memory barriers are just another synchronization construct. You could leave them out. They're not needed since there's no memory model. They are useful as a low level synchronization api. The difference between this and a "memory model" is there is you aren't defining sematics as a meta implementation which may be unnecessarily restrictive (eg. lock actions). =============================================================================== 4/8/2004 Storage Visibility (V) 1) All fetches and stores are atomic. Non-atomic data can be considered as accessed by multiple separate fetches or stores. 2) Stores can be in one of three states; not yet visible, no longer visible (collectively referred to as invisible), or visible. 3) All variables have an initial visible value. 4) A fetch returns a visible value. 5) Prior fetch values are no longer visible if different. 6) Subsequent stores are not yet visible. 7) Prior values replaced by a store are no longer visible. Memory barriers (etc…) infer both invisibility and visibility. Memory locations that do not have all visible values as being defined (known about) are undefined. Functions that can modify memory in an undefined way put the memory into an undefined state (unknown/undefined stores). Deletion of memory puts memory into an undefined state. GC or that point at which asynchronous GC (i.e. RCU quiesce points) can occur also put that memory into an undefined state. Threads – Creation and Termination (T) 1) Any stores no longer visible to a thread before a fork are no longer visible to the new thread. 2) Any stores not yet visible to a new thread are not yet visible before the fork. 3) Any stores visible to a thread when it terminates, are visible to a thread that does a join on that thread. 4) Any stores not yet visible to a thread doing a join, are not yet visible to the terminating thread. Memory Allocation and Deletion Deletion can be considered as starting another unknown thread (asynchronous) that stores into memory. Memory modified by asynchronous functions can be put back to a known state by re-initializing (?necessary?). Generic Memory Barriers (B) Acquire Release Dependent Load Smart Pointers (P) Mutexes (M) 1) The number of lock actions and unlock actions by any given thread are subject to the following constraint 0 <= (#locks - #unlocks) <= 1 The difference is referred to as the (thread) lock count and when the lock count == 1, the thread is in a locked region and is said to hold the lock. Lock and unlock actions are associated with a lock object. 2) If a store by a thread after a lock action is visible to a second thread holding the same lock, then all stores visible to the first thread before its unlock action are visible to the second thread after its lock action. This is true even if the first and second threads are the same as long as the lock actions are different 3) If a store by a thread after a lock action is not visible to a second thread holding the same lock, then stores not visible to the first thread before its lock action are not visible to the second thread before its unlock. This is true even if the first and second threads are the same as long as the lock actions are different occurrences Corollary Multiple fetches and stores within a locked region are atomic with respect to other occurrences of the same locked region. Signaling – Events, Semaphores and Condition Variables Forward Progress Various Notes Indeterminism in the memory model: These definitions allow for some amount of indeterminism in the memory model that should be exploited by the implementation for efficiency and performance. This flexibility is especially useful in the case of distributed shared objects, NUMA systems, and transputers, which don't have central shared memory. Although the memory model may appear to have well defined, totally ordered sequence of values for each variable, that is just an appearance. The implementation may modify the sequence as long as the results of execution conform to the definitions. E.g. a store may be arbitrarily inserted any where in a variables value history sequence as no constraints are violated. Storage Consistency Order The visible order of stores for any storage location is the same for all threads. I.e., if one thread sees two stores in a particular order, then any other thread seeing the same two stores, sees them in the same order. Visibility of stores: Visibility of a value replace by a store isn't the same a seeing the value. The actual (instance or occurrence of the) variable replaced, determines visibility. Specific values being fetched: For proving that a particular value must be fetched, one needs to show that only that value is visible and that no other values are visible. Staleness: Values are allowed to be arbitrarily "stale". See "Immediacy and forward progress". Temporal exclusion of locked regions: There is no requirement. This is deliberate. Locked regions do not have to appear to execute in the order that clock reads within the regions may suggest. Requiring temporal exclusion would place an unnecessary restriction on implementations. There are ways of imposing such an ordering if it is thought to be needed. Immediacy and forward progress: There is also no mechanism that forces "immediate" visibility. Locks don't have any intrinsic memory barrier functionality. They merely denote or bracket locked regions. The requirement for forward progress should be met by specialized mechanisms such as volatile variables or condition variables. This would allow for tradeoffs in the various parts of the implementation. The higher overhead required for these functions would be restricted to their implementation and not be required of the general implementation. Not burdening the general memory model with this requirement allows more flexibility in the implementation for the purposes of efficiency and performance. Store followed by a fetch: There is no requirement for a store of a variable followed by a fetch of that variable to cause the value to be "flushed" to "shared memroy". Lost stores: A store is allowed to be "lost" if there are no circumstances that require it to be seen by other threads. The memory model allows this. The "store" and "fetches" in the definitions refer to thread actions. Word tearing: This is defined as update to variables less than the atomic word size that are done as a read, modify, and store. -- Joe Seigh When you get lemons, you make lemonade. When you get hardware, you make software. .