[cpp-threads] Slightly revised memory model proposal (D2300)

[Boehm, Hans]

I've attached another revision of the memory model (D2334) and the
sequential consistency proofs (D2335).

The former was minimally revised to fix the bug that Sarita pointed out.
(I know that there is a discussion about this in progress; I'll comment
on that separately.  This actually corresponds vaguely to functionally
similar text that was there way back when, e.g. in
http://www.hpl.hp.com/personal/Hans_Boehm/c++mm/mm.html, but got lost
somewhere in the revision process.)

I also removed the stronger synchronizes with guarantee for SC atomic
stores.  It also looks to me like that has implementability issues, and
I don't think it's critical.

The proofs grew significantly.  I added the proof that races in the
official model correspond to SC races.  (This wasn't true before the
above fix.  The right theorem wasn't even stated.)  I also added a
theorem stating effectively that, in the absence of trylock, races
correspond to simultaneous execution of conflicting operations.  I think
that one is also important in trying to explain this to programmers.

(If you see empty boxes in D2335 where there should be text, please read
those as set union symbols.  It displays fine on my Linux box, but the
standard IE font around here seems to be missing the symbol.)

Hans
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.decadentplace.org.uk/pipermail/cpp-threads/attachments/20070706/5803a142/D2335-0001.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.decadentplace.org.uk/pipermail/cpp-threads/attachments/20070706/5803a142/D2334-0001.html