[jmm-dev] avoiding thin-air via an operational out-of-order semantics construction

[Alan Jeffrey]

Oh cool!

At first sight, there looks like this semantics and the Mazurkeiwicz 
trace semantics are pretty close. In particular, both support the 
rewrite (under appropriate restrictions of a and b_i):

   sum_i b_i . a . P_i  ==  a . sum_i b_i . P_i

though they do it by different means.

The derived LTS semantics does it by first constructing the "usual" sum, 
then allows the a action to happen because all branches of the sum can 
perform a, and so the derived LTS can peform an a action and arrive in a 
state where the a has been checked in each branch. (At least that's my 
understanding of what's going on.)

The MT semantics does it by defining prefixed sum as:

   sum_i b_i . P_i
     = { s | forall i . s in P_i }
   cup { s.b_i.t | (forall i . s in P_i) and (exists i . s.t in P_i) }

They're certainly looking very similar, whether one could formalize 
these similarities is another matter...

It looks to me that there's two styles of possible semantics, ones (like 
the derived LTS and MT approaches, and I dare say there are more) that 
don't support executions like TC1 and ones (like the current JMM and the 
Event Structures semantics) which do. The difference is whether a 
speculative write is allowed only when all branches perform the write, 
or whether it is allowed under more liberal situations (in both JMM and 
ES, based on an inductive argument which may involve conflicting events).

A.

On 03/31/2014 08:01 AM, Peter Sewell wrote:
> Dear all,
>
> building on the summary of the thin-air problem that we sent around
> earlier (http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html, Mark
> Batty+Peter Sewell),  we've sketched a semantics that gives the
> desired non-thin-air behaviour for at least some examples, for
> C11-style relaxed atomics / Linux-C ACCESS_ONCE accesses / Java
> volatiles.   At present it only covers reorderings, not eliminations
> and introductions, though we think it can probably be extended to
> those.
>
> The basic idea is to assume that compilers do not do inter-thread
> value range optimisations, using that to let us construct a
> thread-local out-of-order operational semantics out of a conventional
> thread-local (value-passing) labelled transition system. We then
> combine the resulting thread semantics with an operational
> non-multi-copy-atomic storage subsystem, as in our PLDI11 Power model,
> to be sound w.r.t. Power and ARM hardware.  The result is (we think)
> attractively simple to understand.   The big question is whether that
> assumption is reasonable (or can be made so),  and we'd welcome
> thoughts on that.
>
> The semantics is described here:
>
> http://www.cl.cam.ac.uk/~pes20/cpp/notes44.html  (Jean Pichon + Peter Sewell)
>
> (we've also got a formal version in Lem and a command-line prototype
> tool for exploring it).
>
> Comments would be very welcome
>
> Jean + Peter
>