RE: JavaMemoryModel: New approach to defining the Java Memory Model

From: David Holmes (dholmes@dltech.com.au)
Date: Sun Jul 21 2002 - 16:56:46 EDT


I've been pouring over the document and agree that, as it now appears, it
seems easier to understand than the old approach. However, given the
incomplete treatment of volatiles and the absence of final, I'll reserve
judgement on that. :)

You state that volatiles are dealt with as sequentially consistent at
present. I am still waiting to hear exactly how we plan to deviate from SC
for volatiles. Further, the document makes volatiles SC in isolation (as far
as I can tell) and doesn't cover orderings across volatiles, nor (more
importantly) orderings between volatile accesses and normal accesses - I had
expected to see some entries in the table in Figure 3 covering actions on
volatiles.

Your high-level definitions of Execution Trace and UniThread Semantics don't
quite make sense to me. You state that an execution trace defines a sequence
of actions that are "consistent with and ordered according to the unithread
semantics". You do not define what "consistent" means. Further, the
unithread semantics are defined as the "standard semantics for single
threaded programs and allow complete prediction of the behaviour of a
thread". It would seem to me that this precludes an execution trace from
including the typical results we would want to allow for unsynchronized
reads: the execution trace must be consistent with the unithread semantics,
but unithread semantics would never allow the effects of unsynchronized
reads, so the execution trace would not be consistent if it contained such
actions. ;-) It may be that unsynchronized reads are accounted for in the
definition of unithread semantics when it states "behaviour of the thread
based on the values seen by read actions within the thread" - if so then I
wouldn't call this "standard semantics for single threaded programs". Either
way a clarification is needed.

I actually understand the PUR :) and it seems like a neat way of describing
the unintuitive orderings that can occur. There is a typo in the second-last
paragraph of Section 2, page 3, where it states "happens-before paths from
or to r" - I'm not sure what "or" should be?

I look forward to seeing the next installment.

Cheers,
David

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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