RE: JavaMemoryModel: Legal implementations

From: William Pugh (pugh@cs.umd.edu)
Date: Fri Jul 06 2001 - 13:30:33 EDT


At 4:57 PM +0100 7/6/01, Roly Perera wrote:
> > 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
>;)

For example, the specification might say that you cannot reorder two
volatile writes. However, an implementation might be able to prove
that the reordering would not be observable (perhaps because one of
the volatiles is thread local). So it is legal for an implementation
to perform that reordering, even though the formal spec says it is
illegal.

Said another way, the specification constrains the observed behavior
of the system, not the implementation.

        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