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

Lemma path_decomp_u1_pre :
  forall X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : forall x, rel b x -> rel a x),
    clos_trans X rel x y \/ clos_refl_trans X rel x a /\ y = b.
Proof.
  ins; eapply path_decomp_u1 in T; desf; eauto.
  rewrite clos_refl_transE in T0; desf; eauto.
  eapply t_step_rt in T0; desf; eauto.
  left; eapply t_rt_trans; [eapply t_rt_step|]; eauto.
Qed.

Lemma release_seq_u1_pre :
  forall 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: forall x (SB: sb b x), sb a x)
    (NMO: forall x (MO: mo b x), False)
    (NMO': forall x (MO: mo x b), False),
    release_seq mt2 lab sb rf mo x y.
Proof.
  unfold release_seq, release_seq_elem, diff_thread, same_thread; ins; desf; desf; eauto;
  [eapply path_decomp_u1_pre in RSE; desf; eauto; try solve [exfalso; eauto]| |];
  try right; repeat split; unfold NW; ins; eauto;
  try by exploit RSO; eauto; ins; desf; eauto;
         eapply path_decomp_u1_pre in x1; desf; eauto; exfalso; eauto.

  destruct mt2 as [[][]]; induction HB; unfold same_thread in *; ins;
  eauto using release_seq_alt.
  by eapply RS_thr; ins;
     eapply path_decomp_u1_pre in RSthr; desf; eauto; exfalso; eauto.
Qed.

Lemma path_decomp_u1_post :
  forall X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : forall x, rel x a -> rel x b),
    clos_trans X rel x y \/ x = a /\ clos_refl_trans X rel b y.
Proof.
  ins; eapply path_decomp_u1 in T; desf; eauto.
  rewrite clos_refl_transE in T; desf; eauto.
  eapply t_rt_step in T; desf; eauto.
  left; eapply rt_t_trans; [|eapply t_step_rt]; eauto.
Qed.

Lemma release_seq_u1_post :
  forall 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: forall x (SB: sb x a), sb x b)
    (NMO: forall x (MO: mo a x), False)
    (NMO': forall x (MO: mo x a), False),
    release_seq mt2 lab sb rf mo x y.
Proof.
  unfold release_seq, release_seq_elem, diff_thread, same_thread; ins; desf; desf; eauto;
  [eapply path_decomp_u1_post in RSE; desf; eauto; try solve [exfalso; eauto]| |];
  try right; repeat split; unfold NW; ins; eauto;
  try by exploit RSO; eauto; ins; desf; eauto;
         eapply path_decomp_u1_post in x1; desf; eauto; exfalso; eauto.
  destruct mt2 as [[][]]; induction HB; unfold same_thread in *; ins;
  eauto using release_seq_alt.
  by eapply RS_thr; ins;
     eapply path_decomp_u1_post in RSthr; desf; eauto; exfalso; eauto.
Qed.

Lemma path_decomp_u1_both :
  forall X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : forall x, rel b x -> rel a x)
         (DOM' : forall x, rel x a -> rel x b),
    clos_trans X rel x y \/ x = a /\ y = b.
Proof.
  ins; eapply path_decomp_u1 in T; desf; eauto.
  rewrite clos_refl_transE in *; desf; eauto; left.
    by eapply t_rt_step in T; desf; eapply t_rt_step; eauto.
    by eapply t_step_rt in T0; desf; eapply t_step_rt; eauto.
  by eapply t_rt_step in T; desf; eapply t_trans with b; [eapply t_rt_step|]; eauto.
Qed.

Lemma RacqFacq_hb :
  forall mt2 lab (sb asw : relation actid) rf mo
    (Cmo: ConsistentMO lab mo) a b
    (DOM: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw b x), asw a x)
    (DOM'': forall 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.
Proof.
  ins; induction HB; des; subst; eauto with hb.

  {
    unfold synchronizes_with in *; desf; desf; eauto; try (by left; vauto);
    try eapply release_seq_u1_pre in RS; eauto; rewrite ?Ab; ins;
    try (by eapply (proj1 Cmo) in MO; rewrite Ab in MO; ins; desf);
    try eapply path_decomp_u1_both in SBR; desf; eauto;
    try eapply path_decomp_u1_both in SBW; desf; eauto;
    try (by left; constructor; right; left; red; desf; unfold NW; eauto 16);
    try (rewrite Ab in SWthr; ins);
    try (by right; right; split; ins; apply sw_in_hb; red; unnw;
            unfold diff_thread in *; desf; rewrite Ab in *; ins; eauto 16);
    try (by destruct (lab a)).
  }

  left.
  clear HB1 HB2; unfold happens_before in *.
  rewrite t_step_rt in *; desf; desf; eauto 6 using rt_step.
  by exfalso; unfold synchronizes_with in *; desf; rewrite Ab in *.

  left.
  eapply t_trans with a; ins.
  clear HB1 HB2 IHHB1; unfold happens_before in *.
  rewrite t_step_rt in *; desf; desf; eauto 6 using rt_step.
  by exfalso; unfold synchronizes_with in *; desf; rewrite Ab in *.
Qed.

Lemma RacqFacq_acyclic :
  forall mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x y => happens_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: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw b x), asw a x)
    (DOM'': forall x (SB: sb x a), sb x b)
    (NREL: forall z (REL: rel b z), False),
   acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y \/ rel x y).
Proof.
  ins; intros x TT.
  assert (T: clos_trans actid
        (fun x y : actid =>
          x = a /\ y = b \/ (happens_before mt2 lab sb asw rf mo x y \/
         rel x y)) x x).
  { revert TT; generalize x at 1 3; induction 1; ins; desf;
    eauto 10 using clos_trans, sb_in_hb.
    eapply RacqFacq_hb in H; desf; eauto 10 using clos_trans, sb_in_hb.
  }
  clear TT; eapply cycle_decomp_u1 in T; desf; eauto.
  rewrite clos_refl_transE in T; desf; [by rewrite Ab in *; desf|].
  unfold happens_before in T; rewrite clos_trans_of_clos_trans1, t_step_rt in T.
  desf; eauto.
    by eapply (ACYC a); unfold happens_before;
       rewrite clos_trans_of_clos_trans1, t_step_rt;
       eauto 6.
  by unfold synchronizes_with in T; desf; rewrite Ab in *; ins.
  by eapply (ACYC a); unfold happens_before;
     rewrite clos_trans_of_clos_trans1, t_step_rt;
     eauto 8.
Qed.

Theorem RacqFacq_par :
  forall 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: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw b x), asw a x)
    (DOM'': forall 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 mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
  unfold Consistent; intros; desf; unfold NW; intuition.

  split; unfold NW; ins; desf; try by apply FIN; eauto.
  by split; apply FIN; intro X; rewrite X in *.

  red; ins.
  eapply RacqFacq_hb in H; eauto; desf; desf; eauto.
  rewrite Ab in *; ins.

  apply t_step_rt in H; desf.
  by rewrite clos_refl_transE in *; desf; eauto with hb.
  by red in H; desf; destruct (lab b); ins; desf.
  by rewrite clos_refl_transE in *; desf; eauto with hb.

  {
    destruct mt; ins; unfold rfna in *.
      by red; ins; eauto using happens_before_mon_sb.
      by eapply RacqFacq_acyclic; eauto; ins; desc; kill_incons Aa Ab.
      by eapply RacqFacq_acyclic; eauto; ins; desc; kill_incons Aa Ab.
  }

  by unfold ConsistentSB in *; ins; desf; rewrite ?Aa, ?Ab; eauto.

  by unfold ConsistentDSB, inclusion in *; desf; intuition; eauto using clos_trans_mon.

  repeat red; ins; eapply RacqFacq_hb in REL; eauto; desf; rewrite ?Aa, ?Ab in *; ins.
  by eapply CmoH; eauto.

  unfold ConsistentSC in *; desf; intuition; repeat red; ins.
  eapply RacqFacq_hb in REL; eauto; desf; rewrite ?Aa, ?Ab in *; ins.
  by eapply Chbsc; eauto.

  red; ins; edestruct Cscr; eauto; desf; right; split; ins.
  by eapply RacqFacq_hb in HB; eauto; desf; rewrite ?Aa, ?Ab in *; ins; eauto;
     unfold sc_restr_cond, immediate, sc_restr in *; desf; rewrite ?Ab in *; desf.

  red; ins; exploit CrfN; eauto.
  by eapply RacqFacq_hb in HB; eauto; desf; rewrite ?Aa, ?Ab in *; ins.

  red; ins; exploit CrfS; eauto; unfold NW; ins; desf.
  by repeat eexists; eauto using happens_before_mon_sb.

  red; ins; exploit CrfH; eauto; ins; desf; repeat eexists; eauto.
  by eapply RacqFacq_hb in HB; eauto; desf; kill_incons Aa Ab.

  red; ins; eapply RacqFacq_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Crr; eauto.

  red; ins; eapply RacqFacq_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Cwr; eauto.

  red; ins; eapply RacqFacq_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Crw; eauto.

  unfold racy in *; desc; unnw; repeat (eexists; try edone);
  clear WRI NA; intro HB; eapply RacqFacq_hb in HB; eauto;
  desf; rewrite ?Aa, ?Ab in *; ins; eauto.
Qed.

Corollary RacqFacq_par_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 ->
    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 mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
  unfold NW, adjacent; ins; desc; apply RacqFacq_par; eauto.
Qed.

Lemma FrelWrel_hb :
  forall mt2 lab (sb asw : relation actid) rf mo a b
    (Cmo: ConsistentMO lab mo)
    (DOM: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw x a), asw x b)
    (DOM'': forall 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.
Proof.
  ins; induction HB; desf; eauto with hb.

  {
    unfold synchronizes_with in *; desf; desf; eauto; try (by left; vauto);
    try eapply release_seq_u1_post in RS; eauto; rewrite ?Aa; ins;
    try (by eapply (proj1 Cmo) in MO; rewrite Aa in MO; ins; desf);
    try eapply path_decomp_u1_both in SBR; desf; eauto;
    try eapply path_decomp_u1_both in SBW; desf; eauto;
    try (by left; apply sw_in_hb; red; desf; unfold NW; eauto 16);
    try (rewrite Aa in SWthr; ins);
    try (by right; right; split; ins; apply sw_in_hb; red; unnw;
            unfold diff_thread in *; desf; rewrite Aa in *; ins; eauto 16);
    try (by destruct (lab b)).
  }

  left.
  clear HB1 HB2; unfold happens_before in *.
  rewrite t_rt_step in *; desf; desf; eauto 6 using rt_step.
  by exfalso; unfold synchronizes_with in *; desf; rewrite Aa in *.

  left.
  eapply t_trans with b; ins.
  clear HB1 HB2 IHHB0; unfold happens_before in *.
  rewrite t_rt_step in *; desf; desf; eauto 6 using rt_step.
  by exfalso; unfold synchronizes_with in *; desf; rewrite Aa in *.
Qed.

Lemma FrelWrel_acyclic :
  forall mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x y => happens_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: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw x a), asw x b)
    (DOM'': forall x (SB: sb x a), sb x b)
    (NREL: forall z (REL: rel z a), False),
   acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y \/ rel x y).
Proof.
  ins; intros x TT.
  assert (T: clos_trans actid
        (fun x y : actid =>
          x = a /\ y = b \/ (happens_before mt2 lab sb asw rf mo x y \/
         rel x y)) x x).
  { revert TT; generalize x at 1 3; induction 1; ins; desf;
    eauto 10 using clos_trans, sb_in_hb.
    by eapply FrelWrel_hb in H; desf; eauto 10 using clos_trans, sb_in_hb.
  }
  clear TT; eapply cycle_decomp_u1 in T; desf; eauto.
  rewrite clos_refl_transE in T; desf; [by rewrite Aa in *; desf|].
  unfold happens_before in T; rewrite clos_trans_of_clos_trans1, t_rt_step in T.
  desf; eauto.
    by eapply (ACYC b); unfold happens_before;
       rewrite clos_trans_of_clos_trans1, t_rt_step;
       eauto 6.
    by unfold synchronizes_with in T0; desf; rewrite Aa in *; ins.
  by eapply (ACYC b); unfold happens_before;
     rewrite clos_trans_of_clos_trans1, t_rt_step;
     eauto 8.
Qed.

Theorem FrelWrel_par :
  forall 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: forall x (SB: sb b x), sb a x)
    (DOM': forall x (SB: asw x a), asw x b)
    (DOM'': forall 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 mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
  unfold Consistent; intros; desf; unfold NW; intuition.

  split; unfold NW; ins; desf; try by apply FIN; eauto.
  by split; apply FIN; intro X; rewrite X in *.

  red; ins.
  eapply FrelWrel_hb in H; eauto; desf; desf; eauto.
  rewrite Aa in *; ins.

  apply t_rt_step in H0; desf.
  by rewrite clos_refl_transE in *; desf; eauto with hb.
  by red in H1; desf; destruct (lab a); ins; desf.
  by rewrite clos_refl_transE in *; desf; eauto with hb.

  {
    destruct mt; ins; unfold rfna in *.
      by red; ins; eauto using happens_before_mon_sb.
      by eapply FrelWrel_acyclic; eauto; ins; desc; kill_incons Aa Ab.
      by eapply FrelWrel_acyclic; eauto; ins; desc; kill_incons Aa Ab.
  }

  by unfold ConsistentSB in *; ins; desf; rewrite ?Aa, ?Ab; eauto.

  by unfold ConsistentDSB, inclusion in *; desf; intuition; eauto using clos_trans_mon.

  repeat red; ins; eapply FrelWrel_hb in REL; eauto; desf; rewrite ?Aa, ?Ab in *; ins.
  by eapply CmoH; eauto.

  unfold ConsistentSC in *; desf; intuition; repeat red; ins.
  eapply FrelWrel_hb in REL; eauto; desf; rewrite ?Aa, ?Ab in *; ins.
  by eapply Chbsc; eauto.

  red; ins; edestruct Cscr; eauto; desf; right; split; ins.
  by eapply FrelWrel_hb in HB; eauto; desf; rewrite ?Aa, ?Ab in *; ins; eauto;
     eapply Crf in RF; rewrite ?Aa in *; desf.

  red; ins; exploit CrfN; eauto.
  by eapply FrelWrel_hb in HB; eauto; desf; rewrite ?Aa, ?Ab in *; ins.

  red; ins; exploit CrfS; eauto; unfold NW; ins; desf.
  by repeat eexists; eauto using happens_before_mon_sb.

  red; ins; exploit CrfH; eauto; ins; desf; repeat eexists; eauto.
  by eapply FrelWrel_hb in HB; eauto; desf; kill_incons Aa Ab.

  red; ins; eapply FrelWrel_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Crr; eauto.

  red; ins; eapply FrelWrel_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Cwr; eauto.

  red; ins; eapply FrelWrel_hb in HB; eauto; desf; kill_incons Aa Ab.
  by eapply Crw; eauto.

  unfold racy in *; desc; unnw; repeat (eexists; try edone);
  clear WRI NA; intro HB; eapply FrelWrel_hb in HB; eauto;
  desf; rewrite ?Aa, ?Ab in *; ins; eauto.
Qed.

Corollary FrelWrel_par_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 ->
    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 mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
  unfold adjacent; ins; desc; eapply FrelWrel_par; eauto.
Qed.