[cpp-threads] sequential consistency for race-free programs

[Bill Pugh]

On Jul 14, 2005, at 4:45 AM, Peter Dimov wrote:
>> Now reconsider Bill's example:
>>
>>
>>>> Initially x = y = 0
>>>>
>>>> Thread 1:
>>>> r1 = x
>>>> if (r1) y = 1
>>>>
>>>> Thread 2:
>>>> r2 = y
>>>> if (r2) x = 1
>>>>
>
> Why is it important to make the example above well-defined? Even  
> with important-sounding variable names as "launch_all_missiles", it  
> still seems terribly contrived to me.
>
> The "data-race-free" rule, as taught to programmers, is simple: an  
> ordinary variable that is shared between threads shall never be  
> accessed without a lock. This example violates the rule. Why should  
> it be defined? Is it even possible for a non-expert to write  
> correct data-race-free code that doesn't adhere to the rule? I'm  
> inclined to answer "no".


Sorry to be out of the loop for a while on this.

You _have_ to accept this program as being a correctly synchronized,  
data-race free program. Every thing that has been
done for more than a decade in academic research on synchronization  
defines this as correctly synchronized, and there are lots
of equivalent programs that raise exactly the same issues but are  
much harder to accept as being programs
that contain data races.

Here is a similar example:

Initially, p = &p and q = &q

Thread 1:
r1 = p
*r1 = &p

Thread 2:
r2 = q
*r2 = &q

All sequentially consistent executions of this example are data race  
free,
but it is happens-before consistent to have r1 = q and r2 = p. But as  
the threads
interact with completely disjoint variables, I don't see anyway you  
can argue that
this program is incorrectly synchronized.

The point is, you can't use what operations occur textually in the  
program source to decide
whether the program is correctly synchronized; the meaning of  
programs is determined
by what they do when executed.

Bill

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://shadbolt.decadentplace.org.uk/pipermail/cpp-threads/attachments/20050806/a6716d19/attachment.htm