I have encoded a core subset of the community draft in the logic of the
Isabelle theorem prover. This might help some people in testing their
understanding of the model (by which I do not mean to imply that my
understanding is very good). The theory document is at:
http://www.cs.kuleuven.ac.be/~bartj/javamemorymodel/JavaMemoryModel.thy
Error reports would be welcome.
I have some remarks on Appendix A:
- Is it necessary to separately mention $so$ (the synchronization order) in an
execution? Is $so$ not implied by $hb$?
- In Figure 20:
- Should $E'_p$ not be restricted to be in $J - P$? Also, since $E'_p$ is
not prohibited, is it not better to drop the subscript?
- Should the components of $E'_p$ not all be primed, as in $S'_p$, $so'_p$,
etc.? Surely they are not necessarily equal to the components of $E_p$?
- It says $\alpha <= \alpha'\beta'$. I suppose this is equivalent to $\alpha
<= \alpha'$?
- In the definition of J: $so$ should be $so'$.
- "$r_p$ and $r'_p$ observe different values" might be more appropriate
than "$r_p$ and $r'_p$ observe different writes", since the reads occur in
different executions and therefore the term "different write" is not
necessarily well-defined.
I think it might benefit the text if some kind of rationale was given for:
1) the caveat "that x may see different values..."
This is surprising. I thought the purpose of causality was to justify the
specific value seen by x.
2) the fact that only a prefix of a causal order needs to be justified.
Does this not mean that any causal order is okay since the empty prefix is
always justified?
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT