[cpp-threads] Alternatives to SC

[Doug Lea]

Paul E. McKenney wrote:

> So I repeat #2 until there are no more reachable writes, rather than
> applying it only to nodes that were produced by #1, correct?
> 

Yes.

With any formal memory model, it is almost always easiest to
show derivations graphically on a piece of paper. That's what I
usually do. Here's a recipe for doing this with CCCC:

1. Make nodes for all events
2. Add the program-order, write-serialization, and freshness edges.
3. Add causality edges.
4. For each thread i, check if there is a cycle in {i's events unioned
    with all writes}.

In practice, you can combine (3) and (4), adding edges until
you see cycle, or can't add any more. Also, the graphical version
allows you to bypass the error-prone transitive closure and "w"
expansions -- you don't need them to visually see cycle.

Usually, I only revert back to textual form when verifying that
each of the arrows actually stemmed from some rule.

-Doug