At 01:18 AM 11/12/2003 -0500, Jeremy Manson wrote:
>We could conceivably get the same behavior by saying that there is a total
>order over volatile operations but not locks. I don't think this is
>actually semantically different.
>
>It also makes our lives easier when doing proofs, but that's probably not
>as compelling to people who are not Bill and me.
At the risk of reopening an old debate at a late stage...
Clearly there are examples of programs that can detect a lack of SC. They
seem to arise where a program sets out to determine the execution order of
events whose order the program does not specify. The program asserts that x
IMPLIES y or y IMPLIES x, and discovers this to be false.
But does anyone have a example of plausible real life code with no data
races that would break in a non-SC environment?
The existing proofs would remain valid if the implementation is SC even if
the model isn't.
My concern is that SC imposes an execution cost on future implementations,
and once it's in the released model, it'll be next to impossible to remove.
If the model leaves SC out, then implementations could still be SC, pending
additional proofs about what is permissible in a non-SC environment. It's
true that programs could break later because the programmer has
unsuspectingly relied on the SC property of the implementation they're
using, but we always face that sort of problem anyway - how many
implementations avoid any consistency beyond what the model defines?
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:55 EDT