Bill/Jeremy,
Here's a data-race-free program that I think may not appear SC with your
model, as written at the moment. Please let me know if I misunderstood
something:
K, Flag1, Flag2, Flag3 are volatile; initially all variables are 0
Thread 1
K = 1
Flag1 = 1
Thread 2
K = 2
Flag2 = 1
Thread 3
While ((Flag1 != 1) && (Flag2 != 1) {;}
If (K != 1) Flag3 = 1
If ((X == 1) || (K == 1)){
Y = 1
}
If (K == 1) Flag3 = 1
Thread 4
While ((Flag1 != 1) && (Flag2 != 1) {;}
While (Flag3 != 1) {;}
If (Y == 1) {
X = 1
}
This program is data-race-free, as reasoned next - The only possible
data races that can occur are between X and Y on Thread 3 and 4 (rest of
the accesses are volatiles). When K = 1 comes after K = 2, accesses to
Flag order Thread 3 before Thread 4, so no data races. When K = 2 comes
after K = 1, Thread 1 cannot issue Y=1 and Thread 2 cannot issue X=1 in
any SC execution. So there are no data races in any SC execution.
Therefore, the program should only give SC results; i.e., the following
result is not valid:
K = 2, X = 1, Y = 1. (So reads of X and Y in Threads 3 and 4
respectively return 1, and Thread 3's reads of K return 2.)
However, I don't see how your current model will prohibit the above
result: Thread 4's read of Y legitimately returns the value 1 in the
execution where K=1 wins. So I suppose it is allowed to return Y == 1 in
the execution where K=2 wins as well?
Did I miss something? If not, then one solution I see to this is to make
your GUIDs include all path information, so the statement Y = 1 is
distinguished depending on whether it was generated because K was 1 or
because X was 1. But I don't know the impact of such distinctions on the
rest of the model.
Comments?
Sarita
-----------------------------------------------------------------------
Sarita Adve
Associate Professor
University of Illinois at Urbana-Champaign Email: sadve@cs.uiuc.edu
Department of Computer Science Office: 3302 DCL
1304 West Springfield Avenue Phone: 217-333-8461
Urbana, IL 61801 Fax: 217-333-3501
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:41 EDT