Subj : Re: Formal Mutex Semantics
To   : comp.programming.threads
From : Joe Seigh
Date : Tue Aug 16 2005 12:41 pm

Maciej Sobczak wrote:
> Joe Seigh wrote:
> 
>> The mutex m1 has no effect since both threads aren't using it.
> 
> 
> Yes, that's the point.
> 
>> Mutex
>> rule 2, since the 2nd thread sees a store by the 1st thread after its
>> lock action, the 2nd thread sees all stores by the 1st thread before its
>> unlock action.  The store of a is before the unlock action by thread 1.
> 
> 
> That's fine - so you define it as "flush all, refresh all".
> Isn't it unnecessarily restrictive? I know that relaxing it would be 
> confusing (for example, it would break the example from recent thread, 
> "Memory visibility with Pthreads"), but it would still allow to write 
> correct programs and in addition enable potential performance gains, 
> since less stores would have required visibility.
> In that relaxed model, stores made outside any locks would have 
> absolutely no guarantee with regard to their visibility in other threads.

Current thread usage patterns would break, e.g. initializing an object
and queuing it onto a synchronized queue.  You'd have to either iniitialize
the object while holding the queue lock or copy it while holding the queue
lock.  Either way would increase the lock hold time and the probability of
contention.

> 
>>> Related question: what does POSIX guarantee for this example?
>>
>>
>> Posix though it best not to confuse you by trying to define anything.
> 
> 
> No jokes please. If I'm writing programs using pthreads then I should be 
> able to reason about them, no?
> 
> 
What joke?  That's the official Posix position on the issue.

"Formal definitions of the memory model were rejected as unreadable by the vast majority of programmers. In addition, most of the formal work in the literature has concentrated on the memory as provided by the hardware as opposed to the application programmer through the compiler and runtime system. It was believed that a simple statement intuitive to most programmers would be most effective. IEEE Std 1003.1-2001 defines functions that can be used to synchronize access to memory, but it leaves open exactly 
how one relates those functions to the semantics of each function as specified elsewhere in IEEE Std 1003.1-2001. IEEE Std 1003.1-2001 also does not make a formal specification of the partial ordering in time that the functions can impose, as that is implied in the description of the semantics of each function. It simply states that the programmer has to ensure that modifications do not occur "simultaneously" with other access to a memory location."



-- 
Joe Seigh

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

.