JavaMemoryModel: The SC- memory model

From: Sarita Adve (
Date: Mon Nov 17 2003 - 13:34:59 EST

I continue to be concerned that the Manson/Pugh model is still too complex,
and the intuition behind some parts isn't clear. I am particularly concerned
about the forbidden executions part. Another concern is that non-intuitive
behavior (i.e., non-SC behavior) isn't clearly linked to data races. So,
even if one knows that some part of the program does not contain a data
race, one has to still potentially worry about the possibility of prescient
accesses and reason through the full model.

So for the last couple of months, I have been working on fixing up the SC-
model (from community review time), with much feedback from Bill and Jeremy.

This model does not have the complexity of forbidden executions, and
directly links non-SC behavior to a data race.

However, SC- allows the behavior in causality tests 5 and 10, while the
Manson/Pugh model forbids it. Bill, Jeremy, and I are still discussing an
explanation for why these tests should be forbidden.

The full document including the motivation for the model is at:
The document contains a one page concise definition of the model on page 9.
I have also pulled it out and it is separately available from:

I will appreciate your comments.



P.S. For those who saw my presentation of the model in Dagstuhl - this is
essentially the same, except I modified the definition of conflict order to
accommodate non-atomic writes.

Sarita Adve
Associate Professor
Department of Computer Science Email:
University of Illinois at Urbana-Champaign Office: 3302 DCL
1304 West Springfield Avenue Phone: 217-333-8461
Urbana, IL 61801-2987 Fax: 217-333-3501
                 WWW URL:

JavaMemoryModel mailing list -

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