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

[Boehm, Hans]

I'm trying to make another pass over the strawman proposal.  Thinking
about this, I think I've ended up with somewhat contradictory goals.  My
wish-list:

1) Data-race-free programs (based on the sequentially-consistent
interpretation) have sequentially consistent semantics, at least if they
use "ordinary" synchronization primitives. 

2) We would like to accommodate "synchronization" reads and writes
(atomics) that are allowed to participate in what would otherwise be
data races.  We would like these to provide variants that have weak
ordering properties.  In particular, the "synchronization" operations
themselves are allowed to behave in a way that is not sequentially
consistent.

3) We would like to avoid restrictions based on causality, since that's
hard to define and gets us into all sorts of messy issues.

4) (??) Ideally it should be the case that if I start with a
data-race-free program, and change some of the loads and stores to
synchronization operations, this should not allow any additional
outcomes that were not legal for the original program.

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
> > 

If x and y are ordinary variables, I think it actually makes sense, and
is surprisingly clean, to restrict ordinary variables to sequential
consistency.  (After all, we're only interested in whether they are
involved in a race, not the outcome.  If there is no race, we want them
to behave sequentially consistently anyway.)  And we get property (1)
back.

The problem is that if we now turn x and y into unordered
synchronization variables, r1 = r2 = 1 is allowed by happens-before
consistency, which clearly violates (4).  (It probably satisfies (1) to
the extent we want it satisfied, i.e. it holds for "ordinary"
synchronization operations.)

Is this OK?

If not, the solutions seem me to be:

- Deal with causality, or
- Add an add hoc rule that unordered synchronization variables which
don't participate in "races" behave like ordinary variables.

I'd be inclined to say it's OK.  Presumably you're using atomics, you're
both expecting a race, and you know what you're doing, so it doesn't
matter.

Hans