I'm jumping in the middle, but I am away for two weeks and know time is
getting short.
Concerning "guaranteed to occur" ... versus "justified".
Since we are talking about optimizations, at an underlying level we are
talking about proof systems (logics) that are used to determine the safety
or possibility of the optimizations.
We know that these systems generally meet the criteria of Godel's
incompleteness theorem, and hence there will be true statements that cannot
be proved (read: "safe optimizations that cannot be justiied (in the given
logical system)").
In reflecting on this, I came to the conclusion that we need to be careful
to state the property we are interested in rather than the logical system
within which one proves it -- deeper analysis == stronger logical systems,
but we don't want to constrain (or demand) capabilities of the logical
system (i.e., the optimizer's analyses).
So I think we should try to get to something like this (probably not
_quite_ right, but intended to convey the direction I have in mind):
- A read or write of shared memory, or a synchronization operation, may be
omitted if it cannot affect a (visible) outcome of any thread in the
system.
We could also allow a read or write to be ADDED if it cannot affect a
visible outcome.
This does require a definition as to how a read or write can affect an
outcome.
Note that some proofs that it is legal to omit (add) a particular
read/write are harder than others, and in any interesting system, some
omissions/additions will be legal but not provable (i.e., not determined to
be legal by a particular analyzer).
-- Eliot
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT