Re: JavaMemoryModel: Implications of SC-: we need your feedback

From: Sylvia Else (sylviae@optushome.com.au)
Date: Wed Jan 07 2004 - 18:00:23 EST


At 09:10 PM 7/01/2004, Sarita Adve wrote:
>At this point, I feel that SC- has distinct advantages over the Manson/Pugh
>(M/P) model. Unfortunately, Bill, Jeremy, and I cannot come to a consensus,
>and so we need your feedback to ensure the right decision is made.

When I look at test case 5 in
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
I would be more sympathetic to its being forbidden if test case 2 was not
allowed (I'm not suggesting that test case 2 be disalllowed).

If I deliberately code a data race that is in some sense similar to test
case 5, then before I can make use of the fact that the out of thin air
result is forbidden, I have to prove that there is no chain of inferences,
of arbitrary complexity, that allows some reordering that removes the out
of thin air property.

Needless to say, I'm not going to do that, even if I trusted my skills in
this area - I'll simply write the code some other way.

So I'm inclined to agree with Sarita in that M/P is too strong. If I
understand SC-, it at least guarantees that a value will not be stored into
a memory location unless there exists some chain of events, albeit in
different executions, that lead to the value being stored. Somewhere, I
would have to have written code that very clearly created that value.

So there are degrees of out-of-thin-air-ness. M/P provides a stronger
definition of out of thin air, but not one that I as a programmer am going
to be able to make much use of.

On my present understanding of SC-, I would be happy with it, with the
caveat that I remain unconvinced, as indicated in a previous unanswered
posting, that the global total order property for race free executions is
essential.

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