[jmm-dev] LTL specification of relaxed memory

[Alan Jeffrey]

Hi everyone,

I've been messing around with proving the DRF theorem for a Mazurkeiwicz 
trace model of relaxed memory. I'm pretty close to convincing the Agda 
theorem prover that this is true, most of the time has been spent coming 
up with good definitions. I think the definitions are in a state worth 
sharing...

Recall that a Mazurkeiwicz trace model consists of an alphabet Sigma, 
with a binary "independence" relation I. This induces an equivalence ~ 
on Sigma^* given as the smallest congruence containing:

   ab ~ ba  (for any (a,b) in I)

We can define a variant of past time Linear Temporal Logic, whose 
semantics is given as subsets of Sigma^*. The usual operators of LTL are:

   epsilon not in (prev phi)
   sa in (prev phi) whenever s in phi

   epsilon in (wprev phi)
   sa in (wprev phi) whenever s in phi

   (always phi) = (phi and wprev(always phi))
   (sometime phi) = (phi or prev(sometime phi))
   (phi since psi) = (psi or (phi and prev(phi since psi))

The interesting new operator is a permutation operator:

   s in (permute phi) whenever t in phi for some s ~ t

 From permute we can define a "previous state up to permutation" as:

   (pprev phi) =
     exists(a) (a and permute((not a) since (a and prev(phi))))

unpacking this, sa in (pprev phi) whenever there is some sa ~ tau, a is 
not in u, and t is in phi.

LTL can be used to specify the relaxed memory model we're interested in 
(I think). Making use of two new binary relations on Sigma:

   C thought of as "read-write conflict"
   J thought of as "read-write justification"

the canonical example being:

   (W x=v, W x=w) in C
   (R x=v, W x=w) in C
   (W x=v, R x=w) in C
   (W x=v, R x=v) in J

The LTL spec for sequential consistency is:

   start = always false
   justified(a) = start or (not(C(a)) since J(a))
   sconsistent = always forall(a) (a implies prev(justified(a))

Unpacking this...

  * start is only true on the empty trace epsilon.
  * justified(a) is true either if a is the initial action or
    we can find a past action b which justifies a, and
    there is no action c between a and b in conflict with a.
  * sconsistent is true if every action is preceded by a justifier.

After all this, the LTL spec for relaxed consistency is:

   rconsistent = always forall(a) (a implies pprev(justified(a))

that is, the only difference between sequential consistency and relaxed 
consistency is whether we use "prev" (previous state) or "pprev" 
(previous state up to permutation). For example, the canonical trace for 
relaxed memory is:

   s = (1: W x=0) (1: W x=1) (1: W y=1) (2: R y=1) (2: R x=0)

We can double-check that s not in sconsistent (since the justifier for 
the action (2: R x=0) is (1: W x=0) but there is an intervening action 
(1: W x=1) which is conflict with (2: R x=0)). On the other hand s is in 
rconsistent, since we have:

   s ~ (1: W x=0) (2: R x=0) (1: W x=1) (1: W y=1) (2: R y=1)

and so (1: W x=0) can act as the justifier up to permutation.

Just to finish off the problem spec, we can define the DRF property as:

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

Alan.