# The Power memory model

In this section, we define the Power memory model of Alglave et al. We show that it is equivalent to reorderings over a stronger model requiring the relation (po U rf) to be acyclic.

Require Import List Relations Setoid Omega Permutation.
Require Import Classical ClassicalDescription.
Require Import Vbase extralib ExtraRelations.
Set Implicit Arguments.
Remove Hints plus_n_O.

Definition actid := nat.

Inductive act :=
| Async
| Alwsync
| Aload (l : nat) (v : nat)
| Astore (l : nat) (v : nat).

Definition loc a :=
match a with
| Astore l _ ⇒ 1
| _ ⇒ 0
end.

Definition is_access a :=
match a with
| Aload _ _ | Astore _ _true
| _false
end.

match a with
| _false
end.

Definition is_write a :=
match a with
| Astore _ _true
| _false
end.

Definition is_fence a :=
match a with
| Alwsync | Asynctrue
| _false
end.

Proof. by destruct a. Qed.

Lemma is_write_access a : is_write a is_access a.
Proof. by destruct a. Qed.

Hint Resolve is_read_access is_write_access : access.

## Power memory model definition

Section PowerModel.

Variable acts : list actid.
Variable lab : actid act.
Variable po : relation actid.
Variable deps : relation actid.
Variable rmw : relation actid.
Variable ppo : relation actid.
Variable rf : actid option actid.
Variable co : relation actid.

Definitions of auxiliary relations for the model.

Definition rfe x y := rf y = Some x ¬ po x y.

Definition fr x y := z, rf x = Some z co z y.

Definition fre x y := z, rf x = Some z co z y ¬ po x y.

Definition coe x y := co x y ¬ po x y.

Definition po_loc x y :=
po x y is_access (lab x) is_access (lab y) loc (lab x) = loc (lab y).

Definition sync x y :=
s, po x s po s y lab s = Async
is_access (lab x) is_access (lab y).

Definition lwsync x y :=
( s, po x s po s y lab s = Alwsync)
(is_read (lab x) is_access (lab y)
is_access (lab x) is_write (lab y)).

Definition fence := sync +++ lwsync.

Definition hb_power := ppo +++ fence +++ rfe.

Definition prop_base :=
clos_refl rfe ;; fence ;; clos_refl_trans hb_power.

Definition chapo :=
rfe +++ fre +++ coe +++ (fre ;; rfe) +++ (coe ;; rfe).

Definition prop :=
restr_rel (fun xis_write (lab x)) prop_base
+++ (clos_refl chapo ;; clos_refl prop_base ;; sync ;; clos_refl_trans hb_power).

The implicit well-formedness axioms

Definition ExecutionFinite :=
<< CLOlab: a, lab a Askip In a acts >>
<< CLOsb : a b, po a b In a acts In b acts >>.

Definition ConsistentRF_dom :=
a b (RF: rf b = Some a),
l v, <<WRI: lab a = Astore l v>> <<READ: lab b = Aload l v >>.

Definition CompleteRF :=
a (RF: rf a = None)

Definition ConsistentMO_dom :=
a b (MO: co a b),
is_write (lab a) is_write (lab b) loc (lab a) = loc (lab b).

Definition ConsistentRMW_dom :=
a b (RF: rmw a b),
<< PO: po a b >>
<< WRITE: is_write (lab b) >>
<< LOCEQ: loc (lab a) = loc (lab b) >>.

The constraints on the preserved program order (PPO)

Definition ppo_lower_bound :=
a b,
clos_trans (deps +++ po_loc) a b
is_write (lab b)
ppo a b.

Definition ppo_upper_bound :=
a b,
ppo a b
immediate po a b
clos_trans (deps +++ po_loc) a b.

The Power model

Definition ConsistentPower :=
<< CppoL: ppo_lower_bound >>

<< CrfD: ConsistentRF_dom >>
<< COrf: CompleteRF >>
<< Crmw: ConsistentRMW_dom >>
<< CcoD: ConsistentMO_dom >>
<< CcoF: l, is_total (fun a v, lab a = Astore l v) co >>
<< CcoT: transitive co >>
<< CcoI: irreflexive co >>
<< LOC_SC : acyclic (po_loc +++ (fun x yrf y = Some x) +++ co +++ fr) >>
<< ATOM : irreflexive (rmw ;; fre ;; coe) >>
<< NTA : acyclic hb_power >>
<< OBS : irreflexive (fre ;; prop ;; clos_refl_trans hb_power) >>
<< PROP: acyclic (co +++ prop) >>.

## Basic properties of the model

Lemma loceq_rf :
(CrfD: ConsistentRF_dom) a b (H: rf b = Some a),
loc (lab a) = loc (lab b).
Proof.
by ins; apply CrfD in H; desf; rewrite WRI, READ.
Qed.

Lemma loceq_co :
(CcoD: ConsistentMO_dom) a b (H: co a b),
loc (lab a) = loc (lab b).
Proof.
by ins; apply CcoD in H; desf.
Qed.

Lemma loceq_fr :
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
a b (H: fr a b),
loc (lab a) = loc (lab b).
Proof.
unfold fr; ins; desf; transitivity (loc (lab z));
eauto using loceq_co, loceq_rf, eq_sym.
Qed.

Lemma fr_dom :
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(FR: fr x y),
is_read (lab x) is_write (lab y) loc (lab x) = loc (lab y).
Proof.
unfold fr; ins; desc; eapply CrfD in FR; desc.
eapply CcoD in FR0; desc; destruct (lab x), (lab y); ins.
Qed.

Lemma rfe_dom :
(CrfD: ConsistentRF_dom) x y
(RFE: rfe x y),
is_write (lab x) is_read (lab y) loc (lab x) = loc (lab y).
Proof.
unfold rfe; ins; desc; eapply CrfD in RFE; desc.
Qed.

Lemma fre_dom :

(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(FRE: fre x y),
is_read (lab x) is_write (lab y) loc (lab x) = loc (lab y).
Proof.
unfold fre; ins; desc; eapply CrfD in FRE; desc.
eapply CcoD in FRE0; desc; destruct (lab x), (lab y); ins.
Qed.

## A stronger acyclicity condition

Definition nta_rel :=
deps +++ po_loc
+++ (fun x ypo x y (is_fence (lab x) is_fence (lab y)))
+++ rfe.

Lemma acyclic_nta
(CsbT: transitive po)
(CsbI: irreflexive po)
(Cdeps: inclusion deps po)
(CrfD: ConsistentRF_dom)
(NTA : acyclic hb_power)
(PPO_lower : ppo_lower_bound) :
acyclic nta_rel.
Proof.
assert (INCL: inclusion (clos_trans (deps +++ po_loc
+++ (fun x ypo x y
(is_fence (lab x)
is_fence (lab y)))))
po).
by unfold union, po_loc; induction 1; ins; desf; eauto.

unfold nta_rel; intros x X.
rewrite unionC in X.
eapply cycle_ur with (adom:=fun xis_write (lab x))
(bdom:=fun xis_read (lab x)) in X;
try solve [ins; exploit rfe_dom; eauto; ins; desf].
desf; eauto.
eapply NTA, clos_trans_mon; eauto; ins; clear X.
unfold hb_power, union in *; desf; eauto.
destruct (classic (fence a b)) as [|NF]; eauto.
assert (Y: c, clos_refl po a c clos_refl po c b
is_fence (lab c) False).
by clear -H0 H1 NF; ins; apply NF;
unfold fence, sync, lwsync, is_fence, clos_refl, union in *; desf;
[left |right]; ins; eauto 8 with access.
left; left; eapply PPO_lower; unfold union; ins; rename H into Z.
clear - Z INCL CsbT Y; induction Z; desf; eauto using clos_trans;
try solve [exfalso; eauto].
eapply t_trans; [eapply IHZ1 | eapply IHZ2]; ins; [red in H0|red in H];
desf; eapply Y in H1; try red; eauto.
Qed.

End PowerModel.

Definition ntb_rel i ll lab deps rf x y :=
In x i In y (concat ll)
nta_rel lab (mk_po i ll) deps rf x y.

Lemma acyclic_ntb i ll lab deps ppo rf
(ND: NoDup (i ++ concat ll))
(INIT: x, is_read (lab x) In x (concat ll))
(Cdeps: inclusion deps (mk_po i ll))
(CrfD: ConsistentRF_dom lab rf)
(NTA : acyclic (hb_power lab (mk_po i ll) ppo rf))
(PPO_lower : ppo_lower_bound lab (mk_po i ll) deps ppo) :
acyclic (ntb_rel i ll lab deps rf).
Proof.
ins; assert (acyclic (nta_rel lab (mk_po i ll) deps rf)).
eapply acyclic_nta; eauto using transitive_mk_po.
by red; eauto using mk_po_irreflexive.
assert (N: x y, nta_rel lab (mk_po i ll) deps rf x y In y (concat ll)).
unfold nta_rel, union, po_loc; ins; desf; eauto using mk_po_in2.
by eapply rfe_dom in H0; desf; eauto.
intros x X.
eapply cycle_ur with (adom := fun xIn x i)
(bdom := fun xIn x (concat ll)) in X; ins; desf.
by eapply H, clos_trans_mon; eauto; ins; desf.
eapply nodup_app with (a:=x0); eauto.
rewrite t_step_rt in X; desf.
eapply t_rt_step in X; desf.
by exfalso; eapply nodup_app; eauto.
rewrite t_rt_step in X; desf.
rewrite t_rt_step in X0; desf.
by exfalso; eapply nodup_app; eauto.
Qed.

Add Parametric Morphism : rfe with signature
same_relation ==> eq ==> same_relation as rfe_mor.
Proof.
unfold same_relation, inclusion, rfe; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : coe with signature
same_relation ==> eq ==> same_relation as coe_mor.
Proof.
unfold same_relation, inclusion, coe; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : fre with signature
same_relation ==> eq ==> eq ==> same_relation as fre_mor.
Proof.
unfold same_relation, inclusion, fre; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : po_loc with signature
eq ==> same_relation ==> same_relation as po_loc_mor.
Proof.
unfold same_relation, inclusion, po_loc; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : sync with signature
eq ==> same_relation ==> same_relation as sync_mor.
Proof.
unfold same_relation, inclusion, sync; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : lwsync with signature
eq ==> same_relation ==> same_relation as lwsync_mor.
Proof.
unfold same_relation, inclusion, lwsync; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : hb_power with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as hb_power_mor.
Proof.
unfold hb_power, fence; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : prop_base with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as prop_base_mor.
Proof.
unfold prop_base, fence; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : prop with signature
eq ==> same_relation ==> eq ==> eq ==> eq ==> same_relation as prop_mor.
Proof.
unfold prop, fence, chapo; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : ppo_lower_bound with signature
eq ==> same_relation ==> eq ==> eq ==> iff as ppo_lower_mor.
Proof.
by unfold ppo_lower_bound; split; ins; eapply H0; eauto; rewrite H in ×.
Qed.

Add Parametric Morphism : ConsistentRMW_dom with signature
eq ==> same_relation ==> eq ==> iff as ConsistentRMW_dom_mor.
Proof.
unfold same_relation, inclusion, ConsistentRMW_dom; split; ins;
apply H0 in RF; clear H0; desc; unnw; eauto.
Qed.

Add Parametric Morphism : ConsistentPower with signature
eq ==> same_relation ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as ConsistentPower_mor.
Proof.
unfold ConsistentPower; unnw; ins; rewrite H; eauto; tauto.
Qed.

Add Parametric Morphism : nta_rel with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as nta_rel_mor.
Proof.
unfold nta_rel; ins; rewrite H at 1 2.
unfold same_relation, inclusion, union in *; intuition; eauto.
Qed.

## Soundness and completeness of reorderings

Lemma po_loc_reorder lab po a b
(LOC: loc (lab a) loc (lab b)) :
po_loc lab (reorder po a b) <--> po_loc lab po.
Proof.
unfold po_loc, reorder; split; red; ins; desf; eauto; try congruence.
split; ins; left; split; ins; intro; desf.
Qed.

Lemma rfe_reorder lab po rf a b
(Crf: ConsistentRF_dom lab rf)
(LOC: loc (lab a) loc (lab b)) :
rfe (reorder po b a) rf <--> rfe po rf.
Proof.
unfold rfe, reorder; split; red; ins; intuition; desf; eauto;
eapply loceq_rf in H0; eauto.
apply H3; intro; desf; eauto.
Qed.

Lemma fre_reorder lab po rf co a b
(Crf: ConsistentRF_dom lab rf)
(Cco: ConsistentMO_dom lab co)
(LOC: loc (lab a) loc (lab b)) :
fre (reorder po b a) rf co <--> fre po rf co.
Proof.
split; red; ins; exploit fre_dom; eauto; ins; desf;
unfold fre, reorder in *; desf; repeat eexists; eauto;
intro; desf; apply H1; left; split; ins; intro; desf; congruence.
Qed.

Lemma coe_reorder lab po co a b
(Cco: ConsistentMO_dom lab co)
(LOC: loc (lab a) loc (lab b)) :
coe (reorder po b a) co <--> coe po co.
Proof.
unfold coe, reorder; split; red; ins; desf; split; ins; intro; desf;
apply Cco in H; desf.
destruct H0; eauto; left; split; ins; intro; desf; congruence.
Qed.

Lemma sync_reorder lab (po : relation actid) a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
sync lab (reorder po a b) <--> sync lab po.
Proof.
split; red; ins; unfold sync, reorder in *; desf; eauto 8;
try (by destruct (lab a)); try (by destruct (lab b)).
s; repeat split; ins; left; split; ins; intro; desf;
try (by destruct (lab a)); try (by destruct (lab b)).
Qed.

Lemma lwsync_reorder lab (po : relation actid) a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
lwsync lab (reorder po a b) <--> lwsync lab po.
Proof.
split; red; ins; unfold lwsync, reorder in *; desf;
split; ins; eauto 8;
try (by destruct (lab a)); try (by destruct (lab b));
s; repeat split; ins; left; split; ins; intro; desf;
try (by destruct (lab a)); try (by destruct (lab b)).
Qed.

Lemma hbp_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
hb_power lab (reorder po a b) ppo rf <--> hb_power lab po ppo rf.
Proof.
unfold hb_power, fence.
rewrite rfe_reorder, sync_reorder, lwsync_reorder; eauto; reflexivity.
Qed.

Lemma base_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
prop_base lab (reorder po a b) ppo rf <--> prop_base lab po ppo rf.
Proof.
unfold prop_base, fence.
rewrite hbp_reorder, rfe_reorder, sync_reorder, lwsync_reorder;
eauto; reflexivity.
Qed.

Lemma prop_reorder lab po ppo rf co a b
(Crf: ConsistentRF_dom lab rf)
(Cmo: ConsistentMO_dom lab co)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
prop lab (reorder po a b) ppo rf co <--> prop lab po ppo rf co.
Proof.
unfold prop, chapo.
rewrite hbp_reorder, rfe_reorder, fre_reorder, sync_reorder, coe_reorder, base_reorder;
eauto 2; reflexivity.
Qed.

Lemma nta_rel_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
nta_rel lab (reorder po a b) ppo rf <--> nta_rel lab po ppo rf.
Proof.
unfold nta_rel.
rewrite po_loc_reorder, rfe_reorder; eauto; ins; unfold union, reorder.
split; red; ins; repeat split; ins; desf; eauto;
left; right; split; eauto; left; split; ins; intro; desf.
Qed.

Lemma ntb_rel_reorder i ll1 l1 a b l2 ll2 lab ppo rf
(WF: NoDup (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)))
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
ntb_rel i (ll1 ++ (l1 ++ a :: b :: l2) :: ll2) lab ppo rf <-->
ntb_rel i (ll1 ++ (l1 ++ b :: a :: l2) :: ll2) lab ppo rf.
Proof.
unfold same_relation, inclusion, ntb_rel; split; ins; desf;
eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord i);
right;
eapply nta_rel_mor; try symmetry; try eapply mk_po_reorder;
eauto using Permutation_reord, Permutation_nodup;
eapply nta_rel_reorder; eauto.
Qed.

Lemma ConsistentRMW_dom_reorder lab po rmw x y
(LOC: loc (lab x) loc (lab y)) :
ConsistentRMW_dom lab (reorder po x y) rmw
ConsistentRMW_dom lab po rmw.
Proof.
unfold ConsistentRMW_dom, reorder; split; ins; desf;
apply H in RF; clear H; desc; unnw; desf; intuition; eauto; ins; try congruence.
left; split; ins; desf.
Qed.

Lemma ppo_lower_bound_reorder lab po deps ppo a b
(LOC: loc (lab a) loc (lab b)) :
ppo_lower_bound lab (reorder po a b) deps ppo
ppo_lower_bound lab po deps ppo.
Proof.
by split; repeat red; ins; eapply H; ins; rewrite po_loc_reorder in ×.
Qed.

Lemma ConsistentPower_reorder :
lab po deps rmw ppo rf co a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)),
ConsistentPower lab po deps rmw ppo rf co
ConsistentPower lab (reorder po a b) deps rmw ppo rf co.
Proof.
ins; unfold ConsistentPower; split; ins; desc; unnw;
revert CppoL Crmw LOC_SC ATOM NTA OBS PROP;
rewrite po_loc_reorder, fre_reorder, coe_reorder, hbp_reorder, prop_reorder,
ppo_lower_bound_reorder, ConsistentRMW_dom_reorder; eauto 2; ins; intuition.
Qed.

## Reduction of the Power memory model

Definition Power_reorder lab init deps (ll ll' : list (list actid)) :=
ll1 l1 a b l2 ll2,
<< NFa: ¬ is_fence (lab a) >>
<< NFb: ¬ is_fence (lab b) >>
<< LOC: loc (lab a) loc (lab b) >>
<< Nab: ¬ deps a b >>
<< WF: NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) >>
<< EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >>
<< EQ': ll' = ll1 ++ (l1 ++ b :: a :: l2) :: ll2 >>.

Fixpoint metric (ord: relation actid) (ll : list actid) :=
match ll with
| nil ⇒ 0
| a :: ll
length (filter (fun xif excluded_middle_informative (ord x a)
then true else false) ll) +
metric ord ll
end.

Add Parametric Morphism : metric with signature
same_relation ==> eq ==> eq as metric_mor.
Proof.
unfold same_relation; desc; induction y0; ins; f_equal; eauto.
clear - H; induction y0; ins; desf; ins; try congruence;
exfalso; eauto.
Qed.

Lemma reorder_metric (ord : relation actid)
(T: transitive ord) (IRR: irreflexive ord) ll1 l1 a b (ORD: ord b a) l2 ll2 :
metric ord (concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) <
metric ord (concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).
Proof.
rewrite !concat_app, !concat_cons, <- !app_assoc; ins.
rewrite !app_assoc.
induction (concat ll1 ++ l1); ins; desf; ins;
try (solve [exfalso; eauto]); try omega.
rewrite perm_swap at 1; omega.
Qed.

Power-coherence is equivalent to performing reorderings over the stronger Power model that additionally requires (po U rf) to be acyclic.

Theorem Power_alternative :
lab init ll (ND: NoDup (init ++ concat ll)) deps
(WF: inclusion deps (mk_po init ll))
(INIT: x, is_read (lab x) In x (concat ll))
(MAIN: x, In x (concat ll) is_access (lab x))
rmw ppo rf co,
ConsistentPower lab (mk_po init ll) deps rmw ppo rf co

ll',
clos_refl_trans (Power_reorder lab init deps) ll ll'
ConsistentPower lab (mk_po init ll') deps rmw ppo rf co
acyclic (mk_po init ll' +++ (fun x yrf y = Some x)).
Proof.
split; ins; desf; cycle 1.
rename H into J; clear H1 ND; induction J using clos_refl_trans_ind_left; eauto.
unfold Power_reorder in *; desf; apply IHJ; clear IHJ.
by rewrite <- mk_po_reorder, <- ConsistentPower_reorder; eauto.

induction ll using
(well_founded_ind (well_founded_ltof _
(fun pmetric (tot_ext_nat (ntb_rel init p lab deps rf))
(concat p)))); unfold ltof in ×.
destruct (classic ( ll1 l1 a b l2 ll2,
<< NFa: ¬ is_fence (lab a) >>
<< NFb: ¬ is_fence (lab b) >>
<< LOC: loc (lab a) loc (lab b) >>
<< Nab: ¬ deps a b >>
<< EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >>
<< ORD: ¬ tot_ext_nat (ntb_rel init ll lab deps rf) a b >> )).
desf.
exploit (H0 (ll1 ++ (l1 ++ b :: a :: l2) :: ll2));
eauto using Permutation_reord, Permutation_nodup.
red in H; desc.
rewrite ntb_rel_reorder;
eauto using Permutation_nodup, Permutation_reord.
eapply reorder_metric; eauto using tot_ext_nat_trans, tot_ext_nat_extends.
eapply tot_ext_nat_irr, acyclic_ntb;
eauto using Permutation_nodup, Permutation_reord.

by destruct (eqP a b) as [|NEQ]; desf;
eapply tot_ext_nat_total in NEQ; desf; eauto; desf.

rewrite <- mk_po_reorder; eauto using Permutation_reord, Permutation_nodup.
by red; ins; unfold reorder; left; split; eauto; intro; desf.

by eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord init).
by eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord init).

rewrite <- mk_po_reorder, <- ConsistentPower_reorder in H;
eauto using Permutation_reord, Permutation_nodup.
intro X; desc; eexists; split; eauto; eapply rt_trans; eauto.
apply rt_step; ins.
eauto using clos_refl_trans; red; unnw; repeat eexists; eauto.

clear H0; ll; split; [|split]; eauto using rt_refl; intros x X.

assert (Z: ll1 l1 a b l2 ll2,
ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2
is_fence (lab a)
is_fence (lab b)
is_access (lab a) is_access (lab b) loc (lab a) = loc (lab b)
deps a b
tot_ext_nat (ntb_rel init ll lab deps rf) a b).
{ ins; unnw; desf; apply NNPP; intro; destruct H1; desf; ll1, l1, a, b.
do 7 try eexists; eauto; first [intro|apply NNPP; intro]; desf; destruct H0; eauto 8.
right; right; left; repeat split; ins; eapply MAIN;
rewrite concat_app, concat_cons, <- app_assoc; ins; eauto 6 using in_or_app, in_eq, in_cons.
}
clear H1.

eapply clos_trans_mon with (r' := mk_po init ll +++ rfe (mk_po init ll) rf) in X.
2: by unfold union, rfe; ins; tauto.
cut (clos_trans (immediate (mk_po init ll) +++ rfe (mk_po init ll) rf) x x);
[clear X; intro X|]; cycle 1.
revert X; generalize x at 1 3; unfold union.
induction 1; desf; eauto using clos_trans.
eapply clos_trans_mon; [eapply clos_trans_imm, H0|];
eauto using transitive_mk_po, mk_po_in1; red; eauto using mk_po_irreflexive.

red in H; desc; unnw.
eapply tot_ext_nat_irr.
eapply acyclic_ntb; eauto.
instantiate (1:=x); revert X; generalize x at 1 3;
induction 1; [|eby eapply tot_ext_nat_trans].
revert H;
unfold ntb_rel, nta_rel, union, po_loc; ins; desf; eauto 10 using tot_ext_nat_extends.
destruct (classic (In x init)).
by apply proj1, mk_po_in2 in H; eauto using tot_ext_nat_extends.
eapply mk_po_immediateD in H; desf.
specialize (Z _ _ _ _ _ _ eq_refl); desf;
eauto 10 using tot_ext_nat_extends, mk_po_trivial.
Qed.