Following up my specific test cases, I'd like to suggest some general
categories of rules to guide our work on a formalism.
General rule 1:
Any execution that is not consistent with intra-thread semantics, or
in which a read sees a value that it is not allowed to see by the
happens-before ordering, is forbidden. In other words, non-consistent
executions are forbidden.
General rule 2:
If an execution is consistent, and there is a total order over all
the actions that is compatible with the happens before order and each
read sees a write that occurs previously in the total order, then the
execution is allowed. (This includes all SC executions).
General rule 3:
If all sequentially consistent executions of the program are data
race free, then the program can exhibit only sequentially consistent
executions.
Note that these general rules are not complete, but they handle the easy cases.
Thoughts?
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT