At 11:09 AM +0200 7/30/03, Assaf Schuster wrote:
>This is in regard to several of the mails submitted recently in this list,
>e.g., Victor wants to see intra-thread semantics,
>and Sarita wants to see intuition to prohibited reads.
>
>We believe that the true origin for Causality is in intra-thread semantics.
>We thus have been working on a "software-oriented" approach that
>attempts to remove the need for prohibited reads by spelling out
>intra-thread semantics.
>
>The result is a "CnC-compliant" definition w/o prohibited reads.
>
>http://www.cs.technion.ac.il/~assaf/jmm/softnop.pdf
>
>It is a preliminary draft, and is not uptodate with recent "slight
>modifications"
>that might have appeared in the last few days (hours?), but it gives you the
>basic direction.
>
>We will be happy to hear any comments.
>
>---- Assaf
>
Jeremy and I did a quick read through of the paper and found a fairly
fundamental problem. The MM in the Assaf's paper is stronger than
CnC, in that it prohibits executions that the CnC model allows.
Consider the following example:
Initially, x = y = 0
Thread 1:
(1) r1 = x
(2) if r1 >= 0
(3) y = 1
Thread 2:
(4) r2 = y
(5) x = r2
Is execution r1 = r2 = 1 legal?
We have vt orderings: (3) -> (4) and (5) -> (1).
Although your definition of ito order is not entirely formal, I
believe it is fairly clear that we have ito: (1) -> (3) and (4) ->
(5).
Which gives us an eo cycle, and the execution is illegal according to
your model. I don't believe that any form of intra-thread analysis or
transformation would be allowed to reorder (1) and (3) and still
allow r1 to be 1, so the ito edge (1) -> (3) seems fairly hard.
However, a compiler should be allowed to perform a interthread
type/range based analysis that determines that all writes to x and y
are non-negative integers. This would allow transformation of r1 >= 0
to true, and allow (3) to be moved before (1), allowing r1 = r2 = 1.
In our model, we use the causal order 3 4 5 1 2. The only prescient
action is (3) y = 1. This has an empty prefix in the causal order, so
you need to show that in all executions without prescient actions,
the write (3) y = 1 occurs. This is true, so the causal order is
valid, and the execution is legal in our model.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT