[cpp-threads] Another strawman memory model proposal

[Boehm, Hans]

I don't quite understand where this is going.

My current understanding of sequence points (thanks to your help)
is basically:

The statement "There is a sequence point between A and B"
really means:

"The set of acceptable sequential executions is hereby restricted
so that all actions in A appear to this thread to execute before
all actions in B.  The same applies to side effects as observed
by a synchronous outside observer"

Note that this statement is not symmetric in A and B.

When 1.9/7 talks about previous and subsequent evaluations, it is
referring only to those that are explicitly ordered with respect to
the sequence point by one of the statements of the above form.  In
particular, there are likely to be many evaluations that are neither
"previous" nor "subsequent".

Sequence points in the standard order all evaluations of subexpressions
of an expression A with respect to all subevaluations of an expression
B.

Does that sound right?

If we can figure out a way to leverage this to define a sequentially
consistent execution, that would be great.  (I'm not yet sure that
we want to talk about sequential consistency in the final version of 
the standard.  But I suspect that if we can't define that, we're
sunk.)

I think that unavoidably means adding reads to the discussion of
sequence
points.  Consider 

Thread 1:
lock(l); x = ...; unlock(l)

2 options for thread 2:
Thread 2a:
f((lock(l), 17), x, (unlock(l), 42));

Thread 2b:
g((lock(l), r1 = x, unlock(l), r1));

There is a race between Thread 1 and Thread 2a.  There is no
race between Thread 1 and Thread 2b.  We need to capture that
difference, since we want the first case, but not the second,
to exhibit undefined behavior.

Informally, the code in Thread 2a is wrong, because the read
of non-volatile x isn't constrained to occur between the
lock and unlock operations.  We need to have some way of expressing
that formally.

I think it remains critical that we leave the semantics of
programs that use ordinary variables in data races explicitly
undefined.  Moving to something like the Java model imposes
too many optimization constraints

I am actually happy to postpone some of the specification issues
for now.  It would be useful to have a better consensus of what
atomic memory operations we want to specify first.  And then, in
my mind, it may or may not make sense to give as simple a
specification for the lock-based core as possible, and to specify
the atomic operations separately off to the side.  I think
the current model works for the lock-based core, though it may
not say what we want.  It doesn't work if we add barrier-less
CAS or the like.

> >>> - There is a sequence point between unlock on a mutex and a 
> >>> subsequent lock on the same mutex.

You're adding a cross-thread ordering constraint here, presumably,
which orders a synchronization operation in one thread with respect
to that in another.  And which way they get ordered, depends
on the synchronization order, i.e. the order in which synchronization
operations occur in the execution.

By combining this with the intra-thread evaluation order, you get
something very similar to the happens-before relation in the Java
model (and elsewhere).  You still need to add read operations
to the model for any of this to work.

I think the term "sequence point" here is increasingly misleading,
since you are really defining an ordering.  Unlike in the single
threaded case, it's no longer syntactically obvious which subexpressions
come first, i.e. are on one side vs. the other.  The "happens-before"
terminology seems clearer to me, though we may want to
revert to "sequence points" to minimize textual changes to the
standard.

Hans

> -----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: Monday, May 09, 2005 5:04 AM
> To: cpp-threads at decadentplace.org.uk
> Subject: Re: [cpp-threads] Another strawman memory model proposal
> 
> 
> >>> - There is a sequence point between unlock on a mutex and a 
> >>> subsequent lock on the same mutex.
> >>>
> >>> - 1.9/8 does not apply to functions that are executed in 
> a separate 
> >>> thread. There is no sequence point between the end of 
> such function 
> >>> and the evaluation of expressions outside this function.
> >>>
> >>> - There is a sequence point between the end of a function 
> executed 
> >>> in a separate thread and a join action or a successful try_join 
> >>> action on that thread.
> 
> [atomics omitted]
> 
> Forget it. The abstract machine is sequentially consistent; 
> atomics aren't 
> expressible without surgery. pthread_rwlock_rdlock isn't expressible, 
> either.
> 
> The C++ memory model in SCNF is, in its entirety:
> 
> - 1.9/8 does not apply to functions that are executed in a 
> separate thread.
> 
> - The second sentence of 1.9/17 does not apply to functions that are 
> executed in a separate thread. 
> 
> 
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk 
> http://decadentplace.org.uk/mailman/listinfo/cpp-threads_decad
entplace.org.uk