At 11:02 AM 07/26/2002, Bill Pugh wrote:
>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.
I'm still having a lot of trouble understanding validation of PUR's. If
each PUR needs to be validated by some other execution without the PUR,
then it seems the validating execution shows that the behavior is allowed
and we don't need the execution with the PUR.
Could you give an example where PUR's give some behavior that wouldn't
otherwise be allowed?
>>* 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
>-------------------------------
>JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
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