[jmm-dev] thin-air summary

[David Holmes]

Hi Peter,

On 18/02/2014 2:45 AM, Peter Sewell wrote:
> Dear all,
>
> Mark Batty and I have written a short note trying to summarise the
> thin-air problem as crisply as we can:
>
> http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html
>
> Comments welcome, of course.   We've also been thinking here about
> possible approaches; hopefully we'll have another note about that in a
> few days.

I'm a lay-person when it comes to the formalities of all this but given:

4 Example LB+ctrl+data+ctrl-double (language must allow)

r1 = x;        // reads 42
if (r1 == 42)
   y = r1;
---------------------------
r2 = y;        // reads 42
if (r2 == 42)
   x = 42;
else
   x = 42;

the compiler optimization would elide the conditional and simply do the 
store, so this then reduces to:

r1 = x;        // reads 42
if (r1 == 42)
   y = r1;
---------------------------
r2 = y;        // reads 42
x = 42;

which, as stated, now matches "3 Example LB+ctrl+data+po". But in that 
case I don't understand how you can say that for "5 Example 
LB+ctrl+data+ctrl-single" "the candidate execution that we want to 
forbid here is identical to the execution of the previous example that 
we have to allow" - as 5 has a conditional and 4 no longer does, hence 
they are no longer the same ?

Further/similarly, it would seem based on these examples (and I realize 
that there may well be other examples that show otherwise) that the 
straw-man of prohibiting the (rf+dep) cycle would hold if you first 
reduced the code to its "minimal" form ie once 4 is reduced to 3 there 
is no cycle.

Of course I may have just shifted the problem into one of being able to 
define what a "minimal" form is. :)

David
-----

> Peter
>