[cpp-threads] Alternatives to SC

[Paul E. McKenney]

On Mon, Jan 15, 2007 at 09:18:12AM -0500, Doug Lea wrote:
> 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}.

OK, so informally, causality propagates through any thread that has at
least one write operation involved in the chain of causality.  I need
to do more examples, but CCCC is still sounding pretty promising from
my viewpoint.

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

Thank you for the tips, will try this.  Though I suspect that SW analysis
might be a good thing at some point.  ;-)

							Thanx, Paul