Re: JavaMemoryModel: Examples similar to tests 5 and 10

From: Victor Luchangco (Victor.Luchangco@sun.com)
Date: Sun Jan 25 2004 - 09:27:52 EST


Hi folks,

A couple of weeks ago, I said

> I also think "conceptual integrity" is important, but neither
> SC- nor M/P has, in my opinion, the clear upper hand"

I was speaking then about the SC- definition from Nov 17. I had missed
the Jan 7 revision, which eliminated many of the difficulties I had with
the November definition. (Indeed, the Jan defn of SC- is quite similar
to the pre-Nov SC-, which had great conceptual simplicity.) Of course,
"conceptual simplicity" is largely in the eye of the beholder, but I
want to correct any false aspersions I cast on the Jan SC- definition.

I would also like to thank Bill for his recent example (from last
weekend) showing an execution in which a seemingly local object
"escapes" without having been "published". I too find this example
quite disturbing; it is the first example I've seen that really
seems like something we *might* want to prohibit. However, on
closer examination, I find some of the test cases in the list
available from the JMM website are similarly disturbing to me
(thanks to Slyvia and Sarita for calling attention to these
similarities). Test case 18 (and 20), in particular, seem to exhibit
basically the same property. Here it is again, for convenience:

Initially, x = y = 0

Thread 1:
r3 = x
if (r3 == 0)
  x = 42 // imagine "42" is a reference allocated by T1 immediately
r1 = x // before this code
y = r1

Thread 2:
r2 = y
x = r2

Behavior in question: r1 == r2 == r3 == 42

There are, of course, differences between this example and the one Bill
gave last week. However, on the issue of publishing local objects, it
seems to me they are equally bad.

What is difficult in assessing these models is that we don't have a
rigorous specification of what is required for "safety and security",
and I'm increasingly less convinced that "causality" is the only
requirement, or even the main one. I suggest that the problem with
the example Bill gave (and many of the others we wish to prohibit,
including the standard "out-of-thin-air" example, which is Causality
Test Case 4 in the list of test cases) is that it violates a form of
"privacy": One thread sees a value that only another thread should
be able to see. A side benefit of thinking about "privacy" rather
than "causality" is that it will probably fit in better, I believe,
with future attempts to prove "security". Obviously, this idea is
only half-baked, but I believe it would not be difficult to add such
a notion to SC-. I'm less confident about adding it to M/P because
that model is more complex and I understand it less well.

                                Victor

-------------------------------
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