Subj : Re: Formal Mutex Semantics
To   : comp.programming.threads
From : Joe Seigh
Date : Sun Aug 14 2005 12:05 pm

David Hopwood wrote:
> Joe Seigh wrote:
> 
>> 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 difference in your approach is that you're attempting to define the 
> model
> using an (informal) axiomatic semantics rather than an operational 
> semantics;
> not that you're not defining a memory model. An axiomatic semantics can 
> indeed
> make it easier to avoid overspecification, although it also makes under-
> specification more likely, since it's easy to overlook necessary axioms.

There's some memory model but it's as minimal as I can make it.  Axiomatic
semantics based on observable behavior is easier to understand and use.
Contrast that with the first version of Java's semantics which were so
complicated and obstruse, it wasn't clear anyone understood it other then
the mechanical theorm provers they likely used to prove it "correct".
With meta-implementation as specification, though it specifies something
(assuming the meta semantics are clear), it's not alway clear what.  Though
I suppose you could claim it's arbitrary and let history determine whether it's
useful or not.

> 
>> 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.
> 
> [...]
> 
> 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.
> 
I agree it needs more work but given the lack of interest in axiomatic
approach I haven't put too much effort into it, none since 4/8/2004.
I posted it more as a contrast to the discussions of mutex semantics which
are base on nothing but intuitive guesses as what mutex semantics might
actually be.  Some of those are completely off the mark since they
make claims for unobservable behavior.  The stuff I did isn't completely
arbitrary since I reverse engineered it from common thread usage patterns
and went through the necessary, sufficient, consistent, and useful exercises
to some extent.


-- 
Joe Seigh

When you get lemons, you make lemonade.
When you get hardware, you make software.

.