[cpp-threads] Counter strawman proposal :-)

[Boehm, Hans]

After a long pause ...

Peter -

This seems to be much closer to happens-before consistency in Java
than what we have been discussing.  It no longer invokes undefined
behavior if there are races, and assumes there is an "accessed value".
Is that intentional?

With this approach

	r1 = x;
	if (r1 != (<stuff that doesn't touch r1>, r1) abort();

is guaranteed not to abort.  That means that compilers can
no longer reload registers that have been spilled with their
original values, even if they are known not to have been modified.

More comments below ...

> -----Original Message-----
> From: 
> Cpp-threads_decadentplace.org.uk-bounces at decadentplace.org.uk 
> [mailto:Cpp-threads_decadentplace.org.uk-bounces at decadentplace
> .org.uk] On Behalf Of Peter Dimov
> Sent: Sunday, June 12, 2005 6:49 AM
> To: cpp-threads
> Subject: [cpp-threads] Counter strawman proposal :-)
> 
> 
> A modification M of a scalar object is _potentially visible_ 
> to an attempt A 
> to access the stored value of that object if:
> 
> - the modification is not _shadowed by_ another modification, and
> - the modification does not _occur after_ the access.
> 
> If no modifications are _potentially visible_ at the point 
> where the value 
> is accessed, the behavior is undefined.
> 
> If two or more modifications that yield distinct values are 
> _potentially 
> visible_, the accessed value is unspecified. Note that the 
> accessed value is 
> not guaranteed to match any of the potentially visible values.

I think we want to just invoke undefined behavior here.

> 
> 
> A modification M is _shadowed by_ another modification M2 if:
> 
> - M2 _occurs after_ M, and
> - A _occurs after_ M2.
> 
> 
> An operation O1 _occurs after_ an operation O2 if:
> 
> - the two operations are done by the same thread and there 
> exists a sequence 
> point between O2 and O1, or

It would be nice if that works without explicitly modeling reads.
I have to think a bit more about this.

> 
> - O1 _synchronizes with_ O2, or
> 
> - there _exists an ordering constraint between_ O2 and O1.

Why do you separate these?
> 
> 
> There _exists an ordering constraint between_ O1 and O2 when:
> 
> - a sink-(O1 type) barrier _occurs after_ O1 in its thread, and
> - a hoist-(O2 type) barrier _occurs before_ O2 in its thread, and
> - the first barrier precedes the second barrier in the 
> program execution.

This assumes a total ordering on "barriers"?  I thought we wanted
to accommodate the fact that a release store followed by an acquire load
have no visibility ordering between them?
> 
> --
> Peter Dimov
> http://www.pdimov.com 
> 
> 
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk 
> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
entplace.org.uk