51d
Subj : Re: Formal Mutex Semantics
To   : comp.programming.threads
From : Chris Thomasson
Date : Sat Aug 13 2005 03:50 pm

"David Hopwood" <david.nospam.hopwood@blueyonder.co.uk> wrote in message 
news:JzqLe.2292$Xf3.801@fe2.news.blueyonder.co.uk...
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;

I was thinking about using something like this:

http://groups.google.ca/group/comp.programming.threads/msg/55a0d8941bd9450b?hl=en




or, this:

http://groups.google.ca/group/comp.programming.threads/msg/f9efdbf2472c7c0d?hl=en


Simple enough...

;)

.

0