[jmm-dev] LTL specification of relaxed memory

[Alan Jeffrey]

As promised, I now have a proof of the DRF theorem using the LTL 
formulation of DRF and relaxed consistency. The proof has gone through 
the Agda proof checker.

I needed an auxiliary definition, of "compatible action". Define:

   b is compatible with a whenever
     (a I c) implies (b I c) for any c and
     (a C c) implies (b C c) for any c

Note that if b is compatible with a and sa has a data race, then sb has 
a data race.

The requirements on I, J and C are pretty tame:

  * I is symmetric and irreflexive
  * C is symmetric
  * if b in J(a) and c in C(a) then c in C(b)

The result is that for any set of traces S which satisfies the following 
conditions:

  * S is prefix-closed (that is if sa in S then s in S)
  * S is justification-enabled (that is if sa in S
    then sb in S for some b compatible with a
    and b is justified by s)
  * S is DRF (that is any sequentially consistent s has no data race)
  * S is relaxed consistent

we have:

  * S is sequentially consistent

Note that there is no notion of commitment or having to use multiple 
executions for justification.

The next step is to check this definition against the torture test...

A.


On 02/20/2014 09:34 AM, Alan Jeffrey wrote:
> Locking, volatiles, etc. should be treated by the independence and
> justification relations. For example a simple model of locks would be
> something like:
>
>    (m: (un)lock p) I (n: (un)lock q)   when m != n and p != q
>    (m: (un)lock p) I (n: R/W x=v)      when m != n
>    (m: lock p)     J (n: unlock p)
>    (m: unlock p)   J (n: lock p)
>    (init)          J (n: lock p)
>
> I'm hoping that there's a separation of concerns here, where the DRF
> theorem can be proved for any suitable I, J and C, and that a variety of
> memory models can be investigated by varying I, J and C.
>
> A.
>
> On 02/19/2014 06:56 PM, Doug Lea wrote:
>> On 02/19/2014 03:07 PM, Alan Jeffrey wrote:
>>
>>>    datarace = sometime exists(a) (a and pprev(C(a)))
>>>    drf = sconsistent implies not datarace
>>>
>>> so the problem is find conditions on P such that if [P implies drf]
>>> and [P
>>> implies rconsistent] then [P implies sconsistent].
>>>
>>
>> Where, as a first step, the conditions amount to some representation
>> of lock-based access?
>>
>> -Doug
>>
>>