[jmm-dev] LTL specification of relaxed memory
ajeffrey at bell-labs.com
Thu Feb 20 15:17:33 PST 2014
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
* 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
* 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...
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.
> 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?
More information about the jmm-dev