At 4:39 PM -0500 8/8/02, Sarita Adve wrote:
>Right. To eliminate potential confusion in future discussion, I want to
>clarify further:
>
>Simply saying that an execution trace is consistent with program order
>is also "content-free" if there is no other relationship between this
>total order and the values that are read.
In my terminology/description, the values seen by reads are
determined by the memory model.
>In other words, it's fine to
>say that my model has a totally ordered execution trace that is
>consistent with program order, but this statement doesn't imply
>anything. Also, it doesn't preclude talking about my model in the future
>as having a totally ordered execution trace that is not consistent with
>program order.
>
>Sarita
Yes, to summarize.
For the purposes of discussion, I describe two memory models, A and B.
The only thing significant about these models are the behaviors they
allow. I believe that all the models being considered allow behaviors
that somewhere between the behaviors allowed by A and the behaviors
allowed by B. Whether these models are specified in a manner similar
to A and B is not significant.
In both models A and B, we consider the legality of an execution
trace E of a program P. An execution trace is a totally ordered set
of actions. The actions of each thread T of E occur in the program
order of P and are consistent with intra-thread semantics of E
(excluding the values of reads, which are determined by the memory
model and not the intra-thread semantics).
There is a hb order on E, induced by unlock/lock and volatile write/read pairs.
In both A and B, the values read in E must be consistent with hb;
i.e., if R is a read that returns the value of a write W, then we
cannot have R hb
W and we cannot have a W' to the same location where W hb W' hb R in E.
In model B only, a read must see the value of a previous write.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:41 EDT