Jeremy and I have updated the model model.
We were working through a proof that correctly synchronized programs
have only sequentially consistent semantics.
In trying to do the proof, we found some examples that showed our old
model didn't have this property. We changed a few things and we were
able to get a proof. Things that changed:
\item Consistency is now called {\it hb-consistency}.
\item Previously, we allowed a prescient read action to see a write
that occurs later in the causal order.
Now all reads must see writes that occur earlier in the causal order.
\item A write $w$ cannot occur presciently if in the justifying
execution there is a conflicting read $r$ such that $r \hb w$.
\item Prohibited sets are defined in a slightly different way.
In particular,
they are global, so that in order to justify an action $x$ in
an execution $E$, you may not prohibit $E$.
These changes don't effect any of the examples we talked about previously.
Our writeup of the proof that correctly synchronized programs have only SC
semantics is still rather cryptic. We are planning to post that Monday.
We haven't yet figured out if there is a weak version of the
semantics that allows behaviors like that in causality test case 5.
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:51 EDT