[jmm-dev] LTL specification of relaxed memory

Doug Lea dl at cs.oswego.edu
Wed Feb 19 16:56:35 PST 2014

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?


More information about the jmm-dev mailing list