[jmm-dev] LTL specification of relaxed memory

[Alan Jeffrey]

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
>
>