[jmm-dev] LTL specification of relaxed memory

[Doug Lea]

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