Hi all,
I have a program that uses volatile variables and I am trying to reason
about it using the
"A program is correctly synchronized if and only if all sequentially
consistent executions are free of data races." guarantee in JLS3.
JLS3 seems to contain a glitch that prevents me from proving that my program
is free of data races. Specifically, consider a read R of a volatile
variable V and a write W of V that comes after R in the synchronization
order. JLS3 seems to consider R and W to be conflicting accesses. Moreover,
there is no happens-before edge from R to W (and rightly so). Therefore,
JLS3 seems to also consider R and W to constitute a data race. Finally, it
seems therefore that I cannot apply the abovementioned guarantee.
I assume this is an unintentional omission. I see two possible fixes:
1) Define "conflicting accesses" to apply only to non-volatile variables.
or
2) Define "data race" to apply only to conflicting accesses of non-volatile
variables.
Am I correct in this?
Thanks,-
Bart Jacobs
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:10 EDT