[jmm-dev] DRF theorem for event structures model of relaxed memory

[Alan Jeffrey]

Another update on where we are with modeling relaxed memory...

The DRF theorem is back! I proved the DRF theorem for the event 
structures model. Lots of gory details below.

We have an event structures model of a simple imperative programming 
language (good enough for the causality test cases).

Next up... checking that the programming language satisfies the 
preconditions of the DRF theorem, checking that the causality test cases 
have their expected behavior, and making sure we're doing the right 
thing wrt synchronization actions.

A.

DRF Theorem
-----------

 From Winskel, a prime event structure with labels Sigma is a quadruple 
(E,<=,#,l) where:

* E is a set of events
* <= is a partial order
* # is a down-closed symmetric binary relation
* l is a function from E to Sigma

We will write e in HB(d) for e < d and e in HA(d) for e > d.

An event structure is pointed when E has a least element init.

New here, a memory model alphabet is a set Sigma together with:

* An element initialize of Sigma
* A subset Sync of Sigma
* Binary relations RWJ subseteq RWC on Sigma such that
* RWC is transitive
* For any a, (initialize,a) in RWC

[The idea is that RWJ is the "read-write justification" relation, for 
example (R x=v, W x=v) in RWJ, and RWC is the "read-write conflict" 
relation, for example (R x=v, W x=w) in RWC.]

 From RWC we can define WWC and DC (data conflict):

   (a,b) in WWC whenever there exists (c,a) in RWC and (c,b) in RWC
   (a,b) in DC whenever (a,b) in RWC or (b,a) in RWC or (a,b) in WWC

A memory model event structure is a pointed event structure whose labels 
form a memory model alphabet, such that l(init) = initialize.

For any MMES, we can lift RWJ, RWC, WWC and DC from Sigma to E, for example:

   (d,e) in RWJ whenever (d,e) not in # and (l(d),l(e)) in RWJ

Define past-time LTL over E* as per usual, in particular (writing <= on 
strings for prefix order):

   epsilon in wkprev(phi) always
   se in wkprev(phi) whenever s in phi

   s in always phi whenever for all t <= s we have t in phi

   s in eventually phi whenever there exists t <= s s.t. t in phi

   s in phi since psi whenever there exists u <= s s.t. u in psi
     and for all u < t <= s we have t in phi

and one extra modality (writing <~ for non-contiguous substring order):

   s in extended(phi) whenever there exists t ~> s s.t. t in phi

For example, propositional LTL is enough to define being a configuration 
of an ES (as per Winskel though on sequences rather than sets):

   HBClosed = forall e . forall d < e . (e => eventually(d))

   ConflictFree = forall e . (e => always(not(#(e))))

   RepeatFree = forall e . (e => always(not(e)))

   Configuration = HBClosed and ConflictFree and RepeatFree

and the memory model:

   DRF = always (forall e . e => always(DC(e) => HB(e)))

   Sequential = always (forall e . exists d in RWJ(e) .
     e => wkprev(not RWC(e) since d)

   SConfiguration = Configuration and Sequential

   Relaxed = always (forall e . exists d in RWJ(e) .
     e => wkprev(not (HB(e) and HA(d) and RWC(e)) since d)

   RConfiguration = Configuration and
     extended (HBClosed and RepeatFree and Relaxed)

The idea is that a configuration is an rconfiguration (that is, allowed 
by the relaxed memory model) when it can be embedded in a <-closed, 
repeat-free (but *not* conflict-free) sequence of actions such that 
every event has a visible read-write justifier.) For example the program:

   thread 1: r=x; y=r
   thread 2: r=y; x=1

has event structure with order:

   init <= (R x=1) <= (W y=1)
   init <= (R x=0) <= (W y=0)
   init <= (R y=1) <= (W x=1)
   init <= (R y=0) <= (W x=1)

and conflict relation generated by:

   (R x=1) # (R x=0)
   (R y=1) # (R y=0)

The configuration:

   (init) (R y=1) (W x=1) (R x=1) (W x=1)

is an rconfiguration because it can be embedded in:

   (init) (R x=0) (W x=1) (R y=1) (W x=1) (R x=1) (W x=1)

which is relaxed (but note, not conflict-free as it contains (R x=0) as 
well as (R x=1)).

The model doesn't admit the canonical OOTA execution, since the program:

   thread 1: r=x; y=r
   thread 2: r=y; x=r

has event structure with order:

   init <= (R x=1) <= (W y=1)
   init <= (R x=0) <= (W y=0)
   init <= (R y=1) <= (W x=1)
   init <= (R y=0) <= (W x=0)

and conflict relation generated by:

   (R x=1) # (R x=0)
   (R y=1) # (R y=0)

but there is no extension of the configuration:

   (init) (R y=1) (W x=1) (R x=1) (W x=1)

which makes it an rconfiguration, for example the candidate:

   (init) (R x=0) (W x=0) (R y=1) (W x=1) (R x=1) (W x=1)

has an unjustified (R y=1) event.

To state the DRF theorem, we need one more thing which is the concept of 
a "read-write-enabled" event structure. Informally the idea is that if a 
program can perform (R x=1) then it can also perform (R x=0). 
Formalizing this, we define an equivalence class ~ on events such that 
if (d ~ e) then:

   (c,d) in RWC iff (c,e) in RWC
   (d,c) in RWC iff (e,c) in RWC
   (c,d) in HB  iff (c,e) in HB
   either d=e or d#e
   if d#c then either e<=c or e#c
   if e#c then either d<=c or d#c

The read-write-enabled events are the ones

   (d,e) in RWE iff there exists c~d s.t. (c,e) in RWJ

For example (R x=1, W x=0) in RWE whenever we can find (R x=0)~(R x=1) 
such that (R x=0, W x=0) in RWJ. The additional requirement it then that 
every read-write-conflict is read-write-enabled, and the DRF theorem is 
then:

   If (RWC subseteq RWE)
   and (SConfiguration subseteq DRF)
   then (RConfiguration subseteq SConfiguration)