Reorderings with respect to fence operations


Require Import List Vbase Relations ExtraRelations actions c11 cmon reorder.
Set Implicit Arguments.

Lemma path_decomp_u1_pre :
   X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : x, rel b xrel a x),
    clos_trans X rel x y clos_refl_trans X rel x a y = b.

Lemma release_seq_u1_pre :
   mt2 lab sb rf mo a b x y
    (HB: release_seq mt2 lab (sb UNION1 (a,b)) rf mo x y)
    (NWRI: ¬ is_write (lab b))
    (DOM: x (SB: sb b x), sb a x)
    (NMO: x (MO: mo b x), False)
    (NMO': x (MO: mo x b), False),
    release_seq mt2 lab sb rf mo x y.

Lemma path_decomp_u1_post :
   X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : x, rel x arel x b),
    clos_trans X rel x y x = a clos_refl_trans X rel b y.

Lemma release_seq_u1_post :
   mt2 lab sb rf mo a b x y
    (HB: release_seq mt2 lab (sb UNION1 (a,b)) rf mo x y)
    (NWRI: ¬ is_write (lab a))
    (DOM: x (SB: sb x a), sb x b)
    (NMO: x (MO: mo a x), False)
    (NMO': x (MO: mo x a), False),
    release_seq mt2 lab sb rf mo x y.

Lemma path_decomp_u1_both :
   X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : x, rel b xrel a x)
         (DOM' : x, rel x arel x b),
    clos_trans X rel x y x = a y = b.

read(acquire) ; fence(acquire) → read(acquire) || fence(acquire)


Lemma RacqFacq_hb :
   mt2 lab (sb asw : relation actid) rf mo
    (Cmo: ConsistentMO lab mo) a b
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw b x), asw a x)
    (DOM'': x (SB: sb x a), sb x b)
    (Aa: is_acquire_read (lab a))
    (Ab: lab b = Afence (thread (lab a)) FATacq) c d
    (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo c d),
    happens_before mt2 lab sb asw rf mo c d
     c = a d = b
     happens_before mt2 lab sb asw rf mo c a d = b.

Lemma RacqFacq_acyclic :
   mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x yhappens_before mt2 lab sb asw rf mo x y rel x y)) a b
    (Aa: is_acquire_read (lab a))
    (Ab: lab b = Afence (thread (lab a)) FATacq)
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw b x), asw a x)
    (DOM'': x (SB: sb x a), sb x b)
    (NREL: z (REL: rel b z), False),
   acyclic (fun x yhappens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y rel x y).

Theorem RacqFacq_par :
   mt mt2 mtsc acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    a (Aa: is_acquire_read (lab a))
    b (Ab: lab b = Afence (thread (lab a)) FATacq)
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw b x), asw a x)
    (DOM'': x (SB: sb x a), sb x b),
     CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc
     RACE: racy mt2 lab sb asw rf moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

Corollary RacqFacq_par_paper :
   mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
    Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc
    adjacent sb a b
    adjacent asw a b
    is_acquire_read (lab a) →
    lab b = Afence (thread (lab a)) FATacq
   CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc
   RACE: racy mt2 lab sb asw rf moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

fence(release) ; write(release) → fence(release) || write(release)


Lemma FrelWrel_hb :
   mt2 lab (sb asw : relation actid) rf mo a b
    (Cmo: ConsistentMO lab mo)
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw x a), asw x b)
    (DOM'': x (SB: sb x a), sb x b)
    (Ab: is_release_write (lab b))
    (Aa: lab a = Afence (thread (lab b)) FATrel) c d
    (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo c d),
    happens_before mt2 lab sb asw rf mo c d
     c = a d = b
     c = a happens_before mt2 lab sb asw rf mo b d.

Lemma FrelWrel_acyclic :
   mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x yhappens_before mt2 lab sb asw rf mo x y rel x y))
    a b
    (Aa: lab a = Afence (thread (lab b)) FATrel)
    (Ab: is_release_write (lab b))
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw x a), asw x b)
    (DOM'': x (SB: sb x a), sb x b)
    (NREL: z (REL: rel z a), False),
   acyclic (fun x yhappens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y rel x y).

Theorem FrelWrel_par :
   mt mt2 mtsc acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc) a b
    (Aa: lab a = Afence (thread (lab b)) FATrel)
    (Ab: is_release_write (lab b))
    (DOM: x (SB: sb b x), sb a x)
    (DOM': x (SB: asw x a), asw x b)
    (DOM'': x (SB: sb x a), sb x b),
     CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc
     RACE: racy mt2 lab sb asw rf moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

Corollary FrelWrel_par_paper :
   mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
    Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc
    adjacent sb a b
    adjacent asw a b
    lab a = Afence (thread (lab b)) FATrel
    is_release_write (lab b) →
   CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc
   RACE: racy mt2 lab sb asw rf moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

This page has been generated by coqdoc