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

[Sarita V Adve]

Hans,

It was good to see you at FCRC.

(1) There are a few comments from the previous round that are still not
addressed here. For example, the definition of "consistent" does not
seem sufficient to guarantee SC for some reasonable (non-controversial?)
classes of programs. I assume you want
T1: if (A==1) B=1; 
T2: if (B==1) A=1
to be considered as data-race-free and so appear SC (initially A, B are
0 and neither is atomic). However, I don't see anything in the
consistency definition that will preclude both T1 and T2 reading 1 and
writing 1. This has nothing to do with any definition of happens-before
since SC executions of this program do not have any conflicting
accesses. 

There are other issues, but may be moot in case I am misunderstanding
your intent for the above. Perhaps it will be easier to talk on the
phone since this has come up a few times?

(2) Has someone verified from IBM architects that Peter Dimov's
fetch_add example actually works with PPC? Otherwise, that's a lot of
complexity in the new synchronizes-with definition for no return. Sorry
to not have got back to you and others on this aspect earlier, but I am
not sure the current modification is the best one for this (need IBM's
answer before further discussion on this).

Sarita


> -----Original Message-----
> From: Boehm, Hans [mailto:hans.boehm at hp.com] 
> Sent: Thursday, June 21, 2007 9:23 PM
> To: C++ threads standardisation
> Cc: Sarita V Adve
> Subject: RE: [cpp-threads] Slightly revised memory model 
> proposal (D2300)
> 
> Here are the latest revisions of:
> 
> The D2300 memory model.  I sort of followed Lawrence's semi-suggestion
> and included sc stores (not loads) with RMW operations in defining
> synchronizes with.  I also cleaned up the discussion of race-free
> executions in a way that I think is necessary, but may 
> require Clark to
> clean up after my standardese again.
> 
> Some text (mm_rules) to be included in the atomics proposal to explain
> how it meshes with the memory model.
> 
> The sequential consistency proof updated to reflect the memory model
> revisions, and hopefully fixing some other issues.
> 
> Further bug reports would be appreciated.  The C++ paper deadline is
> officially tomorrow.
> 
> Hans
>