Re: JavaMemoryModel: Way forward on JSR-133

From: Sylvia Else (sylviae@optushome.com.au)
Date: Wed Jan 14 2004 - 18:45:18 EST


Note - this message sent only to javamemorymodel@....

At 02:16 AM 15/01/2004, Bill Pugh wrote:

> So here is my proposal.
>
> I think we need to keep the current formalism for the core memory
> model. However, we will change the proposal to note that the details of
> the causality semantics come from trying to find a way of formalizing
> informal constraints, and that people should not be writing code that
> depends upon the formal causality details. It is not the intention of the
> semantics to forbid reasonable compiler or architectural optimizations
> that might, in combination, produce surprising results. If, in the
> future, we find such optimizations that lead to violations of the formal
> causality spec, the spec may be changed in future revisions of the JLS to
> accommodate them. It particular, causality test cases 5 and 10 will be
> listed as ones that are forbidden by the current formalism, but that if
> future optimizations make it desirable to allow them, and no compelling
> safety or security problem is found to result from allowing them, then it
> is likely that the JLS would be revised to allow them.

Isn't this tantamount to saying that programs with data races have no
guarantees beyond that they can't be exploited to break security?

I have previously coded data races that are of the form "Either the field
has its initial value in it, or it contains one of that values that my
program stores." I'm not sure that this reasoning stands up if the
causality model can be weakened in some as yet unspecified way in the
future. In particuarly, it might break if the out-of-thin-air rules get
weakened even futher than SC-.

Sylvia.

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT