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

[Doug Lea]

On 03/26/2014 01:41 PM, Alan Jeffrey wrote:
> Another update on where we are with modeling relaxed memory...

A couple of questions about decoding it ...

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

("Sync" is not used below? I can guess intent, but it would
be more comforting to know.)

> * 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):

Is there a good tutorial reference on the "per usual" techniques?

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

My reading was that this ("weak previous"?) allows binary relations
to apply to the first event, by giving it an artificial empty predecessor?
But I'm not so sure because I can't decode its use in "Relaxed" below.

>
>    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)
>