Here is a stripped down intuitive description of the model in my document.
The model allows reasoning with sequential consistency (SC) semantics except
for a discontinuity at each data race. I'll call this model SC-.
Recall that SC means that we can assume instructions execute one at a time,
instructions of each thread execute in program order, and a read returns the
value of the last write to the same location.
------------------------------The SC-
model---------------------------------------------
With SC-, we can assume that instructions will execute like SC (i.e., one at
a time, in program order) until we come to a memory access that could form a
data race in this SC execution (the race could be with something in the
future of this SC execution). There could be an SC-discontinuity at this
memory access:
If the access is a read:
The read may not return the value of the last write to the same
location; instead,
it could return any value that is written by some write (to the same
location) in
this SC execution (this write may happen in the future of this SC
execution).
If the access is a write:
If this write could form a race with another write in this SC
execution, then each of
these writes could deposit the values of both writes in memory. So
subsequent reads
could see the value of either write (until a later non-race write
occurs).
After this discontinuity, the execution again proceeds in an SC way -
instructions execute one at a time and in program order, with a read
returning a value from the last write to the same location - until the next
data race discontinuity.
----------------------------------------------------------------------------
-----------
This model can be fine-tuned to weaken or strengthen it further, by
weakening or strengthening the constraints on the value that the race read
can return at its discontinuity.
Comments?
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:47 EDT