Subj : Re: Formal Mutex Semantics To : comp.programming.threads From : David Hopwood Date : Sat Aug 13 2005 07:01 pm Joe Seigh wrote: > Here's some stuff I was doing a while back on defining thread semantics= =2E > It's based on earlier work to define mutex semantics. It's not comple= te. > 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. >=20 > It's based on observable semantics and there is no memory model to spea= k of > except for a couple of parts. Basically stores are visible or not=20 > visible. You prove assertions about programs by proving certain value(= s) > are either visible or not visible. The difference in your approach is that you're attempting to define the m= odel using an (informal) axiomatic semantics rather than an operational semant= ics; not that you're not defining a memory model. An axiomatic semantics can i= ndeed make it easier to avoid overspecification, although it also makes under- specification more likely, since it's easy to overlook necessary axioms. > 4/8/2004 > Storage Visibility (V) > 1) All fetches and stores are atomic. Non-atomic data can be=20 > 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. >=20 > Memory barriers (etc=85) infer both invisibility and visibility. >=20 > Memory locations that do not have all visible values as being defined=20 > (known about) are undefined. [...] This is too vague for me to tell what it's trying to say; it needs more discussion of motivation, or more formality, or both. --=20 David Hopwood .