An attempt at a stronger version of SC- that forbids the outcomes of tests 5
and 10 is at
http://www.cs.uiuc.edu/~sadve/jmm/stronger-sc-almost-one-page.pdf. I'll
appreciate your comments.
Here is the intuition and the change from the weaker SC-. The following
motivational text is long, but the actual addition to the formal document is
just 7 lines.
For reference, I repeat test 10 below:
Initially, x = y = z = 0
Thread 1:
r1 = x
if (r1 == 1)
y = 1
Thread 2
r2 = y
if (r2 == 1)
x = 1
Thread 3
z = 1
Thread 4
r3 = z
if (r3 == 1)
x = 1
Behavior in question: r1 == r2 == 1, r3 == 0.
Recall that an execution E obeys SC- if we can validate all reads in E. To
validate a read R, we have to show the existence of a "well-behaved"
execution, say Ev. A key property for Ev is that if R returns the value of
write W in E, then **W should occur in Ev** (it should also be hb-consistent
for R in Ev, but that's not important for now).
For the stronger SC-, we require that not only should the write W occur in
Ev, but the writes that are "responsible" for making W occur in Ev should
also occur in E. For example, consider test 10 and the execution E that
allows r1==r2==1, r3==0. Let's start by trying to validate Thread 2's read
of y. This read returns the value of Thread 1's y=1 in our execution E.
There is a well-behaved (SC) execution, Ev, where this write occurs, but in
that SC execution, the write of y happens because thread 1's read of x
returns 1 from thread 4's write of x. So Thread 4's write of x is
"responsible" for thread 1's write of y, but this responsible write does not
happen in E. So in the stronger SC-, we cannot validate the read of y and
the execution is not allowed.
The key question then is how to formalize when a write is responsible for
another write. A naïve definition would trace through traditional control
and flow dependences for this purpose. This would be a simple constructive
definition, but unfortunately, prohibits optimizations such as test 3. To be
more aggressive, we resort to a more abstract definition:
We first characterize a set of reads that are responsible for a write W in
execution Ev: this is a minimal set of reads such that if those reads return
the same values as in Ev in any (legal) execution, then we are guaranteed
that W will occur in that execution. For example, in test 10, thread 1's
read of x as 1 is responsible for the write of y. That is, we know that for
any execution where that read returns 1, the write of y is guaranteed to
execute, and this is a minimal set of such reads.
Once we identify a set of responsible reads, we define responsible writes as
follows. A write Wr is resposible for a write W if (1) a read that is
responsible for W returns the value of Wr or (2) Wr is responsible for some
write Wr’ and Wr’ is responsible for W.
All of this is formalized in the document above. For those familiar with the
previous version, there are only two changes: (1) a definition for
responsible accesses and (2) a condition 3 in the definition of SC- that
writes that are responsible for W in Ev should also occur in E.
I believe the earlier proof for system optimizations is also still valid
with minor changes, but haven't done those yet.
I haven't had a chance to look at the new M/P model to see if the two
formalizations are equivalent.
There are some more minor variations possible for strengthening/weakening
the model that I am exploring, but I thought your feedback at this stage
would be very useful. I'll appreciate any comments.
Thanks,
Sarita
-----------------------------------------------------------------------
Sarita Adve
Associate Professor
University of Illinois at Urbana-Champaign Email: sadve@cs.uiuc.edu
Siebel Center for Computer Science Office: 4110 SC
201 North Goodwin Avenue Phone: 217-333-8461
Urbana, IL 61801 Fax: 217-265-6582
WWW URL: http://www.cs.uiuc.edu/~sadve
-----------------------------------------------------------------------
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT