JavaMemoryModel: SC- with better line breaks :-)

From: Sarita Adve (
Date: Mon Jul 28 2003 - 16:18:36 EDT

Yikes, the message came back to me with line breaks in ugly places. Here's
the same message with better line breaks. Apologies for the clutter.


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.



JavaMemoryModel mailing list -

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