[jmm-dev] thin-air summary

[Peter Sewell]

On 18 February 2014 04:14, David Holmes <david.holmes at oracle.com> wrote:
> 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 ?

What we're showing here is that "shows that thin-air executions cannot
be forbidden by any per-candidate-execution condition **using the
C/C++11 notion of candidate executions**".  That notion (summarised in
Section 2.5 of the Batty et al. POPL11 paper
<http://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf>) is not a
trace of machine instructions, but instead a set of memory access
events together with various relations over them.  Branches don't
appear explicitly, and those relations don't include control
dependency.

> 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. :)

indeed...

Peter