Definition of the Power memory model
Require Import Classical List Relations.
Require Import Vbase ExtraRelations.
Set Implicit Arguments.
Remove Hints plus_n_O.
Definition actid := nat.
Inductive act :=
| Askip
| Async
| Alwsync
| Aload (l : nat) (v : nat)
| Astore (l : nat) (v : nat).
Definition loc a :=
match a with
| Aload l _
| Astore l _ ⇒ 1
| _ ⇒ 0
end.
Definition is_access a :=
match a with
| Aload _ _ | Astore _ _ ⇒ true
| _ ⇒ false
end.
Definition is_read a :=
match a with
| Aload _ _ ⇒ true
| _ ⇒ false
end.
Definition is_write a :=
match a with
| Astore _ _ ⇒ true
| _ ⇒ false
end.
Lemma is_read_access a : is_read a → is_access a.
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.
Section PowerModel.
Variable acts : list actid.
Variable lab : actid → act.
Variable po : actid → actid → Prop.
Variable deps : actid → actid → Prop.
Variable rmw : actid → actid → Prop.
Variable rf : actid → option actid.
Variable co : actid → actid → Prop.
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_RW x y :=
po x y ∧ is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).
Definition ppo x y :=
(deps x y ∨ seq (clos_refl deps) po_loc_RW x y)
∧ is_read (lab x) ∧ is_access (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 :=
union sync lwsync.
Definition hb_power := union ppo (union fence rfe).
Definition prop_base :=
(seq (clos_refl rfe) (seq fence (clos_refl_trans hb_power))).
Definition chapo :=
union rfe (union fre (union coe (union (seq fre rfe) (seq coe rfe)))).
Definition prop :=
union (restr_rel (fun x ⇒ is_write (lab x)) prop_base)
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base) (seq 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)
(READ: is_read (lab a)), False.
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 >> ∧
<< POI: ∀ c (SB: po c b) (NEQ: c ≠ a), po c a >> ∧
<< POI': ∀ c (SB: po a c) (NEQ: c ≠ b), po b c >> ∧
<< READ: is_read (lab a) >> ∧
<< WRITE: is_write (lab b) >> ∧
<< LOCEQ: loc (lab a) = loc (lab b) >>.
The Power axioms.
Definition uniproc_condition :=
∀ l, acyclic (union (restr_rel (fun x ⇒ is_access (lab x) ∧
loc (lab x) = l) po)
(union (fun x y ⇒ rf y = Some x) (union co fr))).
Definition observation_condition :=
∀ x y (FRE: fre x y) z (PROP: prop y z)
(HB: clos_refl_trans hb_power z x), False.
Definition ConsistentPower :=
<< FIN : ExecutionFinite >> ∧
<< CsbT: transitive po >> ∧
<< CsbI: irreflexive po >> ∧
<< 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 : uniproc_condition >> ∧
<< ATOM : ∀ x y (RMW: rmw x y) z (FRE: fre x z) (COE: coe z y), False >> ∧
<< NTA : acyclic hb_power >> ∧
<< OBS : observation_condition >> ∧
<< PROP: acyclic (union co prop) >>.
Next, we define an equivalent uniproc condition that is more convenient for
proofs.
Definition eqloc rel x y :=
rel x y ∧ is_access (lab x) ∧ is_access (lab y) ∧ loc (lab x) = loc (lab y).
Definition uniproc_condition_eqloc :=
acyclic (union (eqloc po) (union (fun x y ⇒ rf y = Some x) (union co fr))).
We also define a simpler equivalent observation condition.
We define versions of the fence and hb relations to include only
edges that can be ensured without strong synchronization primitives.
Specifically, we exclude any write-to-read edges that are ensured by strong
sync fences.
Definition fence_weak x y :=
(∃ s, po x s ∧ po s y ∧ (lab s = Alwsync ∨ lab s = Async))
∧ (is_read (lab x) ∧ is_access (lab y) ∨
is_access (lab x) ∧ is_write (lab y)).
Definition hb_weak := union ppo (union fence_weak rfe).
Using these versions of fence and hb, we can define an equivalent
propogation condition:
Definition prop_base_weak :=
(seq (clos_refl rfe) (seq fence_weak (clos_refl_trans hb_weak))).
Definition prop_weak :=
union (restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak)
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak)))).
and yet another equivalent observation condition.
We next define an alternative memory model for Power that uses a total
order (so) over sync fence events. The alternative model depends on the
following auxiliary definitions.
Definition so_step so a b :=
∃ f f',
po a f ∧ so f f' ∧ po f' b ∧ lab f = Async ∧ lab f' = Async.
Definition hb_so so := union hb_weak (so_step so).
Definition fence_so so := union fence_weak (so_step so).
Definition prop_base_so so :=
(seq (clos_refl rfe) (seq (fence_so so) (clos_refl_trans (hb_so so)))).
Definition prop_so so :=
(restr_rel (fun x ⇒ is_write (lab x)) (prop_base_so so)).
Definition ConsistentSyncTotal so :=
<< FIN : ExecutionFinite >> ∧
<< CsbT: transitive po >> ∧
<< CsbI: irreflexive po >> ∧
<< 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 >> ∧
<< CsoF: is_total (fun a ⇒ lab a = Async) so >> ∧
<< CsoT: transitive so >> ∧
<< CsoI: irreflexive so >> ∧
<< LOC_SC : uniproc_condition >> ∧
<< ATOM : ∀ x y (RMW: rmw x y) z (FRE: fre x z) (COE: coe z y), False >> ∧
<< NTA : acyclic (hb_so so) >> ∧
<< OBS : ∀ x y (FRE: fre x y) (PROP: prop_base_so so y x), False >> ∧
<< PROP: acyclic (union co (union so (prop_so so))) >>.
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.
by rewrite WRI, READ.
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.
Lemma hb_is_access_l (CrfD: ConsistentRF_dom) x y :
hb_power x y → is_access (lab x).
Proof.
ins; repeat (red in H; desf); eauto with access.
by eapply CrfD in H; desc; rewrite WRI.
Qed.
Lemma hb_is_access_r (CrfD: ConsistentRF_dom) x y :
hb_power x y → is_access (lab y).
Proof.
ins; repeat (red in H; desf); eauto with access.
by eapply CrfD in H; desc; rewrite READ.
Qed.
Hint Immediate hb_is_access_l hb_is_access_r : access.
Lemma hbp_is_access_l (CrfD: ConsistentRF_dom) x y :
clos_trans hb_power x y → is_access (lab x).
Proof.
ins; apply t_step_rt in H; desf; eauto with access.
Qed.
Lemma hbp_is_access_r (CrfD: ConsistentRF_dom) x y :
clos_trans hb_power x y → is_access (lab y).
Proof.
ins; apply t_rt_step in H; desf; eauto with access.
Qed.
Hint Immediate hbp_is_access_l hbp_is_access_r : access.
Lemma hb_weak_is_access_l (CrfD: ConsistentRF_dom) x y :
hb_weak x y → is_access (lab x).
Proof.
ins; repeat (red in H; desf); eauto with access.
by eapply CrfD in H; desc; rewrite WRI.
Qed.
Lemma hb_weak_is_access_r (CrfD: ConsistentRF_dom) x y :
hb_weak x y → is_access (lab y).
Proof.
ins; repeat (red in H; desf); eauto with access.
by eapply CrfD in H; desc; rewrite READ.
Qed.
Hint Immediate hb_weak_is_access_l hb_weak_is_access_r : access.
Lemma hb_weakp_is_access_l (CrfD: ConsistentRF_dom) x y :
clos_trans hb_weak x y → is_access (lab x).
Proof.
ins; apply t_step_rt in H; desf; eauto with access.
Qed.
Lemma hb_weakp_is_access_r (CrfD: ConsistentRF_dom) x y :
clos_trans hb_weak x y → is_access (lab y).
Proof.
ins; apply t_rt_step in H; desf; eauto with access.
Qed.
Hint Immediate hb_weakp_is_access_l hb_weakp_is_access_r : access.
Lemma chapo_access
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) a b :
chapo a b → is_access (lab a) ∧ is_access (lab b).
Proof.
unfold chapo, union, seq; ins; desf.
- eapply rfe_dom in H; desf; eauto with access.
- eapply fre_dom in H; desf; eauto with access.
- red in H; desc; eapply CcoD in H; desf; eauto with access.
- eapply fre_dom in H; desf;
eapply rfe_dom in H0; desf; eauto with access.
- red in H; desc; eapply CcoD in H; desf;
eapply rfe_dom in H0; desf; eauto with access.
Qed.
The two uniproc conditions are equivalent.
Proposition uniproc_condition_alt :
∀
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom),
uniproc_condition ↔ uniproc_condition_eqloc.
Proof.
split; repeat red; ins.
2: by eapply clos_trans_mon in H0; eauto;
unfold union, eqloc, restr_rel; ins; desf; eauto.
eapply (H (loc (lab x)) x).
revert H0; generalize x at 1 3 4.
intros ? K; apply clos_trans_t1n in K; induction K;
red in H0; desf; vauto.
by apply t_step; left; unfold eqloc, restr_rel in *; desf.
by unfold eqloc, restr_rel in *; desf; rewrite H3;
eapply t_trans with y; eauto; apply t_step; left;
unfold eqloc, restr_rel in *; desf.
assert (loc (lab x) = loc (lab y)) as ->; [|by eapply t_trans; vauto].
clear - CrfD CcoD H0; unfold union in *; desf;
eauto using eq_sym, loceq_rf, loceq_co, loceq_fr.
Qed.
Lemma may_chapoE :
clos_refl chapo <--> seq (clos_refl (union coe fre)) (clos_refl rfe).
Proof.
unfold clos_refl, chapo, seq, union; split; red; ins; desf; eauto 8.
Qed.
Lemma freE a b : fre a b ↔ fr a b ∧ ¬ po a b.
Proof.
by unfold fr, fre; split; ins; desf; eauto.
Qed.
Lemma fence_weakE x y :
fence_weak x y ↔ fence x y ∧ ¬ (is_write (lab x) ∧ is_read (lab y)).
Proof.
unfold fence, fence_weak, lwsync, sync, union.
intuition; desf; eauto 10 with access;
try (by destruct (lab x); ins; destruct (lab y); ins; intuition).
Qed.
Lemma fenceE x y :
fence x y ↔ fence_weak x y ∨ sync x y ∧ is_write (lab x) ∧ is_read (lab y).
Proof.
unfold fence, fence_weak, lwsync, sync, union.
intuition; desf; eauto 10 with access.
destruct (lab x); ins; eauto 10.
destruct (lab y); ins; eauto 10.
Qed.
Inclusion lemmas
Lemma inclusion_sync_fence : inclusion sync fence.
Proof. vauto. Qed.
Lemma inclusion_fence_hb : inclusion fence hb_power.
Proof. vauto. Qed.
Lemma inclusion_fence_hb_weak : inclusion fence_weak hb_weak.
Proof. vauto. Qed.
Lemma inclusion_fence_weak_hb : inclusion fence_weak hb_power.
Proof.
by red; ins; rewrite fence_weakE in *; desf; apply inclusion_fence_hb.
Qed.
Lemma inclusion_rfe_hb : inclusion rfe hb_power.
Proof. vauto. Qed.
Lemma inclusion_rfe_hb_weak : inclusion rfe hb_weak.
Proof. vauto. Qed.
Lemma inclusion_hb_weak_hb : inclusion hb_weak hb_power.
Proof.
unfold hb_weak, hb_power, union; red; ins; desf; eauto;
by eapply inclusion_fence_weak_hb.
Qed.
Hint Resolve inclusion_sync_fence
inclusion_fence_hb_weak inclusion_rfe_hb_weak
inclusion_fence_hb inclusion_fence_weak_hb inclusion_rfe_hb
inclusion_hb_weak_hb : inclusion.
Lemma inclusion_base_hb : inclusion prop_base (clos_refl_trans hb_power).
Proof.
eapply inclusion_seq_trans, inclusion_seq_trans; vauto; eauto with inclusion.
Qed.
Lemma inclusion_base_hb_weak :
inclusion prop_base_weak (clos_refl_trans hb_weak).
Proof.
eapply inclusion_seq_trans, inclusion_seq_trans; vauto; eauto with inclusion.
Qed.
Lemma inclusion_base_weak_hb :
inclusion prop_base_weak (clos_refl_trans hb_power).
Proof.
eapply inclusion_seq_trans, inclusion_seq_trans; vauto; eauto with inclusion.
Qed.
Lemma inclusion_fence_po (T: transitive po) : inclusion fence po.
Proof.
unfold fence, sync, lwsync, union; red; ins; desf; eauto.
Qed.
Lemma ppo_in_po
(T: transitive po) (INCL: inclusion deps po) x y :
ppo x y → po x y.
Proof.
unfold ppo, seq, clos_refl, po_loc_RW; ins; desf; eauto.
Qed.
Lemma fr_po_hb :
∀ (CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y,
fr x y → po x y →
hb_power x y.
Proof.
ins; exploit fr_dom; eauto; ins; desc.
unfold hb_power, ppo, po_loc_RW, union, seq, clos_refl.
eauto 12 with access.
Qed.
Transitivity lemmas
Lemma base_hb_trans a b c :
prop_base a b →
clos_refl_trans hb_power b c →
prop_base a c.
Proof.
unfold prop_base, seq; ins; desf; eauto 10 using rt_trans.
Qed.
Lemma rfe_base_trans (CrfD: ConsistentRF_dom) a b c:
rfe a b →
prop_base b c →
prop_base a c.
Proof.
unfold prop_base, rfe, seq, clos_refl; ins; desf; eauto 8.
eapply CrfD in H; eapply CrfD in H0; desf; congruence.
Qed.
Lemma rrfe_base_trans (CrfD: ConsistentRF_dom) a b c:
clos_refl rfe a b →
prop_base b c →
prop_base a c.
Proof.
unfold clos_refl; ins; desf; eauto using rfe_base_trans.
Qed.
Lemma base_sync_base a b c:
clos_refl_trans prop_base a b →
sync b c →
prop_base a c.
Proof.
unfold seq; rewrite clos_refl_transE; ins; desf.
by repeat eexists; eauto using rt_refl, inclusion_sync_fence.
eapply t_step_rt in H; desc.
eapply base_hb_trans; eauto.
eapply inclusion_seq_trans; vauto.
∃ b; split; eauto.
eapply clos_rt_idempotent, clos_refl_trans_mon; eauto using inclusion_base_hb.
eapply rt_step; eauto with inclusion.
Qed.
Hint Resolve base_sync_base rfe_base_trans rrfe_base_trans base_hb_trans : trans.
Lemma ppo_trans (T: transitive deps) a b c :
ppo a b →
ppo b c →
ppo a c.
Proof.
unfold ppo, po_loc_RW, seq, clos_refl; ins; desf; eauto 12;
try (by destruct (lab b); ins);
try (by destruct (lab z); ins).
Qed.
Lemma ppo_weaken (T: transitive po) (INCL : inclusion deps po) a b :
ppo a b →
po a b ∧ is_read (lab a) ∧ is_access (lab b).
Proof.
unfold ppo, po_loc_RW, seq, clos_refl in *; ins; desf; eauto.
Qed.
Lemma ppo_fence_trans (T: transitive po) (INCL : inclusion deps po) a b c :
ppo a b →
fence b c →
fence a c.
Proof.
unfold fence, sync, lwsync, seq, union in ×.
ins; apply ppo_weaken in H; desf; eauto 12 with access.
Qed.
Lemma fence_trans (T: transitive po) a b c :
fence a b →
fence b c →
fence a c.
Proof.
unfold inclusion, fence, ppo, sync, lwsync, seq, union in ×.
ins; desf; try (by destruct (lab b)); eauto 12 with access.
Qed.
Lemma fence_ppo_trans (T: transitive po) (INCL : inclusion deps po) a b c :
fence a b →
ppo b c →
fence a c.
Proof.
unfold inclusion, fence, sync, lwsync, seq, union in ×.
ins; apply ppo_weaken in H0; desf; eauto 10.
by destruct (lab b); ins.
Qed.
Lemma sync_trans (T: transitive po) a b c :
sync a b →
sync b c →
sync a c.
Proof. unfold sync; ins; desf; eauto 8. Qed.
Lemma prop_base_weak_trans a b c :
prop_base_weak a b →
prop_base_weak b c →
prop_base_weak a c.
Proof.
unfold sync, prop_base_weak, seq; ins; desf.
repeat (eexists; eauto).
eapply rt_trans, rt_trans; eauto.
eapply rt_trans, rt_step; [|by vauto].
eapply inclusion_r_rt; eauto; vauto.
Qed.
Lemma prop_base_trans a b c :
prop_base a b →
prop_base b c →
prop_base a c.
Proof.
unfold sync, prop_base, seq; ins; desf.
repeat (eexists; eauto).
eapply rt_trans, rt_trans; eauto.
eapply rt_trans, rt_step; [|by vauto].
eapply inclusion_r_rt; eauto; vauto.
Qed.
Hint Resolve ppo_trans ppo_fence_trans fence_trans fence_ppo_trans : trans.
Hint Resolve sync_trans : trans.
A happens-before path starting from a read either stays in the same thread,
or it must go through a write.
Lemma hb_RT :
∀ (T: transitive po)
(INCL : inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(P : clos_trans hb_power x y)
(R : is_read (lab x)),
po x y ∨
(∃ m : actid,
clos_refl_trans hb_power x m ∧ po x m ∧
clos_refl_trans hb_power m y ∧ is_write (lab m)).
Proof.
ins; induction P; desf.
unfold hb_power, fence, sync, lwsync, union in × |- ; desf; eauto.
by apply ppo_weaken in H; desf; vauto.
by apply rfe_dom in H; desf; destruct (lab x).
case_eq (is_write (lab y)); ins.
by exploit IHP1; ins; desf; eauto 8 using rt_trans, clos_trans_in_rt.
assert (is_access (lab y)) by eauto with access.
assert (is_read (lab y)) by (destruct (lab y); ins); desf.
exploit IHP1; ins; exploit IHP2; ins; desf;
eauto 10 using rt_trans, clos_trans_in_rt.
Qed.
Lemma hb_weak_RT :
∀ (T: transitive po)
(INCL : inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(P : clos_trans hb_weak x y)
(R : is_read (lab x)),
po x y ∨
(∃ m : actid,
clos_refl_trans hb_weak x m ∧ po x m ∧
clos_refl_trans hb_weak m y ∧ is_write (lab m)).
Proof.
ins; induction P; desf.
unfold hb_weak, fence_weak, sync, lwsync, union in × |- ; desf; eauto.
by apply ppo_weaken in H; desf; vauto.
by apply rfe_dom in H; desf; destruct (lab x).
case_eq (is_write (lab y)); ins.
by exploit IHP1; ins; desf; eauto 8 using rt_trans, clos_trans_in_rt.
assert (is_access (lab y)) by eauto with access.
assert (is_read (lab y)) by (destruct (lab y); ins); desf.
exploit IHP1; ins; exploit IHP2; ins; desf;
eauto 10 using rt_trans, clos_trans_in_rt.
Qed.
Lemma hb_weak_TW :
∀ (T: transitive po)
(INCL : inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(P : clos_refl_trans hb_weak x y)
(R : is_write (lab y)),
clos_refl po x y ∨
(∃ m : actid,
clos_refl_trans hb_weak x m ∧ is_read (lab m) ∧
clos_refl_trans hb_weak m y ∧ po m y).
Proof.
ins; unfold clos_refl; induction P; desf; eauto.
unfold hb_weak, fence_weak, sync, lwsync, union in × |- ; desf; eauto.
by apply ppo_weaken in H; desf; vauto.
by apply rfe_dom in H; desf; destruct (lab y).
case_eq (is_read (lab y)); ins.
by exploit IHP2; ins; desf; eauto 8 using rt_trans, clos_trans_in_rt.
assert (is_access (lab y)) by (rewrite clos_refl_transE in P2; desf; eauto with access).
assert (is_write (lab y)) by (destruct (lab y); ins); desf.
exploit IHP1; ins; exploit IHP2; ins; desf;
eauto 10 using rt_trans, clos_trans_in_rt.
Qed.
The observation condition is equivalent to the simplified one.
Proposition observation_condition_simplify :
∀ (T: transitive po)
(INCL : inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom)
(CcoT: transitive co)
(ACYC: acyclic hb_power)
(UNI: uniproc_condition),
observation_condition ↔ observation_condition_simpl.
Proof.
split; repeat red; ins; unfold prop in *; desf.
{
apply uniproc_condition_alt in UNI; ins.
red in BASE; unfold seq in *; desc.
exploit fre_dom; eauto; intros (R & W' & EQ).
case_eq (is_write (lab z0)) as W.
by eapply H; eauto; left; repeat eexists; vauto.
rewrite clos_refl_transE in *; desf.
apply inclusion_fence_po in BASE0; auto.
rewrite freE in *; desc.
revert EQ.
unfold rfe, clos_refl in *; desf;
[|exploit loceq_rf; eauto; intros ->; exploit rfe_dom; try edone; vauto;
ins; desc]; ins;
eapply UNI; unfold union, eqloc; eauto 18 using clos_trans with access.
exploit hb_RT; eauto.
by eapply hbp_is_access_l in BASE1; ins; destruct (lab z0).
intro M.
desf; [|by eapply H; eauto; left; repeat eexists; eauto].
assert (po z x) by (eapply T; [eapply inclusion_fence_po|]; eauto).
rewrite freE in *; desf.
exploit loceq_fr; eauto.
unfold rfe, clos_refl in *; desf;
[|exploit loceq_rf; eauto; intros ->; exploit rfe_dom; try edone; vauto;
ins; desc]; ins;
eapply UNI; unfold union, eqloc; eauto 18 using clos_trans with access.
}
unfold union, seq, restr_rel in *; desf; eauto using base_hb_trans.
assert (M: (∃ y', fr x y' ∧ clos_refl rfe y' z0)).
clear - CrfD CcoD CcoT FRE PROP; apply may_chapoE in PROP.
repeat (red in PROP; desf); unfold fre, fr in *; desf; eauto 10.
by eapply CrfD in PROP; eapply CcoD in FRE0; unfold is_write in *; desf.
clear FRE PROP; desc.
destruct (classic (po x y')).
eapply ACYC, t_rt_trans; eauto using t_step, clos_refl_trans, fr_po_hb.
by eapply inclusion_base_hb; eauto with trans.
by eapply (H x y'); [eapply freE|]; eauto with trans.
Qed.
Lemma hb_from_read (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom) x y :
hb_power x y → is_read (lab x) →
po x y ∧ is_access (lab y).
Proof.
split; eauto with access.
unfold hb_power, fence, lwsync, sync, union in *; desf; eauto using ppo_in_po.
by apply rfe_dom in H; ins; desc; destruct (lab x).
Qed.
Lemma is_accessE a : is_access a ↔ is_read a ∨ is_write a.
Proof.
destruct a; ins; intuition.
Qed.
Lemma hbE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom) x y :
hb_power x y ↔
sync x y ∧ is_write (lab x) ∧ is_read (lab y) ∨ hb_weak x y.
Proof.
unfold hb_power, hb_weak, union; rewrite fenceE; intuition.
Qed.
Lemma rt_hbE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom) x y :
clos_refl_trans hb_power x y ↔
∃ z, clos_refl_trans hb_weak x z ∧
(z = y ∨ sync z y ∧ is_write (lab z) ∧ is_read (lab y)).
Proof.
split; ins; desf;
eauto using rt_step with inclusion.
2: by eapply clos_refl_trans_mon; eauto; ins; rewrite hbE; eauto.
2: by eapply rt_trans, rt_step; eauto with inclusion;
eapply clos_refl_trans_mon; eauto; ins; rewrite hbE; eauto.
induction H using clos_refl_trans_ind_left;
try rewrite hbE in *; ins; desf; eauto 6 using clos_refl_trans.
eauto 8 with trans.
exploit hb_from_read; try rewrite hbE; eauto; ins; desf.
rewrite is_accessE in *; desf.
by unfold sync in *; desc; ∃ z0; repeat split; eauto 12 with access.
∃ z; split; eauto; eapply rt_trans, rt_step; eauto.
unfold sync in *; desf; right; left; repeat split; eauto 8 with access.
Qed.
Lemma t_hbE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom) x y :
clos_trans hb_power x y ↔
clos_trans hb_weak x y ∨
∃ z, clos_refl_trans hb_weak x z ∧ sync z y
∧ is_write (lab z) ∧ is_read (lab y).
Proof.
split; ins; desf;
eauto using t_step with inclusion.
2: by eapply clos_trans_mon; eauto; ins; rewrite hbE; eauto.
2: by eapply rt_t_trans, t_step; eauto with inclusion;
eapply clos_refl_trans_mon; eauto; ins; rewrite hbE; eauto.
rewrite t_rt_step in H; desf.
rewrite rt_hbE, hbE in *; desf;
eauto 6 using rt_t_trans, t_step;
eauto 8 using clos_refl_trans with trans.
exploit hb_from_read; try rewrite hbE; eauto; ins; desf.
rewrite is_accessE in *; desf.
by unfold sync in *; desc; right; ∃ z0; repeat split; eauto 12 with access.
left; eapply rt_t_trans, t_step; eauto.
unfold sync in *; desf; right; left; repeat split; eauto 8 with access.
Qed.
Lemma acyclic_hbE
(T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
acyclic hb_power ↔ acyclic hb_weak.
Proof.
split; repeat red; ins; desf.
by eapply H, t_hbE; eauto.
eapply t_hbE in H0; desf; eauto.
eapply hb_weak_TW in H0; eauto.
desf; [by unfold clos_refl, sync in *; desf; eauto|].
eapply (H x), rt_t_trans, t_step; ins; eauto.
right; left; unfold sync, fence_weak in *; split; desf; eauto 6.
Qed.
Lemma sync_fence_weak_trans :
∀ (T: transitive po) a b c
(S : sync a b)
(F: fence_weak b c),
sync a c ∧ is_write (lab a) ∧ is_read (lab c) ∨ fence_weak a c.
Proof.
unfold sync, fence_weak; ins; desc; clear F2.
eapply is_accessE in S2; destruct S2.
right; repeat (eexists; eauto); desf; eauto with access.
desf.
by eapply is_accessE in F2; destruct F2; [left|right]; repeat split; eauto 10 with access.
by right; repeat (eexists; eauto); desf; eauto with access.
Qed.
Lemma fence_weak_sync_trans :
∀ (T: transitive po) a b c
(F: fence_weak a b)
(S : sync b c),
sync a c ∧ is_write (lab a) ∧ is_read (lab c) ∨ fence_weak a c.
Proof.
unfold sync, fence_weak; ins; desc; clear F2; desf.
by right; split; [∃ s|]; repeat split; eauto; desf; eauto with access.
eapply is_accessE in S3; destruct S3.
2: by right; split; [∃ s|]; repeat split; eauto; desf; eauto with access.
eapply is_accessE in F0; destruct F0.
by right; split; [∃ s|]; repeat split; eauto; desf; eauto with access.
left; repeat split; eauto 8.
Qed.
Lemma fence_weak_sync_trans2 :
∀ (T: transitive po) a b c d
(F: fence_weak a b)
(PO: clos_refl po b c)
(S : sync c d),
sync a d ∧ is_write (lab a) ∧ is_read (lab d) ∨ fence_weak a d.
Proof.
unfold clos_refl; ins; desf; eauto using fence_weak_sync_trans.
unfold sync, fence_weak in *; ins; desc; clear F2; desf.
by right; split; [∃ s|]; repeat split; eauto 6; desf; eauto with access.
eapply is_accessE in S3; destruct S3.
2: by right; split; [∃ s|]; repeat split; eauto; desf; eauto with access.
eapply is_accessE in F0; destruct F0.
by right; split; [∃ s|]; repeat split; eauto; desf; eauto with access.
left; repeat split; eauto 9.
Qed.
Lemma sync_trans2 (T: transitive po) a b c d :
sync a b →
clos_refl po b c →
sync c d →
sync a d.
Proof.
unfold sync; ins; desf; ∃ s; repeat split; ins.
unfold clos_refl in *; desf; eauto.
Qed.
Lemma prop_baseE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y :
prop_base x y ↔
prop_base_weak x y ∨ sync x y ∧ is_write (lab x) ∧ is_read (lab y).
Proof.
unfold prop_base, prop_base_weak, seq; split; ins; desf; eauto;
try first [rewrite fenceE in × |- | rewrite fence_weakE in × |-]; desf;
try (by repeat (eexists; try edone); vauto;
eapply clos_refl_trans_mon, inclusion_hb_weak_hb).
rewrite clos_refl_transE in *; desf; eauto 6 using rt_refl.
rewrite t_hbE in *; desf; eauto 8 using clos_trans_in_rt.
eapply hb_weak_TW in H1; ins; desf.
edestruct fence_weak_sync_trans2; desc; eauto 6 using rt_refl.
by red in H; desf; eauto; apply rfe_dom in H; desf; destruct (lab z); ins.
left; repeat (eexists; try edone).
by red in H2; desc; eapply rt_trans, rt_step; eauto; right; left; split; eauto 6.
red in H; desf.
2: by apply rfe_dom in H; desf; destruct (lab z); ins.
assert (is_access (lab y)).
by rewrite clos_refl_transE in *; desf; eauto with access.
rewrite clos_refl_transE in *; desf; vauto.
rewrite t_hbE in *; desf.
eapply hb_weak_RT in H1; ins; desf.
rewrite is_accessE in *; unfold sync in *; desf.
by right; repeat split; ins; eauto 8 with access.
by left; repeat (eexists; vauto); eauto.
by assert (fence_weak z m); [unfold sync in *; desc; split|]; eauto 8.
rewrite clos_refl_transE in H1; desf; eauto using sync_trans.
eapply hb_weak_RT in H1; ins; desf; eauto using sync_trans2.
assert (fence_weak z m) by (unfold sync in *; desc; split; eauto 6).
eapply hb_weak_TW in H8; ins; desf.
by assert (po z0 z1); [red in H8; desf|]; eauto using sync_trans2.
assert (fence_weak m0 y); [unfold sync in *; desc; split|]; eauto 8.
left; repeat (eexists; vauto).
eapply rt_trans, rt_step; [|right; left]; eauto.
Qed.
Lemma base_weak_sync_trans (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b c :
prop_base_weak a b →
sync b c →
prop_base_weak a c
∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).
Proof.
unfold prop_base_weak, seq; ins; desf.
assert (A: is_access (lab b)).
by unfold sync in *; desf.
rewrite is_accessE in *; desf.
left; repeat (eexists; try edone).
eapply rt_trans, rt_step; eauto; right; left.
by unfold sync in *; desc; split; eauto.
eapply hb_weak_TW in H2; desf.
exploit fence_weak_sync_trans2; eauto.
clear H0 H1 H2; intro K; desf; eauto 6 using rt_refl.
by destruct H; desf; eauto; eapply rfe_dom in H;
desc; destruct (lab z).
left; repeat (eexists; try edone).
eapply rt_trans, rt_step; vauto.
right; left; red in H0; desc; split; eauto 6.
Qed.
Lemma sync_expand (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b :
sync a b →
fence_weak a b
∨ sync a b ∧ is_write (lab a) ∧ is_read (lab b).
Proof.
ins; destruct (classic (is_write (lab a) ∧ is_read (lab b)))
as [|N]; eauto.
red in H; desc; left; repeat eexists; vauto.
by rewrite is_accessE in *; desf; eauto; destruct N.
Qed.
Lemma prop_base_weak_hb_weak_trans a b c :
prop_base_weak a b →
clos_refl_trans hb_weak b c →
prop_base_weak a c.
Proof.
unfold sync, prop_base_weak, seq; ins; desf; eauto 8 using rt_trans.
Qed.
Lemma sync_hb_sync :
∀ (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b c d
(S: sync a b)
(C: clos_refl_trans hb_weak b c)
(S': sync c d),
prop_base_weak a c ∧ sync c d ∨
sync a b ∧ clos_refl_trans hb_weak b d ∨
sync a d ∧ is_write (lab a) ∧ is_read (lab d).
Proof.
ins; eapply sync_expand in S; desf; vauto.
by left; split; ins; eexists; split; vauto.
eapply sync_expand in S'; desf.
by right; left; split; ins;
eapply rt_trans, rt_step, inclusion_fence_hb_weak; eauto.
eapply hb_weak_TW in C; desf; eauto 8 using sync_trans2, rt_refl.
red in S'; desc; right; left; split; ins; eapply rt_trans, rt_step; eauto.
by right; left; split; eauto 6.
Qed.
Lemma rt_prop_baseE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(P: clos_refl_trans prop_base x y) :
clos_refl_trans prop_base_weak x y ∨
∃ z,
clos_refl_trans prop_base_weak x z ∧
∃ w,
sync z w ∧ clos_refl_trans hb_weak w y.
Proof.
induction P using clos_refl_trans_ind_left; eauto using clos_refl_trans.
clear P; rewrite prop_baseE in *; desf;
eauto 6 using rt_refl;
eauto 8 using rt_trans, rt_step, inclusion_base_hb_weak.
edestruct sync_hb_sync; des; eauto 6 using clos_refl_trans.
right; eauto 8 using clos_refl_trans, prop_base_weak_hb_weak_trans.
Qed.
We prove that the two definitions of the propagation order are equivalent.
Lemma propE (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y :
prop x y ↔ prop_weak x y.
Proof.
unfold prop, prop_weak, restr_rel, seq, union; split; ins; desf; eauto;
try rewrite prop_baseE in *; desf; eauto 10.
by destruct (lab y).
{
right; eexists; split; eauto; clear H.
rename H0 into L; eapply rt_prop_baseE in L; ins.
rename H2 into K; eapply rt_hbE in K; ins; desf; eauto.
by edestruct sync_hb_sync with (a:= z3) (d := z1); desf;
eauto 8 using clos_refl_trans, prop_base_weak_hb_weak_trans.
by edestruct sync_hb_sync with (a:= z0) (d := y); desf;
eauto 8 using clos_refl_trans, prop_base_weak_hb_weak_trans.
edestruct sync_hb_sync with (a:= z3) (d := z1) as [M|M]; eauto;
clear L0 L1 H1; desf.
by edestruct sync_hb_sync with (a := z0) (d := y); desf;
eauto; clear K K0 M0; eauto 9 using clos_refl_trans.
by edestruct sync_hb_sync with (a := z3) (c:=z2) (d := y); desf;
eauto using rt_trans; clear K K0 M0; eauto 9 using clos_refl_trans.
by edestruct sync_hb_sync with (a := z3) (c:=z2) (d := y); desf;
eauto using rt_trans; clear K K0 M0; eauto 9 using clos_refl_trans.
}
right; repeat (eexists; try edone);
eapply clos_refl_trans_mon; ins; eauto with inclusion.
by rewrite prop_baseE; eauto.
Qed.
As a result, we can further simplify the observation condition.
Lemma observation_condition_alternative :
∀ (T: transitive po)
(INCL : inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom)
(UNI: uniproc_condition),
observation_condition_simpl ↔ observation_condition_alt.
Proof.
split; red; ins; eapply H; eauto;
rewrite prop_baseE in *; desf; eauto.
rewrite freE in *; unfold sync in *; desf.
exploit fr_dom; eauto; ins; desf.
apply uniproc_condition_alt in UNI; ins.
edestruct (UNI x); unfold union, eqloc;
eapply t_trans; apply t_step; eauto 6 with access.
Qed.
Lemma sync_base_weak_trans (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b c :
sync a b →
prop_base_weak b c →
is_read (lab b) →
prop_base_weak a c ∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).
Proof.
unfold prop_base_weak, clos_refl, seq; ins; desf.
2: by eapply rfe_dom in H0; desf; destruct (lab b).
exploit sync_fence_weak_trans; eauto.
intro M; desf; eauto 10.
rewrite clos_refl_transE in *; desf; eauto.
edestruct hb_weak_RT as [N|N]; eauto; desf.
assert (is_access (lab c)) by eauto with access.
rewrite is_accessE in *; desf.
by right; repeat split; ins; unfold sync in M |- *; desf; eauto 8 with access.
red in M; desc; left; eexists; split; vauto; eexists; split; vauto.
by red; split; eauto 6.
left; eexists; split; vauto; eexists; split; eauto.
red; unfold sync in M; desf; split; vauto; eauto 6.
Qed.
Lemma sync_rt_base_weak_trans (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b c :
sync a b →
clos_refl_trans prop_base_weak b c →
is_read (lab b) →
clos_refl_trans prop_base_weak a c
∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).
Proof.
ins.
assert (is_access (lab a)) by (unfold sync in *; desf).
rewrite is_accessE in *; desf.
left; eapply rt_trans; eauto.
by unfold sync in *; desc; eapply rt_step; repeat eexists; vauto.
rewrite clos_refl_transE in *; ins; desf; eauto.
eapply clos_trans_of_transitive in H0; try red; eauto using prop_base_weak_trans.
edestruct sync_base_weak_trans; desc; eauto using t_step.
Qed.
Lemma rt_base_weak_sync_trans (T: transitive po)
(CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
(INCL: inclusion deps po)
a b c :
clos_refl_trans prop_base_weak a b →
sync b c →
is_write (lab b) →
clos_refl_trans prop_base_weak a c
∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).
Proof.
ins.
assert (is_access (lab c)) by (unfold sync in *; desf).
rewrite is_accessE in *; desf.
rewrite clos_refl_transE in *; ins; desf; eauto.
eapply clos_trans_of_transitive in H; try red; eauto using prop_base_weak_trans.
edestruct base_weak_sync_trans; desc; eauto using t_step.
left; eapply rt_trans; eauto.
by unfold sync in *; desc; eapply rt_step; repeat (eexists; vauto).
Qed.
Notation "P +++ Q" := (union P Q) (at level 50, left associativity).
Lemma propE2 (T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
prop <--> prop_weak.
Proof.
by split; red; ins; rewrite propE in *; ins.
Qed.
Lemma propagation_simpl1
(T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
acyclic (co +++ prop) ↔
acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
+++ (seq (seq (clos_refl fre) (clos_refl rfe))
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak))))).
Proof.
rewrite propE2; ins.
unfold prop_weak; rewrite may_chapoE.
unfold union, seq, coe.
split; intros A x P; apply (A x); revert P;
generalize x at 1 3; induction 1; desf; eauto using clos_trans.
by eapply t_step; unfold clos_refl in *; desf; eauto 14.
red in H; unfold clos_refl at 1; desf; eauto 14 using t_step.
eapply t_trans; eapply t_step; eauto 14.
Qed.
Lemma inclusion_base_weak_base :
inclusion prop_base_weak prop_base.
Proof.
unfold inclusion, prop_base, prop_base_weak, seq; ins; desf;
repeat eexists; eauto; try rewrite fenceE; eauto.
by eapply clos_refl_trans_mon, inclusion_hb_weak_hb.
Qed.
Lemma prop_base_so_trans so :
transitive (prop_base_so so).
Proof.
unfold prop_base_so, hb_so, union, seq; red; ins; desf.
repeat (eexists; try edone).
eapply rt_trans, rt_trans; eauto.
eapply rt_trans with z0, rt_step.
by red in H0; desf; eauto using clos_refl_trans with inclusion.
by destruct H1; desf; eauto with inclusion.
Qed.
Lemma inclusion_fence_so so : inclusion fence_weak (fence_so so).
Proof. vauto. Qed.
Lemma inclusion_hb_so so : inclusion hb_weak (hb_so so).
Proof. vauto. Qed.
Lemma inclusion_base_so so :
inclusion prop_base_weak (prop_base_so so).
Proof.
unfold prop_base_weak, prop_base_so, union, seq; red; ins; desf.
repeat (eexists; try edone).
eby eapply inclusion_fence_so.
by eapply clos_refl_trans_mon, inclusion_hb_so.
Qed.
Lemma inclusion_fence_hb_so so : inclusion (fence_so so) (hb_so so).
Proof.
unfold fence_so, hb_so, union; red; ins; desf; eauto with inclusion.
Qed.
Lemma inclusion_base_hb_so so :
inclusion (prop_base_so so) (clos_trans (hb_so so)).
Proof.
unfold prop_base_so, union, seq; red; ins; desf.
eapply t_rt_trans; eauto.
eapply rt_t_trans with z, t_step, inclusion_fence_hb_so; ins.
by unfold hb_so, union; red in H; desf;
eauto using clos_refl_trans with inclusion.
Qed.
Hint Resolve inclusion_fence_so : inclusion.
Hint Resolve inclusion_hb_so : inclusion.
Hint Resolve inclusion_base_so : inclusion.
Hint Resolve inclusion_fence_hb_so : inclusion.
Hint Resolve inclusion_base_hb_so : inclusion.
Lemma so_sync_case_split :
∀ so (CsoF : is_total (fun a : actid ⇒ lab a = Async) so)
(T : transitive so)
(IRR: irreflexive so)
x y (S: union (so_step so) sync x y)
z w (S': union (so_step so) sync z w),
sync x w ∧ sync z y ∨ so_step so x w ∨ so_step so z y.
Proof.
unfold so_step, sync, union; ins; desf.
destruct (eqP f f0) as [|NEQ]; desf; eauto 10.
by eapply CsoF in NEQ; desf; eauto 10.
destruct (eqP s f) as [|NEQ]; desf; eauto 10.
by eapply CsoF in NEQ; desf; eauto 10.
destruct (eqP s f) as [|NEQ]; desf; eauto 10.
by eapply CsoF in NEQ; desf; eauto 10.
destruct (eqP s s0) as [|NEQ]; desf.
left; repeat split; eauto 10.
by eapply CsoF in NEQ; desf; eauto 10.
Qed.
Lemma rfe_base_so_trans (CrfD: ConsistentRF_dom) so a b c:
rfe a b →
prop_base_so so b c →
prop_base_so so a c.
Proof.
unfold prop_base_so, rfe, seq, clos_refl; ins; desf; eauto 8.
eapply CrfD in H; eapply CrfD in H0; desf; congruence.
Qed.
Lemma rrfe_base_so_trans (CrfD: ConsistentRF_dom) so a b c:
clos_refl rfe a b →
prop_base_so so b c →
prop_base_so so a c.
Proof.
unfold clos_refl; ins; desf; eauto using rfe_base_so_trans.
Qed.
Lemma helper_so_irreflexive :
∀ (T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) so
(CsoF : is_total (fun a ⇒ lab a = Async) so)
(CsoT : transitive so)
(CsoI : irreflexive so)
(UNI: uniproc_condition)
(NTA: acyclic (hb_so so))
(OBS: ∀ x y, fre x y → prop_base_so so y x → False),
irreflexive
(seq (seq (clos_refl fre) (clos_refl rfe))
(seq (clos_refl_trans prop_base_weak)
(seq (so_step so +++ sync) (clos_refl_trans hb_weak)))).
Proof.
unfold seq; red; ins; desf.
red in H; desf; red in H1; desf.
eapply (NTA z1).
eapply rt_t_trans with z, rt_t_trans with z0, t_rt_trans;
eauto using clos_trans, clos_refl_trans_mon, inclusion_hb_so with inclusion.
by red in H3; desf; vauto; eapply rt_step, inclusion_hb_so; vauto.
eapply clos_refl_trans_mon, inclusion_hb_so.
by clear - H0; induction H0; eauto using clos_refl_trans, inclusion_base_hb_weak.
by vauto.
by eapply clos_refl_trans_mon, inclusion_hb_so.
eapply acyclic_mon with (rel' := hb_weak) in NTA; eauto using inclusion_hb_so.
rewrite <- acyclic_hbE in *; ins.
eapply (NTA z1).
eapply rt_t_trans with z, rt_t_trans with z0, t_rt_trans;
eauto using clos_trans, clos_refl_trans_mon, inclusion_hb_weak_hb with inclusion.
by red in H3; desf; eauto using clos_refl_trans with inclusion.
by clear H1 H2 H3; induction H0; eauto using clos_refl_trans, inclusion_base_weak_hb.
eapply OBS; eauto.
eapply rrfe_base_so_trans; eauto.
eapply (ct_of_transitive (@prop_base_so_trans so)), rt_t_trans, t_step.
eby eapply clos_refl_trans_mon, inclusion_base_so.
eexists; split; vauto; eexists z2; split; vauto.
by eapply clos_refl_trans_mon, inclusion_hb_so.
assert (OBS': observation_condition_alt).
eby red; ins; eapply OBS, inclusion_base_so.
eapply observation_condition_alternative in OBS'; eauto.
eapply OBS'; eauto.
eapply rrfe_base_trans; eauto.
eapply (ct_of_transitive prop_base_trans), rt_t_trans with z0, t_step.
by eapply clos_refl_trans_mon, inclusion_base_weak_base.
eexists; split; vauto; ∃ z2; split; vauto.
by eapply clos_refl_trans_mon, inclusion_hb_weak_hb.
Qed.
Lemma helper_so_transitive :
∀ (T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) so
(CsoF : is_total (fun a ⇒ lab a = Async) so)
(CsoT : transitive so)
(CsoI : irreflexive so)
(UNI: uniproc_condition)
(NTA: acyclic (hb_so so))
(OBS: ∀ x y, fre x y → prop_base_so so y x → False),
transitive
(seq (seq (clos_refl fre) (clos_refl rfe))
(seq (clos_refl_trans prop_base_weak)
(seq (union (so_step so) sync) (clos_refl_trans hb_weak)))).
Proof.
red; unfold seq; ins; desc.
edestruct so_sync_case_split with (x := z5) (z := z2); desc; eauto;
unfold union; desf; eauto 15.
edestruct helper_so_irreflexive with (x := y); eauto.
by unfold seq, union; eauto 15.
Qed.
Lemma propagation_expand
(T: transitive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
acyclic (co +++ prop) ↔
acyclic (seq (seq (clos_refl fre) (clos_refl rfe))
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak)))) ∧
acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
+++ restr_rel (fun x ⇒ is_write (lab x))
(clos_trans
(seq (seq (clos_refl fre) (clos_refl rfe))
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak)))))).
Proof.
rewrite propagation_simpl1; ins; unfold union, seq.
split.
intros A; split; intros x P; apply (A x); revert P;
generalize x at 1 3; induction 1; desf; eauto using clos_trans.
by eapply t_step; unfold clos_refl in *; desf; eauto 14.
by red in H; desf; eapply clos_trans_mon; eauto.
intros [A B] a CYC.
eapply cycle_ur with (adom:= fun x ⇒ is_write (lab x)) in CYC; desf; eauto;
try (by unfold restr_rel; ins; desf; eapply CcoD in R; desf).
Qed.
Completeness of the model with a total order on syncs with respect to the
default Power model.
Lemma SyncTotal_complete
(INCL: inclusion deps po) so
(C: ConsistentSyncTotal so) :
ConsistentPower.
Proof.
assert (K:=C); red in K; red; ins; desf; unnw.
assert (acyclic hb_power).
by eapply acyclic_hbE, acyclic_mon; try exact NTA; vauto.
intuition.
{
rewrite observation_condition_simplify,
observation_condition_alternative; eauto.
red; ins; eapply OBS, inclusion_base_so; eauto.
}
{
eapply propagation_expand; ins; split.
eapply acyclic_mon.
by eapply trans_irr_acyclic, helper_so_transitive;
eauto using helper_so_irreflexive.
by unfold seq, union; clear; red; ins; desf; eauto 15.
intros x P; eapply (PROP x), clos_trans_mon; eauto; clear x P.
unfold union, prop_so, restr_rel; ins; desf; eauto;
right; right; split; ins; [by eapply inclusion_base_so|].
eapply clos_trans_mon, clos_trans_of_transitive in H0.
2: by eapply helper_so_transitive; eauto.
2: by unfold seq, union; ins; desf; eauto 15.
unfold seq, union in *; desc.
destruct H0; clarify; [|by apply fre_dom in H0; desc; destruct (lab a)].
eapply rrfe_base_so_trans; eauto.
eapply (ct_of_transitive (@prop_base_so_trans so)), rt_t_trans, t_step.
eby eapply clos_refl_trans_mon, inclusion_base_so.
desf.
eexists; split; vauto; eexists z2; split; vauto.
eby eapply clos_refl_trans_mon, inclusion_hb_so.
assert (prop_base z0 b).
eexists z0; split; vauto; eexists; split; vauto.
eby eapply clos_refl_trans_mon, inclusion_hb_weak_hb.
by eapply inclusion_base_so; rewrite prop_baseE in H0; desf; destruct (lab b).
}
Qed.
For the soundness direction, we use the following auxiliary definition.
Definition Trel :=
restr_rel (fun x ⇒ lab x = Async)
(seq (seq po (clos_refl_trans hb_weak))
(seq (clos_refl_trans (co +++ prop_weak))
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak) po)))).
Lemma helper_prop_alt_restr
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
restr_rel (fun x : actid ⇒ ¬ is_access (lab x))
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq
(fun x y ⇒
∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
(clos_refl_trans hb_weak))))
<-->
restr_rel (fun x : actid ⇒ ¬ is_access (lab x))
(fun x y ⇒ ∃ s, po x s ∧ po s y ∧ lab s = Async).
Proof.
unfold seq, clos_refl, restr_rel; split; red; ins; desf; eauto 15 using rt_refl.
2: by exploit chapo_access; eauto; ins; desf.
rewrite clos_refl_transE in H4; desf; try by (exfalso; eauto with access).
rewrite (crt_of_transitive prop_base_weak_trans) in H2.
red in H2; desf; eauto 6; apply inclusion_base_hb_weak in H2.
rewrite clos_refl_transE in H2; desf; eauto 6 with access.
exfalso; eauto with access.
Qed.
Lemma seqA2 X (r r' r'' : relation X) x y :
seq (seq r r') r'' x y ↔ seq r (seq r' r'') x y.
Proof.
unfold seq; split; ins; desf; eauto 8.
Qed.
Lemma helper1 :
∀
(T: transitive po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(R : clos_trans
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq
(fun x y : actid ⇒
∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
(clos_refl_trans hb_weak)))) x y)
(ACC : is_access (lab y)),
seq
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq
(fun x y : actid ⇒
∃ s, po x s ∧ po s y ∧ lab s = Async
∧ is_access (lab y))
(clos_refl_trans hb_weak))))
(clos_refl_trans
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak))))) x y.
Proof.
ins; apply clos_trans_t1n in R; induction R.
eexists; split; vauto.
unfold seq in *; desf; repeat (eexists; try edone).
rewrite clos_refl_transE in H2; desf; eauto with access.
specialize (IHR ACC); clear R.
unfold seq in H; desc.
do 2 (rewrite seqA2; eexists; split; try edone); clear H H0 ACC.
rewrite seqA2.
unfold seq in *; desf.
assert (z2 = z5 ∨ is_access (lab z2)).
rewrite clos_refl_transE in H2; desf;
[red in IHR; desf;
[apply (inclusion_rt_rt2 inclusion_base_hb_weak) in IHR1;
rewrite clos_refl_transE in IHR1; desf|]|]; eauto with access.
by eapply chapo_access in IHR; desf; eauto.
desf; [by ∃ z6; repeat eexists; eauto|].
(repeat (eexists; split); try edone).
eapply rt_trans; [apply rt_step|]; eauto.
repeat (eexists; try edone).
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in IHR1.
rewrite clos_refl_transE in IHR1; desf; eauto with access.
red in IHR; desf; [|by eapply chapo_access in IHR; desf; eauto].
rewrite clos_refl_transE in H2; desf; eauto with access.
Qed.
Lemma helper2 :
∀
(T: transitive po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y
(R : clos_trans
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq
(fun x y : actid ⇒
∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
(clos_refl_trans hb_weak)))) x y)
(ACC : is_access (lab x))
(ACC : is_access (lab y)),
clos_trans
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak)))) x y.
Proof.
ins; eapply helper1 in R; ins; red in R; desc.
eapply t_rt_trans; eauto; apply t_step.
clear R0; unfold seq in *; desc.
repeat (eexists; try edone).
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in R0.
rewrite clos_refl_transE in R0; desf; eauto with access.
red in R; desf; eapply chapo_access in R; desf; eauto.
Qed.
Lemma acyclic_prop_alt
(T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
acyclic (co +++ prop) ↔
acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
+++ seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq (fun x y ⇒ ∃ s, po x s ∧ po s y ∧ lab s = Async)
(clos_refl_trans hb_weak)))).
Proof.
rewrite propE2; ins.
unfold prop_weak, union; split; ins.
2: by eapply acyclic_mon; eauto; unfold union, seq, sync;
intros x y J; desf; eauto 15.
intros x CYC.
eapply cycle_ur with (adom:= fun x ⇒ is_write (lab x)) in CYC; desf; eauto;
try (by unfold restr_rel; ins; desf; eapply CcoD in R; desf).
eapply acyclic_case_split with (f := fun x ⇒ ¬ is_access (lab x)) in CYC; ins.
clear x CYC; rewrite helper_prop_alt_restr; ins.
split.
apply acyclic_mon with (rel:=po); eauto using trans_irr_acyclic.
by unfold restr_rel; red; ins; desc; eauto.
ins; apply NEG; clear NEG; intro ACC.
eapply helper2 in CYC; eauto using t_step.
by eapply H, clos_trans_mon; eauto.
eapply H, clos_trans_of_clos_trans, clos_trans_mon; eauto.
clear H x x0 CYC; ins; desf; eauto using t_step.
eapply helper2 in H; eauto with access.
by eapply clos_trans_mon; eauto.
Qed.
Lemma inclusion_base_weak_hb2 :
inclusion prop_base_weak (clos_trans hb_weak).
Proof.
unfold prop_base_weak, seq; red; ins; desc.
eapply rt_t_trans, t_rt_trans; [|eapply t_step|]; eauto with inclusion.
red in H; desf; eauto using rt_refl, rt_step with inclusion.
Qed.
Lemma helper_prop_access
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) a b :
seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq sync (clos_refl_trans hb_weak))) a b →
is_access (lab a) ∧ is_access (lab b).
Proof.
unfold seq; ins; desf.
eapply (crt_of_transitive prop_base_weak_trans) in H0.
unfold clos_refl, sync in *; rewrite clos_refl_transE in *; desf;
try eapply chapo_access in H; ins; desf;
try eapply inclusion_base_weak_hb2 in H0; ins; desf;
eauto with access.
Qed.
Lemma coprop_access
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) a b :
clos_trans (co +++ prop_weak) a b →
is_access (lab a) ∧ is_access (lab b).
Proof.
unfold seq, prop_weak, union, restr_rel; ins; desf.
split.
rewrite t_step_rt in *; desf.
by eapply CcoD in H; desf; eauto with access.
by eapply inclusion_base_weak_hb2 in H; eauto with access.
by eapply helper_prop_access in H; desf.
rewrite t_rt_step in *; desf.
by eapply CcoD in H0; desf; eauto with access.
by eapply inclusion_base_weak_hb2 in H0; eauto with access.
by eapply helper_prop_access in H0; desf.
Qed.
From the propagation axiom, we get that Trel is acyclic.
Lemma acyclic_Trel
(T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom)
(H : acyclic (co +++ prop)) :
acyclic Trel.
Proof.
unfold Trel; ins.
eapply trans_irr_acyclic.
rewrite acyclic_prop_alt in *; ins.
red; unfold seq, restr_rel; ins; desf.
eapply H, rt_t_trans, t_step; eauto.
2: by right; repeat (eexists; vauto).
eapply clos_refl_trans_mon; eauto.
by clear; unfold prop_weak, union, sync, seq; ins; desf; eauto 15.
unfold restr_rel, transitive; ins; desc; split; ins.
rename H0 into M, H1 into N; rewrite seqA2 in ×.
destruct M as (x1 & X & M), N as (y1 & Y & N).
rewrite <- !seqA2 in M, N.
destruct M as (yp & M & Y'), N as (zp & N & Z').
assert (A: x1 = yp ∨ is_access (lab yp)).
unfold seq in M; desc.
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in M0.
rewrite clos_refl_transE in M0; desf; eauto with access.
red in M1; desf; [|by eapply chapo_access in M1; desf; eauto].
rewrite clos_refl_transE in M2; desf.
by rewrite clos_refl_transE in M; desf; eauto with access.
by eapply coprop_access in M2; desf; eauto.
desf.
by ∃ y1; split; eauto; rewrite <- !seqA2 in *; ∃ zp; eauto.
assert (B: y1 = zp ∨ is_access (lab y1)).
unfold seq in N; desc.
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in N0.
rewrite clos_refl_transE in N; desf; eauto with access.
rewrite clos_refl_transE in N2; desf.
2: by eapply coprop_access in N2; desf; eauto.
red in N1; desf; [|by eapply chapo_access in N1; desf; eauto].
by rewrite clos_refl_transE in N0; desf; eauto with access.
desf.
by ∃ x1; split; eauto; rewrite <- !seqA2 in *; ∃ yp; eauto.
∃ x1; split; eauto; rewrite <- !seqA2 in *; ∃ zp; split; eauto.
do 2 (red in N; desc; eexists; split; eauto); clear N0 N1.
rewrite !seqA2 in *; red in M; desc; eexists; split; eauto; clear M.
unfold seq in *; desc; eapply rt_trans, rt_trans; eauto.
apply rt_step; right; right; repeat (eexists; try edone).
Qed.
Lemma so_step_trans so
(CsoF: is_total (fun a ⇒ lab a = Async) so)
(CsoT: transitive so)
(Cww: ∀ x y (SO : so_step so x y)
(HB: clos_refl_trans hb_weak y x), False) a b
(A: so_step so a b) c
(B: clos_refl_trans hb_weak b c) d
(C: so_step so c d) :
so_step so a d.
Proof.
unfold so_step in *; desc.
destruct (eqP f f'0) as [|N]; [|eapply CsoF in N]; desf; eauto 10.
edestruct (Cww c b); eauto 10 using rt_trans.
Qed.
Lemma rt_hb_soE so
(CsoF: is_total (fun a ⇒ lab a = Async) so)
(CsoT: transitive so)
(Cww: ∀ x y (SO : so_step so x y)
(HB: clos_refl_trans hb_weak y x), False) :
clos_refl_trans (hb_so so) <-->
seq (clos_refl_trans hb_weak)
(seq (clos_refl (so_step so)) (clos_refl_trans hb_weak)).
Proof.
unfold hb_so, union, seq; split; red; ins.
rename H into J;
induction J; desf; eauto 6 using clos_refl_trans.
unfold clos_refl in IHJ0; desf; eauto 7 using clos_refl_trans.
unfold clos_refl in IHJ4; desf; eauto 7 using clos_refl_trans.
by eapply so_step_trans in IHJ0; eauto using rt_trans.
desf; eapply rt_trans, rt_trans; eauto using clos_refl_trans_mon;
unfold clos_refl in *; desf; vauto.
Qed.
Lemma t_hb_soE so
(CsoF: is_total (fun a ⇒ lab a = Async) so)
(CsoT: transitive so)
(OTH: ∀ x y (SO : so_step so x y)
(HB: clos_refl_trans hb_weak y x), False) :
clos_trans (hb_so so) <-->
union (clos_trans hb_weak)
(seq (clos_refl_trans hb_weak)
(seq (so_step so) (clos_refl_trans hb_weak))).
Proof.
unfold hb_so, union, seq; split; red; ins.
rewrite t_step_rt in *; desf; eapply rt_hb_soE in H0;
ins; unfold seq, clos_refl in *; desf;
eauto 8 using rt_trans, rt_step;
eauto 8 using rt_trans, rt_refl.
by eapply so_step_trans in H0; eauto 8 using rt_refl.
desf; eauto using clos_trans_mon.
eapply rt_t_trans, t_rt_trans; eauto using clos_refl_trans_mon;
vauto.
Qed.
Lemma seq_union_l X (r1 r2 r : relation X) :
seq (r1 +++ r2) r <--> seq r1 r +++ seq r2 r.
Proof.
unfold seq, union; split; red; ins; desf; eauto.
Qed.
Lemma seq_union_r X (r r1 r2 : relation X) :
seq r (r1 +++ r2) <--> seq r r1 +++ seq r r2.
Proof.
unfold seq, union; split; red; ins; desf; eauto.
Qed.
Lemma seqA X (r1 r2 r3 : relation X) :
seq (seq r1 r2) r3 <--> seq r1 (seq r2 r3).
Proof.
unfold seq, union; split; red; ins; desf; eauto.
Qed.
Lemma unionA X (r1 r2 r3 : relation X) :
union (union r1 r2) r3 <--> union r1 (union r2 r3).
Proof.
unfold seq, union; split; red; ins; desf; eauto.
Qed.
Lemma unionC X (r1 r2 : relation X) :
union r1 r2 <--> union r2 r1.
Proof.
unfold seq, union; split; red; ins; desf; eauto.
Qed.
Lemma base_soE so
(CsoF: is_total (fun a ⇒ lab a = Async) so)
(CsoT: transitive so)
(OTH: ∀ x y (SO : so_step so x y)
(HB: clos_refl_trans hb_weak y x), False) :
prop_base_so so <-->
union
(seq (clos_refl rfe) (seq (so_step so) (clos_refl_trans hb_weak)))
(seq prop_base_weak (seq (clos_refl (so_step so)) (clos_refl_trans hb_weak))).
Proof.
unfold prop_base_so, prop_base_weak, fence_so.
rewrite !seq_union_l, !seq_union_r, rt_hb_soE, !seqA, unionC; ins.
eapply union_mor; try reflexivity.
unfold seq; split; red; ins; desf; eauto 10 using rt_refl.
red in H2; desf; eauto 7 using rt_trans.
by eapply so_step_trans in H1; eauto.
Qed.
Lemma base_soE2 so
(CsoF: is_total (fun a ⇒ lab a = Async) so)
(CsoT: transitive so)
(OTH: ∀ x y (SO : so_step so x y)
(HB: clos_refl_trans hb_weak y x), False) :
prop_base_so so <-->
union prop_base_weak
(union (seq rfe (seq (so_step so) (clos_refl_trans hb_weak)))
(seq (clos_refl prop_base_weak) (seq (so_step so) (clos_refl_trans hb_weak)))).
Proof.
rewrite base_soE; ins.
unfold clos_refl, union, seq; split; red; ins; desf; eauto 8;
eauto 8 using rt_refl, prop_base_weak_hb_weak_trans.
Qed.
We define some further auxiliary definitions, which help us reason about
paths involving sync edges.
Definition sync_ext_l x y := po x y ∧ is_access (lab x) ∧ lab y = Async.
Definition sync_ext_r x y := po x y ∧ lab x = Async ∧ is_access (lab y).
Definition sync_ext := union sync (union sync_ext_l sync_ext_r).
Definition fence_ext := union fence (union sync_ext_l sync_ext_r).
Definition hb_ext := union ppo (union fence_ext rfe).
Definition prop_base_ext :=
(seq (clos_refl rfe) (seq fence_ext (clos_refl_trans hb_ext))).
Definition prop_ext :=
union (restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak)
(seq (clos_refl chapo)
(seq (clos_refl_trans prop_base_weak)
(seq sync_ext (clos_refl_trans hb_weak)))).
Lemma prop_extE
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
prop_ext <-->
prop_weak +++
seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l) +++
seq (sync_ext_r) (clos_refl_trans hb_weak).
Proof.
unfold prop_ext, prop_weak, sync_ext.
rewrite !seq_union_l, !seq_union_r; unfold union; split; red; ins; desf; eauto.
left; right; unfold seq in *; desf.
rewrite clos_refl_transE in H2; desf; eauto.
by apply hb_weakp_is_access_l in H2; ins; red in H1; desf; destruct (lab z1).
right; unfold seq in *; desf.
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in H0.
rewrite clos_refl_transE in H0; desf; eauto.
2: by apply hb_weakp_is_access_r in H0; ins; red in H1; desf; destruct (lab z0).
by red in H; desf; eauto; apply chapo_access in H; desc;
red in H1; desf; destruct (lab z0).
by unfold seq in *; desf; eauto 10 using rt_refl.
by unfold seq in *; desf; eauto 10 using rt_refl.
Qed.
We prove a few basic lemmas that allow us to perform equational reasoning.
Lemma seq_sync :
seq sync_ext_l sync_ext_r <--> sync.
Proof.
unfold seq, sync, sync_ext_r, sync_ext_l.
split; red; ins; desf; eauto 8.
Qed.
Lemma seq_sync_ext_l :
seq sync_ext_l sync_ext_l <--> (fun _ _ ⇒ False).
Proof.
unfold seq, sync, sync_ext_r, sync_ext_l.
by split; red; ins; desf; eauto 8; destruct (lab z).
Qed.
Lemma seq_sync_ext_r :
seq sync_ext_r sync_ext_r <--> (fun _ _ ⇒ False).
Proof.
unfold seq, sync, sync_ext_r, sync_ext_l.
by split; red; ins; desf; eauto 8; destruct (lab z).
Qed.
Lemma seq_sync_ext_chapo
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
seq sync_ext_l (clos_refl chapo) <--> sync_ext_l.
Proof.
unfold seq, sync_ext_l, clos_refl; split; red; ins; desf; eauto 6.
apply chapo_access in H0; desf; destruct (lab z); ins.
Qed.
Lemma seq_sync_ext_base_star
(CrfD: ConsistentRF_dom) :
seq sync_ext_l (clos_refl_trans prop_base_weak) <--> sync_ext_l.
Proof.
unfold seq, sync_ext_l, clos_refl; split; red; ins; desf;
eauto 6 using clos_refl_trans.
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in H0.
rewrite clos_refl_transE in *; desf; try rewrite H2 in *; desf.
by eapply hb_weakp_is_access_l in H0; try rewrite H2 in *; desf.
Qed.
Lemma seq_hb_weak_star_sync_ext
(CrfD: ConsistentRF_dom) :
seq (clos_refl_trans hb_weak) sync_ext_r <--> sync_ext_r.
Proof.
unfold seq, sync_ext_r, clos_refl; split; red; ins; desf;
eauto 6 using clos_refl_trans.
rewrite clos_refl_transE in *; desf; try rewrite H1 in *; desf.
by eapply hb_weakp_is_access_r in H; try rewrite H1 in *; desf.
Qed.
Lemma coprop_extE
(T: transitive po)
(IRR: irreflexive po)
(INCL: inclusion deps po)
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) :
acyclic (co +++ prop_ext) ↔
acyclic (co +++ prop_weak).
Proof.
rewrite prop_extE; ins; split; ins.
by unfold union in *; eapply acyclic_mon; eauto; red; ins; desf; eauto.
assert (A: seq
(seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l))
(seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l))
<--> (fun _ _ : actid ⇒ False)).
rewrite !seqA, <- (seqA sync_ext_l), seq_sync_ext_chapo,
<- (seqA sync_ext_l), seq_sync_ext_base_star, seq_sync_ext_l, !seqrF; ins;
reflexivity.
assert (B: seq (seq sync_ext_r (clos_refl_trans hb_weak))
(seq sync_ext_r (clos_refl_trans hb_weak)) <-->
(fun _ _ : actid ⇒ False)).
rewrite !seqA, <- (seqA _ sync_ext_r), seq_hb_weak_star_sync_ext,
<- seqA, seq_sync_ext_r, !seqFr; ins;
reflexivity.
rewrite !unionA, <- unionA.
intros x J; eapply cycle_ur with (adom := fun x ⇒ is_access (lab x)) in J;
try (by ins; apply t_step with (R := co +++ prop_weak), coprop_access in R; desf).
desf.
eapply acyclic_unc in J; ins.
rewrite !seqA, <- (seqA sync_ext_l), seq_sync.
by eapply acyclic_mon; eauto; vauto.
eapply H, clos_trans_of_clos_trans, clos_trans_mon; eauto; clear x x0 J.
instantiate; ins; desf; vauto.
eapply pathp_unc in H0; ins; unfold union in H0; desf.
rewrite !seqA, <- (seqA sync_ext_l), seq_sync in H0.
by eapply clos_trans_mon; eauto; vauto.
by apply t_step_rt in H0; unfold seq, sync_ext_r in H0; desf; destruct (lab a).
by exfalso; unfold seq, sync_ext_l in H0; desf;
rewrite clos_refl_transE, t_rt_step in *; desf; destruct (lab b).
by exfalso; unfold seq, sync_ext_r in H0; desf; destruct (lab a).
Qed.
Lemma helper_restr1
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) r :
restr_rel (fun x : actid ⇒ lab x ≠ Async)
(restr_rel (fun x ⇒ lab x = Async) r +++ co +++ prop_ext)
<-->
restr_rel (fun x : actid ⇒ lab x ≠ Async)
(co +++ prop_weak).
Proof.
rewrite prop_extE, <- !union_restr; ins.
unfold restr_rel, union, seq, sync_ext_l, sync_ext_r;
split; red; ins; desf; eauto 8.
Qed.
Lemma prop_ext_sync_r :
∀
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y (L: lab y = Async),
prop_ext x y ↔
seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l) x y.
Proof.
ins; split; ins; [apply prop_extE in H|apply prop_extE];
unfold union, seq in *; desf; eauto 8.
by unfold prop_weak, restr_rel, union in *; desf;
[|apply helper_prop_access in H; ins; desf];
rewrite L in *; ins.
by exfalso; red in H; desc; rewrite clos_refl_transE in *; desf;
[|apply hb_weakp_is_access_r in H0; ins];
rewrite L in *; ins.
Qed.
Lemma prop_ext_sync_l :
∀
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y (L: lab x = Async),
prop_ext x y ↔
seq (sync_ext_r) (clos_refl_trans hb_weak) x y.
Proof.
ins; split; ins; [apply prop_extE in H|apply prop_extE];
unfold union, seq in *; desf; eauto 8.
by unfold prop_weak, restr_rel, union in *; desf;
[|apply helper_prop_access in H; ins; desf];
rewrite L in *; ins.
exfalso; red in H1; desc.
apply (inclusion_rt_rt2 inclusion_base_hb_weak) in H0.
by rewrite clos_refl_transE in *; desf;
(red in H; desf; [|apply chapo_access in H; ins; desf]);
try apply hb_weakp_is_access_l in H0; ins; desf;
rewrite L in *; ins.
Qed.
Lemma prop_ext_sync_both :
∀
(CrfD: ConsistentRF_dom)
(CcoD: ConsistentMO_dom) x y (L: lab x = Async) (L' : lab y = Async),
prop_ext x y ↔ False.
Proof.
ins; rewrite prop_ext_sync_l; ins.
unfold seq, sync_ext_r; split; ins; desf.
rewrite clos_refl_transE in *; desf;
[|eapply hb_weakp_is_access_r in H0; ins]; rewrite L' in *; ins.
Qed.
We next prove that the soundness of the alternative model.
Lemma SyncTotal_sound
(INCL: inclusion deps po) (C: ConsistentPower) :
∃ so, ConsistentSyncTotal so.
Proof.
assert (K:=C); red in K; desc.
set (T' := restr_rel (fun x ⇒ lab x = Async) (tot_ext acts Trel)).
assert (TOT: is_total (fun a ⇒ lab a = Async) T').
by eapply is_total_restr; red; ins; eapply tot_ext_total; ins;
apply FIN; intro X; rewrite X in *; ins.
assert (IRR: irreflexive T').
unfold T'; red; unfold restr_rel; ins; desf.
by eapply tot_ext_irr in H; eauto using acyclic_Trel.
assert (T: transitive T').
by eapply restr_rel_trans, tot_ext_trans.
assert (Cww: ∀ x y, so_step T' x y → clos_refl_trans hb_weak y x → False).
unfold so_step; ins; desc.
eapply IRR, T; eauto; split; ins;
eapply tot_ext_extends; split; ins.
by unfold seq, union; repeat (eexists; try edone); vauto.
∃ T'; red; unnw; intuition.
red; rewrite t_hb_soE; try done.
unfold seq, union; red; ins; desf; eauto using rt_trans.
eby eapply NTA, clos_trans_mon, inclusion_hb_weak_hb.
rewrite observation_condition_simplify,
observation_condition_alternative in *; ins.
eapply base_soE2 in PROP0; ins.
destruct PROP0; eauto.
unfold union, seq, so_step in H; desf;
eapply IRR, T; eauto; split; ins;
eapply tot_ext_extends; split; ins.
unfold seq, union; repeat (eexists; try edone); try apply rt_refl.
by apply may_chapoE; unfold seq, clos_refl, union; eauto 10.
unfold seq, union; repeat (eexists; try edone); [apply rt_refl| |].
by apply may_chapoE; unfold seq, clos_refl, union; eauto 10.
by red in H; desf; vauto.
unfold prop_so; rewrite base_soE2; ins.
rewrite <- !union_restr.
eapply acyclic_mon with (rel := clos_trans (T' +++ co +++ prop_ext)).
eapply trans_irr_acyclic; vauto.
eapply min_cycle with (rel' := T') (dom := fun a ⇒ lab a = Async);
ins; eauto.
by unfold union; red; ins; apply t_step; eauto.
unfold union in *; desf; eauto;
repeat red in R'; desf.
by apply CcoD in R; rewrite R'0 in *; desf.
by rewrite prop_ext_sync_both in R.
rewrite propE2 in PROP; ins.
unfold T' at 1 6; repeat split; ins; try rewrite helper_restr1 in *; ins.
by eapply (acyclic_mon PROP); unfold restr_rel; red; ins; desf.
unfold union in *; desf; eauto.
by rewrite prop_ext_sync_both in CYC.
unfold T', restr_rel in ×.
unfold union in R; desf; [by apply CcoD in R; rewrite D1 in *; desf|].
unfold union in R'; desf; [by apply CcoD in R'; rewrite D2 in *; desf|].
apply prop_ext_sync_r in R; ins.
apply prop_ext_sync_l in R'; ins.
red in S; desf.
assert (P: prop_weak c1 c2).
right; unfold seq, sync_ext_r, sync_ext_l, sync in *; desc.
by repeat (eexists; try edone).
by eapply PROP, t_rt_trans, clos_refl_trans_mon; vauto; ins; desf.
eapply (IRR b1); split; ins; eapply T; try edone;
split; ins; apply tot_ext_extends; split; ins.
unfold seq, sync_ext_l, sync_ext_r in *; desc.
eexists; split; vauto; eexists; split; eauto.
by eapply clos_refl_trans_mon; eauto; instantiate; ins; desf.
rewrite prop_extE; ins.
red; unfold prop_weak, union; ins; desf; eauto 6 using t_step;
unfold restr_rel, seq, so_step in H; desc.
eapply t_trans with f, t_trans with f'; apply t_step; eauto;
right; [left; right|right].
∃ z; split; vauto; repeat (eexists; vauto).
by apply rfe_dom in H; desf; eauto with access.
eexists; split; try edone;
eauto using clos_refl_trans_mon with inclusion.
repeat split; ins.
by rewrite clos_refl_transE in *; desf; eauto with access.
eapply t_trans with f, t_trans with f'; try apply t_step; eauto;
right; [left; right|right].
eexists; split; vauto; ∃ z; repeat (eexists; vauto).
by red in H; desf; eauto using inclusion_base_weak_base, clos_refl_trans.
by red in H; desf; try apply inclusion_base_weak_hb2 in H; eauto with access.
eexists; split; try edone;
eauto using clos_refl_trans_mon with inclusion.
repeat split; ins.
by rewrite clos_refl_transE in *; desf; eauto with access.
Qed.
Putting the two directions together, we get that the two Power models are
equivalent.
Theorem SyncTotal (INCL: inclusion deps po):
ConsistentPower ↔ ∃ so, ConsistentSyncTotal so.
Proof.
split; ins; desc; eauto using SyncTotal_sound, SyncTotal_complete.
Qed.
End PowerModel.
This page has been generated by coqdoc