Bill sent a list of design goals for the memory model specification in his
first email. I'd like to suggest adding two more goals to that list:
*** Data-race-free programs should be guaranteed sequentially consistent
results. (Whether a program is data-race-free should be determined by its
behavior on a sequentially consistent machine.) This is a bound on how weak
the model can be.
*** The new specification should not impose "excessive" ordering constraints
on current hardware. This means that any constraints not necessary to ensure
SC for data-race-free programs should be imposed with "care and
deliberation." This is a bound on how strong the model can be.
If we agree with the above, then I'd like to argue next that the alternative
memory model suggested in Bill's Java Grande paper (I think this is the only
alternative on the table so far) misses some of the above, and suggest some
fixes:
****************************************************************************
(1) Model is too weak: needs control dependence orderings
****************************************************************************
The alternative model does not impose any orderings for control dependences.
Consider the following example:
Initially A = B = 0
Processor 1 Processor 2
if (A == 1) if (B == 1)
B = 1 A = 1
Result: Both processors return 1 for their reads
This execution is not possible on a sequentially consistent system, but I
think it is possible with the alternative model. Note that the program is
data-race-free - there cannot be a race on any sequentially consistent
machine.
Fix: A minimal fix is quite complex, and I'll leave that for later. A more
conservative, but simpler, fix is to impose an ordering from a read to a
write if the write is "control dependent" on the read.
****************************************************************************
(2) Model is too weak: needs ordering from a read to an unlock (condition 3
only orders writes and unlocks)
****************************************************************************
Processor 1 Processor 2
synchronized(X){ synchronized(X){
... = A ... = B
B = 1 A = 2
} }
Result: Processor 1 returns 2 for A, Proc 2 returns 1 for B
I believe this result is allowed for the alternative model, but wouldn't
occur on a SC machine.
Fix: If A is before B in program order, A is a *read* or write, B is an
unlock, then impose ordering from A to B.
****************************************************************************
(3) Model is too strong: condition 2 should not order "memory op --> lock"
****************************************************************************
This condition is not needed to ensure SC for data-race-free programs. Is
there an example for why it is needed?
****************************************************************************
(4) Model is too strong: condition 3 should not order "unlock --> write"
****************************************************************************
Comment similar to that for (3). I guess the only need so far for this
constraint has been as part of one solution for the constructor safety
issue.
****************************************************************************
(5) Miscellaneous comments:
****************************************************************************
- Depending on how everything else works out, condition 4 in the paper may
need to be changed a little.
- I have relatively minor quibbles about terminology (e.g., locks/unlocks)
and formalism used, but that can be sorted out once we converge on the order
constraints.
- Depending on how everything else works out, we may need to impose
orderings between lock/unlock (or whatever we end up calling them) actions.
Comments?
Sarita
-----------------------------------------------------------------------
Prof. Sarita Adve
Dept. of Electrical Engg. - MS 366 Office: 3029 Duncan Hall
Rice University E-mail: sarita@rice.edu
6100 Main Street Phone : 713-737-5686
Houston, TX 77005 Fax : 713-737-6196
WWW: http://www-ece.rice.edu/~sarita
-----------------------------------------------------------------------
-------------------------------
This is the JavaMemoryModel mailing list, managed by Majordomo 1.94.4.
To send a message to the list, email JavaMemoryModel@cs.umd.edu
To send a request to the list, email majordomo@cs.umd.edu and put
your request in the body of the message (use the request "help" for help).
For more information, visit http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:13 EDT