The other side of the argument was that allowing the ordering below broke no known useful code sequences or algorithms and restrictions on future implementations should be a consideration.
- Rick
-----Original Message-----
From: owner-javamemorymodel@cs.umd.edu
[mailto:owner-javamemorymodel@cs.umd.edu]On Behalf Of Jeremy Manson
Sent: Wednesday, December 10, 2003 10:18 PM
To: javamemorymodel@cs.umd.edu
Subject: Re: JavaMemoryModel: Total orders
> OK, but then I'm left with the question of whether or not the non-existence
> of a total order could be visible to the program. If it cannot, then why is
> a total order stated to exist? On the other hand, if a lack of total order
> has detectable consequences, then my objection stands, even though my
> example doesn't.
I mentioned before that, for volatiles, there is only a happens-before
edge between a volatile write and subsequent volatile reads of the same
variable. We have the informal requirement, however, that all accesses to
volatiles be sequentially consistent.
So consider the following code, with volatile v and w:
Thread 1:
v = 1;
Thread 2
w = 1;
Thread 3
r1 = v;
r2 = w;
Thread 4
r3 = w;
r4 = v;
If we only have happens-before, we can get r1 == r3 == 1, but r2 ==
r4 == 0. This is not a legal SC result. With a total order over
synchronization actions, and the requirement that all volatile reads
see the last write in the synchronization order, this cannot happen.
That requirement for volatile reads, by the way, is at the end of Section
7.2.1, and admittedly doesn't jump out at the reader. Perhaps it should
be moved to a more prominent place?
Enforcing SC for volatiles may have an impact on implementations, but we
asked around quite a bit, and (to the best of my recollection) no one gave
us a practical argument against it on any multiprocessor in use.
We could conceivably get the same behavior by saying that there is a total
order over volatile operations but not locks. I don't think this is
actually semantically different.
It also makes our lives easier when doing proofs, but that's probably not
as compelling to people who are not Bill and me.
Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:55 EDT