Doug Lea wrote,
> Miles Sabin wrote,
> > It feels like you're trading on the obvious reasonableness of the
> > the much weaker property "For _every_ execution E of a program ...".
>
> This turns out to be a STRONGER property, at least in the sense that
> people/models have framed it. It takes a lot of backing up to
> explain:
I phrased it badly. Bill's original was,
Given a particular execution E of a program, create a partition of
the threads and variables in the program so that if a thread accessed
a variable in E, then the thread and variable are in the same
partition.
I _meant_ to say,
Given all possible executions of a program, create a partition of
the threads and variables in the program so that if a thread accessed
a variable in any execution E, then the thread and variable are in the
same partition.
which is much weaker as a constraint on memory models (or else I'm
hopelessly confused) ... so weak that I can't imagine a non-broken
memory model that didn't satisfy it.
> The isolation property Bill posted is our current best shot at
> characterizing this at a high enough level to be able to explore and
> discuss it.
I think that an approach along these lines is likely to be useful. But
it can be a delicate operation to try and axiomatize "reasonable" or
"intuitive" principles: for the most part my experience has been that
you either end up with impossibility results, or you end up with a
consistent theory of something which is only misleadingly related to
the original intuitions it was meant to formalize.
On reflection, I think my worry comes down to this. Bill claimed that
the isolation property allows us "to explain the behavior in E of the
threads in each partition, without having to examine the behavior or
programs for the other threads". Sounds good, but I'm not sure I
understand what it means.
For me an explanation of the behaviour of a thread is pretty much
intrinsically counter-factual: it's an explanation of why it did this
rather than that. The problem here is that the choice of a _particular_
execution E excludes this kind of explanation: I can't consider what
would have happened if things had gone otherwise by considering the
partition induced by E, because "otherwise" implies an execution
different from E, so very likely with a different induced partition.
To some extent the fact that we've chosen a particular execution means
that there isn't any explanation to do ... things turned out the way
they did, because that's how we set things up. Assuming that M/P has
the stronger isolation property we can throw some of the information
embodied in that choice away and get much of it back via the partition
induced by E, so clearly the property isn't trivial. But it's still not
clear to me that it's reasonable, in particular that it's reasonable
enough that we're forced to reject weaker models which don't satisfy
it.
Cheers,
Miles
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT