[jmm-dev] State of play with modeling relaxed memory

[Alan Jeffrey]

Ah yes, I owe the world a status report...

I looked into modeling relaxed memory using Mazurkeiwicz traces, that is 
strings of actions up to appropriate reorderings. My main result here is 
negative, in that you can build a model of memory, and get it to support 
speculative write, in that:

               r=x; y=1  ==  y=1; r=x
   if(b){y=1;}else{y=1;} == y=1

The justification for speculative write is:

   sum_i a_i . b . P  ==  b . sum_i a_i . P

when b is independent of every a_i. The problem with this model is that 
it only supports a speculative write w when every branch performs w. In 
particular, it doesn't support causality test case 1:

   thread 1: r1 = x; if (r1 >= 0) { y = 1; }
   thread 2: r2 = y; x = r2;

The trace semantics of thread 1 is:

   P = sum_v (R x=v) . P_v

where

   P_+n = (W y=1)
   P_-n = 0

Since some P_v doesn't perform (W y=1), P can't perform (W y=1) before 
(R x=v).

So, assuming that TC1 (and similar examples) still stands, I don't see 
how to get a Mazurkeiwicz trace model to fly.

However, the diversion into traces was not a waste of time, as it got me 
to formulate memory properties using LTL, which is still useful no 
matter what the underlying model is.

James and I are now back to looking at event structures. We have 
variants of the previous LTL specifications of sequential consistency 
and relaxed consistency, and we're hoping to have the semantics of an 
concurrent imperative language, with a notion of program refinement 
which will support compiler optimizations such as variable reordering.

Alan.

On 03/11/2014 07:08 PM, Doug Lea wrote:
>
> Paul is probably busy arguing with Linus, or else he'd mention
> that you can now get the online first edition of his
> Is Parallel Programming Hard, And, If So, What Can You Do About It?
> at
> https://www.kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.html?release
>
> ... including sections on barriers, and everything there is
> to know (and more!) about RCU.
>
> While I'm at it, on jmm-dev non-news fronts:
> I know of or have heard rumors about people working
> on various model formulations.
> Postings on progress or updates would be welcome.
> I'll send some reminders of other pending issues over the
> next week or so.
>
> -Doug
>
>
>