At 5:45 AM -0500 7/29/03, Sarita Adve wrote:
>Bill and Jeremy,
>
>Can you give us all a *full* intuitive description of consistency+causality
>please? We don't have one yet that includes the effect of prohibited reads.
>Or are you going to argue that you don't need to have prohibited reads in
>your intuitive description? I hope that is not the case.
>
OK, here is yet another attempt at a complete but informal semantics.
An execution is legal if and only if:
* The execution respects intra-thread semantics.
* Each read sees a write that it is allowed to see by the happens-before
ordering.
* There does not exist an action X such that in reasoning why X occurred,
you have to assume that X occurred. You show this by showing that X is
guaranteed to be allowed to happen, without assuming X has happened.
Prohibited executions/reads allow you to say that certain executions cannot
happen, perhaps due to compiler transformations such as redundant load
elimination. If some executions are prohibited, and X is guaranteed
to be allowed to happen in all non-prohibited executions, then X may be
considered to be guaranteed to be allowed to occur.
The only prohibited reads/executions that can be considered are ones that
restrict the writes that could be seen by a read (e.g., this read always
sees the previous write to this variable within this thread, or this read
always sees the same write as was seen by another read of this variable in
this thread).
Optional clarification:
We say "X is guaranteed to be allowed to happen", rather than saying
"X is guaranteed to happen", because if X is a data race read, you can't
guarantee which write X will see. So when we say a data race R that sees W
is guaranteed to be _allowed_ to happen, we mean that it is guaranteed that:
- the write W is guaranteed to happen
- the read R is guaranteed to happen (although we can't guarantee which
write it will see)
- it is guaranteed that R could see W (they both access the same variable
and the happens-before ordering does not prohibit R from seeing W).
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:47 EDT