[cpp-threads] sequential consistency for race-free programs
Boehm, Hans
hans.boehm at hp.com
Fri Jul 15 02:26:17 BST 2005
I agree. But I think the problem is that precisely defining what it
means for the compiler to speculate either requires the same complexity
as in the Java model treatment of causality, or we need to restrict
ourselves to sequential consistency in defining data races. And the
latter doesn't handle the case in which a data race on ordinary
variables is possible only because of non-sequentially-consistent
behavior of atomics.
How about a compromise? We insist that ordinary memory operations be
sequentially consistent in the data race definition, which I still think
(as of 18:22, 7/14/05) is technically OK, and makes things fully precise
for simple programs, and wave our hands and say "no speculative stores"
for atomics? That's imprecise, but I think it limits the damage to
programs using the atomics library. And as a practical matter, the
tricky optimization questions are far more likely to arise for ordinary
variables than for atomics. We thus have some hope that the remaining
ambiguities will never need to be explored.
Does this sound reasonable?
Hans
-----Original Message-----
From:
Cpp-threads_decadentplace.org.uk-bounces at decadentplace.org.uk
[mailto:Cpp-threads_decadentplace.org.uk-bounces at decadentplace.org.uk]
On Behalf Of Maged Michael
Sent: Thursday, July 14, 2005 6:03 PM
To: cpp-threads at decadentplace.org.uk
Subject: RE: [cpp-threads] sequential consistency for race-free
programs
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.o
rg.uk
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://shadbolt.decadentplace.org.uk/pipermail/cpp-threads/attachments/20050714/6e7e1322/attachment.htm
More information about the cpp-threads
mailing list