Bill Pugh wrote:
> At 5:38 PM -0500 6/29/01, Sarita Adve wrote:
> > >
> >> Reordering a monitorexit and a finite number of volatile reads
> >> may fall into the category of something that is illegal in the
> >> semantics, but can't be observed so is legal in the
> implementation.
> >
> >This really should not be an issue. The *semantics* should
> be specified
> >in a way that all implementations are legal. (Hence the previous
> >suggestion of giving up on per-process orderings as a way to specify
> >the semantics.)
> >
>
> Clearly, you don't want something such that all possible
> implementations are legal (e.g., implementations that ignore the
> volatile annotation and keep volatile variables in registers).
I apologize for speaking for Sarita, but I believe the original point
was about the meaning of "specification" and "implementation": a program
which purports to be an implementation but which does not conform to the
specification is not an implementation. By this definition all
implementations are legal.
> It is only illegal to violate the formal semantics in an
> implementation if you can be caught and convicted. In other words, if
> the program can exhibit a observed behavior that cannot be explained
> by the semantics, the implementation is broken. Otherwise it is
> legal, and it doesn't matter what is done under the covers.
and in an earlier message:
> 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.
This point doesn't make much sense to me. A violation which cannot be
observed does not exist. The specification only implies behaviour, i.e.
that which can be observed.
(More cynically, if you can't be caught and convicted, you didn't do it
;)
> Bill
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
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