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

[Maged Michael]

Hans Boehm wrote:
> But here's an example that might be instructive anyway, particularly
> because I don't yet like how any of the proposals deals with it.  (I
> think
> this is similar to one of the JSR 133 discussions which I can't
> immediately find):
>
> Thread 1:
> while (!self_destruct_left);
> self_destruct_right = true;
> blow_up_port_side_of_ship();
>
> Thread 2:
> while (!self_destruct_right);
> self_destruct_left = true;
> blow_up_starboard_side_of_ship();
>
> (Assume for now that there is no code to set self_destruct_left
> or self_destruct_right.  Naively both threads should loop forever,
> and the ship should be safe.)
>
> With ordinary variables, and the guarantee we are discussing, things
> behave as expected.  (Though we can't easily add an actual
> self-destruct mechanism, since that would involve a race.)
>
> With happens-before consistency and undefined semantics for races,
> anything can happen, including the ship blowing up immediately.
>
> If we use atomics instead, with unordered semantics, I think the
> ship is allowed to blow up immediately, under all proposals.  That's
> slightly weird, I think.

Consider the following rule: "No speculative stores to shared locations 
(or any actions with externally observable side-effects) are allowed", 
where "speculative" means that the compiler is not absolutely certain of 
the value to be stored.

If we follow this rule, the compiler will not allow the speculative stores 
to the self_destruct_... variables or the blowup_... actions. It will also 
not allow the out-of-thin-air scenario in Figure 4 of the Java Memory 
Model paper
http://www.cs.umd.edu/users/jmanson/java/popl05.pdf

However this rule will allow the acceptable scenarios in Figures 5 and 6 
of the same paper. In these examples what looks like speculative stores 
are not really speculative because the compiler can determine the value to 
be stored with absolute certainty.

Maged




"Boehm, Hans" <hans.boehm at hp.com> 
Sent by: Cpp-threads_decadentplace.org.uk-bounces at decadentplace.org.uk
07/14/2005 07:46 PM
Please respond to
cpp-threads


To
<cpp-threads at decadentplace.org.uk>
cc

Subject
RE: [cpp-threads] sequential consistency for race-free programs






The real question here is what it means to be "shared between threads".
Clearly people (including ordinary programmers to the extent they deal
with threads at all) routinely to the following:

1. initialize data structure S
2. Fork threads
3. Read S in multiple threads without locking

I would argue that it's unreasonable to outlaw this in a coding
standard.  It's pervasive, and it's exactly what you want people
to do.

Thus whether or not a variable is written concurrently has to
be an important part of the guidelines we give to programmers.

I think it is also fairly common to conditionally acquire locks,
particularly in libraries, as in:

if (this_program_is_multithreaded) lock(...)
...
if (this_program_is_multithreaded) unlock(...)

Not all code will obey a purely syntactic locking discipline,
even for read/write variables. C++ isn't that kind of language.

If we have to start talking about "potentially written in
code that isn't actually executed", to define data races, I think
we've lost.

My main concern is that we have a good simple story for the programmer.
I really don't see a viable replacement for something like
"Programs without a concurrent update to a shared variable have
the semantics you expect, i.e. sequential consistency."

But here's an example that might be instructive anyway, particularly
because I don't yet like how any of the proposals deals with it.  (I
think
this is similar to one of the JSR 133 discussions which I can't
immediately find):

Thread 1:
while (!self_destruct_left);
self_destruct_right = true;
blow_up_port_side_of_ship();

Thread 2:
while (!self_destruct_right);
self_destruct_left = true;
blow_up_starboard_side_of_ship();

(Assume for now that there is no code to set self_destruct_left
or self_destruct_right.  Naively both threads should loop forever,
and the ship should be safe.)

With ordinary variables, and the guarantee we are discussing, things
behave as expected.  (Though we can't easily add an actual
self-destruct mechanism, since that would involve a race.)

With happens-before consistency and undefined semantics for races,
anything can happen, including the ship blowing up immediately.

If we use atomics instead, with unordered semantics, I think the
ship is allowed to blow up immediately, under all proposals.  That's
slightly weird, I think.

If we use acquire loads for the loop tests, I think nothing is
precluded, and the ship is still allowed to blow up immediately.
(I assume that acquire loads can be paired with ordinary stores.)
There is no happens-before cycle.  I'm not sure whether that's
worse than the preceding example or not.

If we use acquire loads and release stores, I think the execution
in which the ship blows up involves a happens-before cycle, and it's
thus disallowed.  Which is good.

I believe there are published (and implemented?) optimization techniques
that could result in the outcome where the ship blows up immediately.
Thus I
think that what the spec states here matters.

I disagree that proving data-race-freedom for examples like this is
hard.
Even in large programs, the argument is likely to be confined to
small sections of code.  If the bodies in the above while loops where
large, and took care of more routine operations, the argument becomes
no more complicated.  Still neither of the self_destruct... variables
is ever set, so we shouldn't expect to execute anything after the
loop.

Hans



> -----Original Message-----
> From: Peter Dimov
> Sent: Thursday, July 14, 2005 10:41 AM
> To: cpp-threads at decadentplace.org.uk
> Subject: Re: [cpp-threads] sequential consistency for 
> race-free programs
> 
> 
> Hans Boehm wrote:
> > Peter -
> >
> > In Bill's example, no shared variables are written by 
> either thread. 
> > It's hard to tell people that they need to lock when there is no 
> > concurrent write.
> 
> Let's get back to the simple rule:
> 
> >> 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.
> 
> Note that this is a local rule. You review the code:
> 
> >>>>> Thread 1:
> >>>>> r1 = x
> >>>>> if (r1) y = 1
> 
> and you can immediately tell that it violates it. The shared 
> variable x is 
> being read without a lock. The shared variable y is being 
> written without a 
> lock. The code is broken (according to the rule). You don't need to 
> enumerate all possible candidate executions to reach this 
> conclusion, or 
> know what the other threads are doing. The code for the other 
> threads may 
> even not have been written yet.
> 
> I maintain that adhering to this rule is the only reasonable 
> way for an 
> ordinary programmer to write correct MT code.
> 
> I, personally, would never attempt to write this kind of 
> data-race-free code 
> even if it's technically legal to do so. From my perspective, 
> trying to 
> legalize this example has significant cost and brings no benefit.
> 
> The reason that taking advantage of this is hard to 
> unworkable is that it 
> requires a global analysis of the program. Proving that 
> anything beyond a 
> toy example is data-race-free seems insanely hard. Convincing 
> a compiler 
> author that his optimizations break conforming code would be 
> even harder. 
> Therefore, from a programmer's perspective, it would be 
> reasonable to avoid 
> such code or outlaw it via a coding standard.
> 
> > Think of x and y as both being named something synonymous with 
> > "application_is_single_threaded".  In that case, this code looks 
> > obviously safe.  In my opinion, making it undefined is clearly 
> > unacceptable.
> >
> > The intent of the pthread spec is also pretty clearly to 
> allow things 
> > like this.  Thus in addition to being completely 
> inconsistent with the 
> > Java spec, we'd be breaking Pthread code that was clearly 
> intended to 
> > be legal.
> 
> We wouldn't be _breaking_ it. We won't _guarantee_ that it will work. 
> Nothing guarantees its correctness today, so the status of 
> the code doesn't 
> change. 
> 
> 
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk 
> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
entplace.org.uk

-- 
cpp-threads mailing list
cpp-threads at decadentplace.org.uk
http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decadentplace.org.uk


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://shadbolt.decadentplace.org.uk/pipermail/cpp-threads/attachments/20050714/8a864d50/attachment.html