Re: JavaMemoryModel: Specification

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Jul 10 2001 - 12:13:41 EDT


At 4:58 PM -0400 7/9/01, David Smiley wrote:
>I think it is worth noting that there are programs that might be deemed "not
>correctly synchronized" by your definition, but are still "correct" in the
>intent of the program (i.e. not broken or wrong). An example is the
>double-check lock idiom where the code within the double-check is
>idempotent. Another example is for caching algorithms that avoid
>synchronization in ways that would cause rare race conditions, but the
>result of such a race condition is not bad, provided that the common case is
>for the race to win the way you want it to.

"Correct" is perhaps a bad choice of words. The memory model for Java
has to cover the semantics of all programs, including buggy and
malicious programs.

A more appropriate term, although much more clumsy, would be "In the
simple model". In other words, we can describe a set of properties
that, if true, means that your program is "in the simple model", and
can be understood using sequentially consistent semantics.

These properties should not be part of the formal specification, but
rather something derived from the formal specification (and it would
be a goal of the formal spec to allow these properties to be
derived). If you tried to put these properties directly into the
formal specification, I would worry that there would be
discontinuities at the boundary between "correct" and "incorrect"
programs.

At 4:17 PM -0500 7/9/01, Sarita Adve wrote:
>Are you saying that these programs are correct based on the happens-before
>based definition that Bill gave earlier but not by the definition I gave?
>

I haven't checked closely but I think they are the same.

        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:33 EDT