Re: JavaMemoryModel: Why CnC

From: Bill Pugh (
Date: Tue Jul 29 2003 - 14:06:32 EDT

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.
>It is a preliminary draft, and is not uptodate with recent "slight
>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) ->

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.


JavaMemoryModel mailing list -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT