RE: JavaMemoryModel: Isolation properties in the JMM

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Sun Feb 08 2004 - 00:23:18 EST


I thought the following observations on the "isolation property" may be of
interest, in addition to Miles' and Sylvia's messages.

(1) Bill and I have discussed before that we should be able to handle
control and data dependences uniformly. We can view tests 5 and 10 as the
data and control dependence versions of the same situation. It seems that
the isolation property applies to test 10 but not test 5. So it seems
unsatisfactory to use this property to justify prohibiting test 10 since the
property doesn't show why test 5 should be prohibited. (Note that I'm not
debating here whether the property is useful, but observing that this
doesn't seem to be the key behind the debate around tests 5 and 10.)

(2) The following similar (but not identical) property was proposed a few
months ago to justify prohibiting tests 5 and 10 (see
http://www.cs.umd.edu/~pugh/java/memoryModel/archive/1528.html):

   In order to understand how a particular execution happened, it should
   suffice to examine the code that did happen. You shouldn't have
   to examine whether some code that you know didn't execute might
   form a race with the code that did execute.

It was later found that test 6 violated this property. Since we couldn't
afford to prohibit test 6, we were forced to live without this property.
Given that this and some other very intuitive sounding properties are not
upheld, it isn't clear that the new isolation property must be required to
be upheld.

Sarita

> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Sylvia Else
> Sent: Friday, February 06, 2004 7:29 AM
> To: javamemorymodel@cs.umd.edu
> Subject: Re: JavaMemoryModel: Isolation properties in the JMM
>
>
> At 05:00 AM 6/02/2004, Bill Pugh wrote:
>
> >The idea of the isolation property is for threads not in the same
> >partition, you only need to examine their behavior in this execution
> >enough to determine that they are not in the same partition.
> >
> >Without this property, you may have to consider all
> potential behaviors of
> >all threads, including threads that weren't even created in
> the execution
> >you are trying to understand.
>
> Yet as a developer, I tend not to want to understand
> executions, so much as
> predict them. I rather question the utility of the partioning
> scheme you
> described, or its associated isolation property. I note,
> though, that it
> appears that SC- cannot be partitioned this way.
>
> Even your partitioning model has the characteristic that
> modifications to
> the program that on the fact of it shouldn't affect the isolation
> nevertheless bring threads previous separately partitioned into one
> partition. An example is where both threads are modified to
> make reads of a
> common variable.
>
> Both models could be partitioned statically, and a static
> partitioning has
> more scope for being used predictively.
>
> Sylvia.
>
> -------------------------------
> 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:57 EDT