[cpp-threads] Alternatives to SC

[Doug Lea]

Jeremy Manson wrote:
> 
>>
>> Yes. As a first approximation, CAS can be modeled as a read followed
>> by a write. The model can be made more precise about effects by
>> explicitly adding it as an event though.
>>
> 
> Wouldn't a CAS being modeled this way give up atomicity?  i.e.,
> 

Here's how. And while I'm at it, a sketch of further steps
you might take to turn CCCC core into a full language-level
memory model.
(Most of this is on hold while I do other things though.)

1. As a preliminary, the version I posted needlessly requires
orderings for writes that are never read. There's an easy way
to relax this technically, at the expense of breaking the
helpful correspondence between 4 ideas == 4 rules, without
adding anything useful. Except it may be useful for (2) ...

2. It's also easy to incorporate CAS (and other RMWs) under the
fiction (or, on some machines, fact) that a CAS etc always
writes, but writes the old value again on failure. This
unconditionally orders CAS(x) in W(x). For LL/SC this might be
too much of a  fiction, but language-level models usually don't
deal with LL/SC since it isn't supported on most machines.
One downside of always-write approach is that a successful
CAS may include a chain of predecessors to previously
failed CASing threads before hitting the one that originally
wrote the value. This is fine except that it adds clutter to
derivations, that is only partially helped by (1) above.

3. To address less-than-strong-atomics, you can define
"lazyWrite", which promises that eventually the write of x becomes
part of the global W(x), and does so in (local) FIFO order.
This may entail explicitly modeling the resulting parallelism between
the instruction stream and the store mechanics, but in a way
that is hopefully ignorable when expressed at language level.
LazyWrite can be mapped to C++ atomic<release> and Java AtomicX.lazySet.
Which then invites "eagerRead" which permits returning lazyWrites.
Although since the semantics of reads rely on flavor of write,
the mechanics of eager- and strong- reads are likely
the same -- locally maintaining program-order.

4. For ordinary variables and raw atomics, you then need to
introduce instruction-level parallelism/reorderings,
perhaps as par{op1, op2, ..}, in turn respecting
program-order dependencies, which can be done by incorporating Vijay
Saraswat et al's RAO (http://www.saraswat.org/rao.html).

At this point, I'm not sure that any of this outside the core
is anything beyond an academic exercise. But as I've been saying,
core CCCC might itself be useful in explaining the semantics of
volatiles/strong-atomics.

-Doug