Subj : Re: Formal Mutex Semantics
To   : comp.programming.threads
From : Joe Seigh
Date : Tue Aug 16 2005 10:59 am

Maciej Sobczak wrote:
> Joe Seigh wrote:
> 
>> Here's some stuff I was doing a while back on defining thread semantics.
> 
> [...]
> 
> I cannot find it stated explictly, so here's my request for clarification:
> 
> Let's suppose there are two shared mutexes (m1, m2) and two shared 
> variables (a, b) initialized to 0.
> One thread does this:
> 
> lock(m1);      // you can remove this line
> a = 1;
> unlock(m1);    // you can remove this line
> lock(m2);
> b = 1;
> unlock(m2);
> 
> and another thread does this:
> 
> lock(m2);
> if (b == 1) assert(a == 1);
> unlock(m2);
> 
> Question is: does your "mutex semantics" guarantee the assertion above?
> In other words: is the visibility of stores guaranteed for all stores 
> that happened before unlock(m2) in thread 1, even if those stores where 
> performed before lock(m2)?
> 
The mutex m1 has no effect since both threads aren't using it.   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.

> I think such guarantee is not needed and the more relaxed version would 
> guarantee that the visibility of stores is guaranteed only for those 
> stores that were done when the given mutex was locked. Locking different 
> mutex (or not locking it at all - if you remove respective lines above) 
> would not guarantee anything with respect to the other thread. It is 
> like having stores which are associated only with a given mutex (some 
> interesting issues may arise when many mutexes are locked at the same 
> time), or putting it in other words, having *selective* flush/refresh 
> with the mutex object used as a key for selection.
> 
> What was your intention with regard to the example above?
> 
> Related question: what does POSIX guarantee for this example?

Posix though it best not to confuse you by trying to define anything.
You supposedly have inate intuitive knowlege of mutex semantics.


-- 
Joe Seigh

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

.