JavaMemoryModel: Mechanization of core memory model

From: Bart Jacobs (
Date: Wed Aug 06 2003 - 13:30:14 EDT

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:

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 -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT