"Roach motel" reorderings

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

We say that two actions a and b are adjacent according to a relation rel if

every action directly reachable from b is directly reachable from a;
every action directly reachable from a, except for b, is also directly reachable by b ;
every action that reaches a directly can also reach b directly; and
every action that reaches b directly, except for a, can also reach a directly.

Note that adjacent actions are not necessarily related by rel.

Definition adjacent (rel: relation actid) (a b: actid) :=
  << LA_ac : forall c, rel b c -> rel a c >> /\
  << LA_ca : forall c, rel c b -> c <> a -> rel c a >> /\
  << LA_cb : forall c, rel c a -> rel c b >> /\
  << LA_bc : forall c, rel a c -> c <> b -> rel b c >>.

A weaker notion of adjacency, that drops conditions (ii) and (iv) from the previous definition.

Definition adjacentW (rel: relation actid) (a b: actid) :=
<< LA_ac : forall c, rel b c -> rel a c >> /\
<< LA_cb : forall c, rel c a -> rel c b >>.

An even weaker notion that uses clos_trans _ rel instead of rel in the conclusion.

Definition adjacentWW (rel: relation actid) (a b: actid) :=
  << LA_ac : forall c, rel b c -> clos_trans _ rel a c >> /\
  << LA_cb : forall c, rel c a -> clos_trans _ rel c b >>.

Ltac unfolds :=
  repeat match goal with |- context [?x] => unfold x end.

Lemma adjacent_weaken rel a b :
  adjacent rel a b -> adjacentW rel a b.
Proof. unfolds; intuition. Qed.

Lemma adjacentW_weaken rel a b :
  adjacentW rel a b -> adjacentWW rel a b.
Proof. unfolds; intuition. Qed.

Definition has_loc a :=
  match a with
    | Aalloc _ _ _
    | Aload _ _ _ _
    | Astore _ _ _ _
    | Armw _ _ _ _ _ => true
    | _ => false
  end.

Notation same_loc a b :=
  (<< SL_A : has_loc a >> /\
   << SL_B : has_loc b >> /\
   << SL_Eq: loc a = loc b >>).

Two distinct actions a and b are reorderable if

they belong to the same thread,
they do not access the same location,
a is not an acquire access or fence,
b is not a release access or fence,
if the model type mt is MThbUrfnaAcyclic or MThbUrfAcyclic, and a is a read, then b is not a write,
if a is a release fence, then b is not an atomic write,
if b is an acquire fence, then a is not an atomic read, and
a and b are not both SC actions.

Definition admissible_reordering mt acts lab (a b: actid) :=
  << AR_Neq: a <> b >> /\
  << AR_In_a: In a acts >> /\
  << AR_In_b: In b acts >> /\
  << AR_ST: thread (lab a) = thread (lab b) >> /\
  << AR_SL: ~ same_loc (lab a) (lab b) >> /\
  << AR_Not_Acq_Wr: ~ is_acquire (lab a) >> /\
  << AR_Not_Rel_Ra: ~ is_release (lab b) >> /\
  << AR_Arfna_RW: mt = MThbUrfnaAcyclic ->
                  is_read (lab a) ->
                  is_write (lab b) ->
                  False >> /\
  << AR_Arf_RW: mt = MThbUrfAcyclic ->
                is_read (lab a) ->
                is_write (lab b) ->
                False >> /\
  << AR_Not_Fence_Rel_Write: is_fence (lab a) ->
                             is_release (lab a) ->
                             is_write (lab b) ->
                             ~ is_na (lab b) ->
                             False >> /\
  << AR_Not_Read_Fence_Acq: is_read (lab a) ->
                            ~ is_na (lab a) ->
                            is_fence (lab b) ->
                            is_acquire (lab b) ->
                            False >> /\
  << AR_Not_Both_Sc: ~ (is_sc (lab a) /\ is_sc (lab b)) >>.

The tactic xplit deals with all existential quantifiers and conjunctions in the goal.

Ltac xplit :=
  repeat match goal with
  | |- exists x, _ => eexists
  | |- _ /\ _ => split
  end.

Lemma Crf_Read:
  forall lab rf
         (Crf: ConsistentRF lab rf)
         a b (RF: rf a = Some b),
    is_read (lab a).
Proof.
  by ins; eapply Crf in RF; desf; eauto with access.
Qed.

Lemma Crf_Write:
  forall lab rf
         (Crf: ConsistentRF lab rf)
         a b (RF: rf a = Some b),
    is_write (lab b).
Proof.
  by ins; eapply Crf in RF; desf; eauto with access.
Qed.

Lemma Cmo_Write1:
  forall lab mo
         (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    is_write (lab a).
Proof.
  unfold ConsistentMO; ins; des; eapply CmoD in MO.
  desf; eauto with access.
Qed.

Lemma Cmo_Write2:
  forall lab mo
         (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    is_write (lab b).
Proof.
  unfold ConsistentMO; ins; des; eapply CmoD in MO.
  desf; eauto with access.
Qed.

Lemma RS_Write1:
  forall mt2 lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b
         (RS: release_seq mt2 lab sb rf mo a b)
         (Wc: is_write (lab b)),
    is_write (lab a).
Proof.
  unfold release_seq; ins; desf.
  desf; eauto using Cmo_Write1.
  induction RS; desf; eauto using Cmo_Write1, Crf_Write.
Qed.

Lemma sync_release:
  forall mt2 lab sb rf mo flag a b,
  synchronizes_with mt2 lab sb rf mo flag a b ->
  is_release (lab a).
Proof.
  intros.
  unfold synchronizes_with in *.
  des; eauto with access.
Qed.

Lemma sync_acquire:
forall mt2 lab sb rf mo flag a b,
  synchronizes_with mt2 lab sb rf mo flag a b ->
  is_acquire (lab b).
Proof.
  intros.
  unfold synchronizes_with in *.
  des; eauto with access .
Qed.

Hint Immediate sync_release sync_acquire : sync.

Lemma rf_eq_loc:
  forall lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    loc (lab a) = loc (lab b).
Proof.
  ins; eapply Crf in RF; desf.
  by destruct (lab a); destruct (lab b); inversion READ; inversion WRITE; subst; auto.
Qed.

Lemma rf_has_loc1:
  forall lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    has_loc (lab a).
Proof.
  ins; eapply Crf in RF; desf.
  by destruct (lab a); inversion WRITE; auto.
Qed.

Lemma rf_has_loc2:
  forall lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    has_loc (lab b).
Proof.
  ins; eapply Crf in RF; desf.
  by destruct (lab b); inversion READ; auto.
Qed.

Lemma rf_same_loc:
  forall lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    same_loc (lab a) (lab b).
Proof.
  ins; xplit; eauto using rf_eq_loc, rf_has_loc1, rf_has_loc2.
Qed.

Lemma mo_eq_loc:
  forall lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    loc (lab a) = loc (lab b).
Proof.
  unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
  by destruct (lab a); destruct (lab b); inversion MO; inversion MO0; subst; auto.
Qed.

Lemma mo_has_loc1:
  forall lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    has_loc (lab a).
Proof.
  unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
  by destruct (lab a); inversion MO; subst; auto.
Qed.

Lemma mo_has_loc2:
  forall lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    has_loc (lab b).
Proof.
  unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
  by destruct (lab b); inversion MO0; subst; auto.
Qed.

Lemma mo_same_loc:
  forall lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    same_loc (lab a) (lab b).
Proof.
  ins; xplit; eauto using mo_eq_loc, mo_has_loc1, mo_has_loc2.
Qed.

Hint Immediate
     rf_has_loc1 rf_has_loc2 rf_same_loc
     mo_has_loc1 mo_has_loc2 mo_same_loc : loc.

Lemma reordering_ct:
  forall rel a b (LA: adjacentWW rel a b)
             x y (Ct: clos_trans _ (rel UNION1 (a ,b )) x y),
    clos_trans _ rel x y \/ a =x /\ b =y.
Proof.
  ins; induction Ct; desf; dupdes LA; eauto using clos_trans.
    by eapply t_step_rt in IHCt2; desf; eauto using t_rt_trans.
  by eapply t_rt_step in IHCt1; desf; eauto using rt_t_trans.
Qed.

Lemma reordering_rse:
  forall lab sb
         a b (LA: adjacentWW sb a b) mt2
         x y (RSE: release_seq_elem mt2 lab (sb UNION1 (a ,b )) x y),
    release_seq_elem mt2 lab sb x y \/ a =x /\ b =y.
Proof.
  unfold release_seq_elem, same_thread; ins; desf; intuition.
  eapply reordering_ct in RSE; desf; eauto.
Qed.

Lemma reordering_st :
  forall lab sb
         a b (LA: adjacentWW sb a b) mt2
         x y (RS: same_thread mt2 lab (sb UNION1 (a ,b )) x y)
             (NEQ : x = a -> y = b -> False),
    same_thread mt2 lab sb x y.
Proof.
  unfold same_thread; ins; desf.
  by eapply reordering_ct in RS; desf; intuition.
Qed.

Lemma reordering_rs:
  forall mt acts lab sb rf mo
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2
         x y (RS: release_seq mt2 lab (sb UNION1 (a ,b )) rf mo x y),
    release_seq mt2 lab sb rf mo x y.
Proof.
  unfold release_seq; ins; desf; desf; unnw; eauto.
  right; desf; intuition.
    eapply reordering_rse in RSE; eauto.
    desf; intuition.
    dupdes Cmo; eapply CmoD in RSMO; desf.
    dupdes AR; exfalso; eapply AR_SL.
      by xplit; destruct (lab x); destruct (lab y); inversion RSMO; inversion RSMO0; eauto.
  unnw; ins.
  eapply RSO in MA; eauto.
  eapply reordering_rse in MA; eauto; desf.
  dupdes Cmo; eapply CmoD in RSMO; eapply CmoD in MB; desf.
  destruct (lab y); inversion RSMO0; inversion MB0; subst; subst.
    dupdes AR; exfalso; eapply AR_SL.
      by xplit; destruct (lab x); destruct (lab c); inversion RSMO; inversion MB; eauto.
    dupdes AR; exfalso; eapply AR_SL.
      by xplit; destruct (lab x); destruct (lab c); inversion RSMO; inversion MB; eauto.

  induction RS; vauto.
  eapply RS_thr; eauto; eapply reordering_st; eauto; ins; desf.
  dupdes Cmo; eapply CmoD in RSmo.
  dupdes AR; exfalso; eapply AR_SL.
  by destruct (lab a); destruct (lab b); ins; desf.
Qed.

Lemma reordering_sw:
  forall mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2
         x y (SW: synchronizes_with mt2 lab (sb UNION1 (a ,b )) rf mo true x y),
    synchronizes_with mt2 lab sb rf mo true x y.
Proof.
  unfold synchronizes_with; ins;
  destruct SW as [ H | SW ]; [ left | right ].
  desf; xplit; eauto using reordering_rs.
  destruct SW as [ H | SW ]; [ left | right ].
  des; unnw; intuition; eauto.
  xplit; eauto using reordering_rs.
  eapply reordering_ct in LA; eauto.
  intuition. subst.
  dupdes AR; exfalso.
    by eapply AR_Not_Read_Fence_Acq; eauto using Crf_Read, reordering_rs with access.
  destruct SW as [ H | SW ]; [ left | right ].
  des; unnw; intuition; eauto.
  xplit; eauto using reordering_rs.
  generalize LA; eapply reordering_ct in LA; eauto; intro.
  intuition. subst.
  dupdes AR; exfalso.
  eapply AR_Not_Fence_Rel_Write;
    by eauto using Crf_Write, RS_Write1, reordering_rs with access.
  des; unnw; intuition; dupdes AR; des; clarify.
  eapply reordering_ct in SBW; eauto.
  eapply reordering_ct in SBR; eauto.
  des; clarify.
  xplit; eauto using reordering_rs.
  by destruct AR_Not_Fence_Rel_Write; eauto using Crf_Write, RS_Write1, reordering_rs with access.
  by destruct AR_Not_Read_Fence_Acq; eauto using Crf_Read with access.
  by destruct AR_Not_Fence_Rel_Write; eauto using Crf_Write, RS_Write1, reordering_rs with access.
Qed.

Lemma reordering_hb_intermediate:
  forall mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2 asw
         x y (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y),
    happens_before mt2 lab sb asw rf mo x y
    \/ (x = a \/ happens_before mt2 lab sb asw rf mo x a )
       /\
       (y = b \/ happens_before mt2 lab sb asw rf mo b y ).
Proof.
  ins; induction HB; desf; eauto 6 using reordering_sw, sw_in_hb with hb.
Qed.

Lemma reordering_hb_cycle:
  forall mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2 asw
         x (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x x),
    happens_before mt2 lab sb asw rf mo x x \/
    happens_before mt2 lab sb asw rf mo b a.
Proof.
  ins.
  eapply reordering_hb_intermediate in HB; eauto.
  destruct HB as [ ? | HB ].
    by eauto.
    desf; subst; eauto using hb_trans.
    dupdes AR; intuition.
Qed.

Lemma reordering_hb_right:
  forall mt mt2 acts lab sb asw rf mo
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         x (HB: happens_before mt2 lab sb asw rf mo x a),
    happens_before mt2 lab sb asw rf mo x b.
Proof.
  ins; induction HB; eauto using hb_trans; desf.
  by dupdes LASB; eauto using t_sb_in_hb, clos_trans.
  by dupdes AR; exfalso; eauto with sync.
  by dupdes LAASW; eauto using t_asw_in_hb, clos_trans.
Qed.

Lemma reordering_hb_left:
  forall mt mt2 acts lab sb asw rf mo
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         y (HB: happens_before mt2 lab sb asw rf mo b y),
    happens_before mt2 lab sb asw rf mo a y.
Proof.
  ins; induction HB; eauto using hb_trans; desf.
  by dupdes LASB; eauto using t_sb_in_hb, clos_trans.
  by dupdes AR; exfalso; eauto with sync.
  by dupdes LAASW; eauto using t_asw_in_hb, clos_trans.
Qed.

Final reordering_hb lemma

Lemma reordering_hb:
  forall mt mt2 acts lab sb asw rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         x y (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y),
    happens_before mt2 lab sb asw rf mo x y \/ (x =a /\ y =b ).
Proof.
  ins; induction HB; desf; eauto using hb_trans, sb_in_hb, asw_in_hb.
  by left; eapply sw_in_hb, reordering_sw; eauto.
  by left; eapply reordering_hb_left; eauto.
  by left; eapply reordering_hb_right; eauto.
Qed.

Lemma hb_adjacentW:
  forall mt mt2 acts lab sb asw rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    adjacentW (happens_before mt2 lab sb asw rf mo) a b.
Proof.
  ins; unfold adjacentW; repeat split; try red; ins.
  eapply reordering_hb_left; eauto.
  eapply reordering_hb_right; eauto.
Qed.

Lemma path_decomp_three_steps:
  forall X (eq_X_dec: forall (x y: X), {x =y } + {x <>y })
         rel x y
         (XY: clos_trans X rel x y),
    rel x y \/
    (exists z, rel x z /\ rel z y ) \/
    (exists z t, z <> y /\ t <> x /\ rel x z /\ clos_trans X rel z t /\ rel t y ).
Proof.
  ins.
  eapply clos_trans_t1n in XY.
  destruct XY.
    by eauto.
    destruct (eq_X_dec y z); subst.
      by eauto.
    eapply clos_t1n_trans in XY.
    eapply clos_trans_tn1 in XY.
    destruct XY.
    by eauto.
    destruct (eq_X_dec y0 x); subst.
      by eauto.
    eapply clos_tn1_trans in XY.
    by eauto 9.
Qed.

Lemma reordering_acyclic_hb:
  forall mt mt2 acts lab sb asw rf mo
         (IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    irreflexive (happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo).
Proof.
  ins; intros x HB.
  eapply reordering_hb_cycle in HB; eauto.
  des; eauto.
  eapply path_decomp_three_steps in HB; eauto using eq_nat_dec.
  dupdes AR; dupdes LASB; dupdes LAASW.
  by des; eauto 7 with sync hb.
Qed.

Lemma hb_admissible_union:
  forall mt mt2 acts lab sb asw rf mo
         (IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo
    <--> happens_before mt2 lab sb asw rf mo UNION1 (a ,b ).
Proof.
  split; unfold inclusion; ins.
  eapply reordering_hb in H; eauto. by intuition.
  intuition; eauto using happens_before_mon_sb.
Qed.

We develop separate lemmas for the acyclity axioms.

MTorig

Lemma acyclicity_orig:
  forall mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b,
    ConsistentRF_na mt2 lab (sb UNION1 (a ,b )) asw rf mo.
Proof.
  ins; dupdes CONS; unfold ConsistentRF_na; ins.
  by eauto using happens_before_mon_sb.
Qed.

MThbUrfnaAcyclic and MThbUrfAcyclic

Lemma decomp_path_sbUrf_UNION:
  forall sb rf P a b x y
         (PATH: clos_trans actid (fun x y => (sb UNION1 (a ,b )) x y \/ rf y = Some x /\ P x y) x y),
    clos_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) x y
    \/ clos_refl_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) x a
       /\ clos_refl_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) b y.
Proof.
  ins. induction PATH.
    by desf; intuition.
    desf; intuition.
      by eauto using t_trans.
      by eauto using clos_trans_in_rt, rt_t_trans.
      by eauto using clos_trans_in_rt, t_rt_trans.
Qed.

We prove the acyclicity result parametrically with respect to any restriction of the reads from relation.

Lemma acyclicity_relUrf:
  forall mt acts lab rel rf P
         (ACYC: acyclic (fun x y => rel x y \/ rf y = Some x /\ P x y))
         (Crf: ConsistentRF lab rf)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentW rel a b)
         (ABNRW: ~ (is_read (lab a) /\ is_write (lab b))),
    acyclic (fun x y => (rel UNION1 (a ,b )) x y \/ rf y = Some x /\ P x y).
Proof.
  ins; intros x HB.
  eapply decomp_path_sbUrf_UNION in HB; desf; eauto.
  dupdes LA; dupdes Crf; dupdes AR.

  rewrite clos_refl_transE in HB; desf.

  rewrite clos_refl_transE in *; desf.
  eapply t_step_rt in HB0; des.
    by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_ac|]|]; eauto.

  rewrite clos_refl_transE in *; desf.
    by eapply Crf0 in HB0; desf; destruct (lab a); destruct (lab b); ins; desf; eauto.

  eapply t_rt_step in HB1; desf.
    by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_cb|]|];
       eauto using clos_refl_trans.

  eapply Crf0 in HB0; eapply Crf0 in HB3; desf.
  by destruct (lab a); destruct (lab b); ins; desf; eauto.

  assert (M := HB).
  eapply t_rt_step in M; desf.
  apply LA in M0.
  by eapply ACYC, t_rt_trans, HB0; eauto using rt_t_trans, t_step.
  clear M.

  rewrite clos_refl_transE in *; desf.
  eapply t_step_rt in HB; des.
    by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_ac|]|]; eauto.

  rewrite clos_refl_transE in *; desf.
    by eapply Crf in HB; desf; destruct (lab a); destruct (lab z);
       inversion READ; inversion WRITE; eauto.

  eapply t_rt_step in HB0; desf.
    by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_cb|]|];
       eauto using clos_refl_trans.

  eapply Crf0 in HB; eapply Crf0 in M0; desf.
  by destruct (lab a); destruct (lab x); inversion WRITE0; inversion READ; eauto.

  eapply t_step_rt in HB0; desf.
  apply LA_ac in HB0.
  by eapply ACYC, t_rt_trans, HB1; eauto using t_trans, t_step.

  eapply Crf in M0; eapply Crf0 in HB0; desf.
  by apply ABNRW; destruct (lab a); destruct (lab b); ins; desf.
Qed.

The two acyclity lemmas are deduced by instantiation of the parametric lemma.

Lemma acyclicity_hbUrf:
  forall mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MThbUrfAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering MThbUrfAcyclic acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y \/ rf y = Some x)
    \/ is_read (lab a) /\ is_write (lab b).
Proof.
  ins; assert ((is_read (lab a) /\ is_write (lab b)) \/ ~ (is_read (lab a) /\ is_write (lab b))).
    by destruct (lab a); destruct (lab b); simpl; intuition.
  desf; eauto.
  dupdes CONS.
  left; intros x hxx.
  eapply acyclicity_relUrf with
    (P := fun x y => True)
    (rel := happens_before mt2 lab sb asw rf mo); eauto using hb_adjacentW.
  intros t htt; eapply ACYC.
    by eapply clos_trans_monotonic; [ | eapply htt]; red; intuition.
  eapply clos_trans_monotonic; [ | eauto ].
  red; ins; desf; eauto.
  left; eapply hb_admissible_union; eauto.
Qed.

Lemma acyclicity_hbUrfna:
  forall mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MThbUrfnaAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering MThbUrfnaAcyclic acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y \/ rfna lab rf x y)
    \/ is_read (lab a) /\ is_write (lab b).
Proof.
  ins; assert ((is_read (lab a) /\ is_write (lab b)) \/ ~ (is_read (lab a) /\ is_write (lab b))).
    by destruct (lab a); destruct (lab b); simpl; intuition.
  desf; eauto.
  dupdes CONS.
  left; intros x hxx.
  eapply acyclicity_relUrf with (P := fun x y => is_na (lab x) \/ is_na (lab y)); eauto using hb_adjacentW.
  eapply clos_trans_monotonic; [ | eauto ].
  red; ins; desf; eauto.
  by left; eapply hb_admissible_union; eauto.
Qed.

We prove the main theorem of this section, that the admissible reorderings preserve semiconsistent executions and data races.

Theorem Semiconsistent_reordering :
  forall mt mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    << CONS': Semiconsistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf mo sc >> /\
    << RACE: racy mt2 lab sb asw rf mo -> racy mt2 lab (sb UNION1 (a ,b )) asw rf mo >>.
Proof.
  ins; dupdes CONS.

  assert (case_hb: forall x y,
                     happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y ->
                     happens_before mt2 lab sb asw rf mo x y \/ x =a /\ y =b).
    by eauto using reordering_hb.

  unfold Semiconsistent; desf; unfold NW; intuition.

  unfold ExecutionFinite, admissible_reordering in *;
    desf; intuition.
  by red; ins; desf; eauto.

  by eapply reordering_acyclic_hb; eauto.

  destruct mt.
    by eapply acyclicity_orig; eauto.
    by eauto.
    exploit acyclicity_hbUrfna; eauto.
      by ins; desf; dupdes AR; exfalso; eauto.
    exploit acyclicity_hbUrf; eauto.
      by ins; desf; dupdes AR; exfalso; eauto.
    by eauto.

  by dupdes AR; dupdes Csb; red; ins; desf; subst; eauto.

  by dupdes Cdsb; repeat split; try red; ins; eauto using clos_trans_mon.

  unfold ConsistentMOhb in *; desf; intuition; red; ins.
  eapply CmoH; eauto.
  destruct (case_hb _ _ REL).
  by eauto. desf.
  by exfalso; dupdes AR; eapply AR_SL; desf;
     destruct (lab a); destruct (lab b); inversion IWa; inversion IWb;
     subst; eauto.

  unfold ConsistentSC in *; desf; intuition; red; ins.
  unfold restr_subset; ins.
  eapply Chbsc; eauto.
  destruct (case_hb _ _ REL).
  by eauto. desf.
  by exfalso; dupdes AR; eapply AR_Not_Both_Sc; eauto.

  unfold SCrestriction; ins.
  generalize RF, SC.
  eapply Cscr in RF. eapply RF in SC. clear RF. ins. desf.
    by intuition.
    right; intuition.
    eapply SC1; eauto.
    destruct (case_hb _ _ HB).
    by eauto. desf.
    unfold sc_restr in *. desf.
    eapply Crf in RF. desf.

    exfalso; dupdes AR; eapply AR_SL; xplit.
    destruct (lab a); inversion WRITE; eauto.
    by unfold sc_restr_cond, sc_restr, immediate in SC2; desf; desc; destruct (lab b); ins.

    by unnw; red in SC2; unfold immediate, sc_restr in SC2; desf; desf;
    destruct (lab a); destruct (lab b0); ins; desf.

  unfold ConsistentRF_dom_none in *; desf; intuition; ins.
  eapply CrfN; eauto.
  destruct (case_hb _ _ HB).
  by eauto. desf.
  by exfalso; dupdes AR; eapply AR_SL; desf;
     destruct (lab a); destruct (lab b); inversion READ; inversion WRI;
     subst; eauto.

  unfold ConsistentRFhb in *; desf; intuition; ins.
  exploit Crf; eauto. ins; desf.
  eapply CrfH; eauto.
  destruct (case_hb _ _ HB).
  by eauto. desf.
  by exfalso; dupdes AR; eapply AR_SL; desf;
     destruct (lab a); destruct (lab b); inversion READ; inversion WRITE;
     subst; eauto.

  unfold CoherentRR in *; desf; intuition; ins.
  eapply Crr; [ | exact RFa | exact RFb | exact MO ].
  destruct (case_hb _ _ HB).
  by eauto. desf.
  exfalso; dupdes AR; eapply AR_SL; desf; xplit; eauto with loc.
  erewrite <- rf_eq_loc by eauto.
  erewrite <- mo_eq_loc by eauto.
  by eauto using rf_eq_loc.

  unfold CoherentWR in *; desf; intuition; ins.
  eapply Cwr; eauto.
  destruct (case_hb _ _ HB).
  by eauto. desf.
  exfalso; dupdes AR; eapply AR_SL; desf; xplit; red; eauto with loc.
  erewrite <- mo_eq_loc by eauto.
  by eauto using rf_eq_loc.

  unfold CoherentRW in *; desf; intuition; ins.
  eapply Crw; eauto.
  destruct (case_hb _ _ HB).
  by eauto. desf.
  exfalso; dupdes AR; eapply AR_SL; desf; xplit; red; eauto with loc.
  erewrite <- rf_eq_loc by eauto.
  symmetry; by eauto using mo_eq_loc.

  unfold racy in *; desc; unnw; repeat (eexists; try edone);
  clear WRI NA; intro HB; eapply case_hb in HB; desf;
  by dupdes AR; eapply AR_SL; destruct (lab a); ins; destruct (lab b); ins.
Qed.

Using restrict_rf, we can lift this theorem to preserve consistent executions.

Theorem Consistent_reordering :
  forall mt (MT: mt <> MTorig) 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 (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    exists rf',
      << CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf' mo sc >> /\
      << RACE: racy mt2 lab sb asw rf mo -> racy mt2 lab (sb UNION1 (a ,b )) asw rf mo >>.
Proof.
  ins; exploit Semiconsistent_reordering; eauto using Consistent_weaken.
  intro; desf; unnw.
  eexists,; eauto using Consistent_restrict_rf, race_free_restrict_rf.
Qed.

Note that the theorem above requires a weaker adjacency condition. The theorem shown in the paper is a simple corollary.

Corollary Consistent_reordering_paper :
  forall 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 ->
    admissible_reordering mt acts lab a b ->
    adjacent sb a b ->
    adjacent asw a b ->
    mt <> MTorig ->
  exists rf',
    << CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf' mo sc >> /\
    << RACE: racy mt2 lab sb asw rf mo -> racy mt2 lab (sb UNION1 (a ,b )) asw rf mo >>.
Proof.
  ins; eapply Consistent_reordering;
  eauto using adjacent_weaken, adjacentW_weaken.
Qed.

This page has been generated by coqdoc