At 2:57 PM -0600 7/25/02, Yue Yang wrote:
>* Reordering Lock->ReadNormal
>
>I understand that figure 3 was not exhaustive. The following observation
>addresses the "completeness" aspect in case it might be overlooked by some
>people.
>
>Since operations are only synchronized through the same lock, thread local
>or nested locks have no effects and can be removed. Therefore, a later
>write instruction should not be "blocked" by such "redundant" locks. As a
>result, the entry for Lock->ReadNormal (and similarly,
>ReadVolatile->ReadNormal) should be conditional depending on whether the
>lock is redundant. For any implementations, a global analysis is needed to
>take the full advantage of the relaxations allowed by the spec.
In particularly, you can note that thread-local and nested locks
induces only redundant happens-before edges, and thus have no effects
and can be eliminated.
>
>* Validating PUR vs. Specifying bypassing policy
>
>It seems to me that the mechanism of validating PUR using a valid
>execution trace is not as intuitive as specifying the memory model
>directly with a bypassing table similar to Table 3. Because it is really
>hard to reason if a trace is legal when it relies on the validity of
>another possible trace. I would like to suggest using the reordering table
>as part of the spec. People can then reason about all the interleaving
>based on that. This is probably going to be a major shift in the
>notation. But as demonstrated by our UMM framework, this is quite
>elegant. (For those of you who are not aware of our work on UMM, please
>check our web site at http://www.cs.utah.edu/~yyang/research.)
I don't believe that enumerating a reordering table is a good way to
define a memory model. I don't think you can accurately capture all
of the cases you want in an elegant way.
PURs are not intended to be intuitive, in the sense that I expect
more than a handful of people to depend on understanding it. Most
people will use a reordering table. But PURs provide a good
foundation that will allow the serious memory model hacker to
discover new allowed reorderings.
>
>* Non-operational vs. operational spec
>
>You mentioned that you've moved away from an operational model. I think
>both styles have their merits. Non-operational specs, if done properly,
>might be more concise and easy to understand at the high level. An
>operational spec, especially for those based on guarded commands, might be
>more precise and easier to be verified. And it doesn't necessarily have
>to be more complicated. So at least an alternative operational spec can be
>used as a useful companion for system designers and programmers.
>
You don't want to have two specs. It just creates confusion and conflict.
Although the spec isn't an operational spec, it can be easily
implemented. We are adapting our previous simulator (which still uses
allWrites, previous and overwritten internally). The main change is
to replace initWrites with PURs, and handle the automatic generation
and validation of PURs.
Bill
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT