At 4:53 PM -0500 6/29/01, Sarita Adve wrote:
>For similar reason, I suggest we avoid defining the semantics in terms of
>"per-process" orderings that are imposed. Instead, we should define them in
>terms similar to the happens-before terminology Bill used earlier. Then when
>we want to interpret the semantics in terms of optimizations allowed, I
>suggest we discuss safe reorderings rather than restricted orderings. More
>concretely, I would like to suggest avoiding statements such as:
>
>> The release/acquire semantics of volatiles and locks imposed the
>> following orderings between volatile and monitor actions
>>
>> volatile read, followed by anything
>> monitor enter, followed by anything
>> anything followed by a volatile write
> > anything followed by a monitor exit
> >
There are very important distinctions between:
* The definition of the memory model
* Properties of the memory model
And also between
* The definition of the memory model
* Valid implementations of the memory model
Perhaps I should have been more clear. At the moment, I wanted to
discuss what properties we want the memory model to have. A property
of the memory model might not exist in the formal specification.
Rather, it might be something that can be deduced from the formal
specification.
For example, under our proposed formal semantics, the fact that you
can reorder a volatile write and a following (normal) read can be
deduced from the formal specification, but is not explicit in the
formal specification.
Similarly, there might be things that are forbidden in the formal
specification, but can be done in implementations because it is
impossible to observe a violation of the formal specification. For
example, I believe that reordering of a monitorexit and a finite
number of volatile reads falls into this category, although it
requires more thought.
Before we get into the process of deciding how to formalize the
semantics we want, we need to decide (informally) the properties we
want the semantics to have. Therefore, discussions of whether or not
some particular compiler optimizations is legal is an appropriate
topic of discussion at this point, although such optimizations may
not wind up in the formal specification.
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:32 EDT