Commit 636eefbd by Jacques-Henri Jourdan

Canonical structure for join semilattice.

parent 68f95e02
-Q theories promising
-arg -w -arg -notation-overridden,-projection-no-head-constant,-redundant-canonical-projection
theories/base.v
theories/location.v
theories/value.v
......
From promising Require Export base.
Inductive memOrder := | Plain | Relaxed | StrongRelaxed | AcqRel | SeqCst .
Instance memOrder_sqle : Sqle memOrder :=
Definition memOrder_le : relation memOrder :=
λ o1 o2,
match o1, o2 with
| Plain, _ => True
......@@ -21,31 +20,17 @@ Instance memOrder_sqle : Sqle memOrder :=
| SeqCst, SeqCst => True
end.
Instance memOrder_dec_eq : EqDecision memOrder.
Instance memOrder_dec : EqDecision memOrder.
Proof. solve_decision. Defined.
Instance memOrder_PartialOrder : @PartialOrder memOrder ().
Proof.
split; first split.
- by move => [].
- move => [] [] []; firstorder.
- move => [] []; firstorder.
Qed.
Instance memOrder_sqle_dec : o1 o2 : memOrder, Decision (o1 o2).
Proof. move => [] []; firstorder. Qed.
Instance memOrder_join : Join memOrder :=
λ o1 o2, if (decide (o1 o2)) then o2 else o1.
Instance memOrder_JSL : JoinSemiLattice memOrder.
Proof.
econstructor.
- eauto with typeclass_instances.
- move => x y. rewrite /join /memOrder_join /=. by case (decide (x y)).
- move => x y. rewrite /join /memOrder_join /=.
case (decide (x y)) => [//|] /=.
destruct x,y; firstorder.
- move => x y ?. rewrite /join /memOrder_join.
by case (decide (x y)).
Qed.
Instance memOrder_le_dec : RelDecision memOrder_le.
Proof. move => [] []; firstorder. Defined.
Program Canonical Structure memOrder_JSL :=
Make_JSL memOrder (=) memOrder_le
(λ o1 o2, if (decide (memOrder_le o1 o2)) then o2 else o1) _ _ _ _ _ _ _ _.
Next Obligation. split; [move=>[]//|move=>[][]//[]//]. Qed.
Next Obligation. move=>[][]//. Qed.
Next Obligation. move=>[][]//. Qed.
Next Obligation. move=>[][]//. Qed.
Next Obligation. move=>[][][]//. Qed.
......@@ -117,7 +117,7 @@ Section Memory.
Proof.
inversion ADD. move => t'.
case (decide (t' = t)) => [->|?];
[rewrite lookup_insert|by rewrite lookup_insert_ne].
[rewrite lookup_insert|rewrite lookup_insert_ne //; by destruct lookup].
case Eqt : (C !! t); [|done].
exfalso. apply (DISJ _ _ Eqt t).
- by apply interval_elem_ub, WF.
......@@ -489,7 +489,7 @@ Section Memory.
case_match => Eqv.
eexists. eexists. repeat split; eauto.
- apply (cell_head_lookup (flip ())). by eauto.
- eapply (cell_head_top (flip (@sqle Qp Qp_sqle))). by eauto.
- apply (cell_head_top _ _ _ _ Heqo).
Qed.
Lemma cell_deallocated_correct2 C:
......@@ -838,12 +838,10 @@ Section Memory.
Lemma join_closed_timemap (T1 T2: timeMap) M (C1: T1 M) (C2: T2 M) :
T1 T2 M.
Proof.
move => l to. rewrite lookup_join.
move => l to. rewrite lookup_union_with.
destruct (T1 !! l) as [t1|] eqn: Eq1; rewrite Eq1;
destruct (T2 !! l) as [t2|] eqn: Eq2; rewrite Eq2; cbn; last done.
- move => [].
move : (Qp_Join_case t1 t2) => [-> <-|-> <-];
[by apply C1|by apply C2].
- move => [<-]. rewrite /join /jsl_join /=. destruct decide; [by apply C2|by apply C1].
- move => [<-]. by apply C1.
- move => [<-]. by apply C2.
Qed.
......@@ -990,7 +988,7 @@ Section Memory.
destruct (T2 !! l) as [to|] eqn:HT2; rewrite HT2; last done.
cbn => Le.
destruct (In _ _ HT2) as [m [to' [Le' Eq]]].
exists m, to'. split; [by etrans|by assumption].
exists m, to'. split=>//. etrans; [apply Le|done].
Qed.
Global Instance closed_view_downclosed:
......@@ -1002,7 +1000,8 @@ Section Memory.
Global Instance opt_closed_view_downclosed:
Proper ((@sqle (option view) _) ==> (@eq memory) ==> flip impl) ().
Proof.
move => [V1|] [V2|] Sqle ??-> // In. move : Sqle In. cbn => -> //.
move => [?|] [?|] Sqle ??-> // In.
eapply (closed_view_downclosed _ _ Sqle _ _ eq_refl In).
Qed.
Lemma closed_timemap_wf_view (V : view) M (WF: wf V) (HC: V.(rlx) M):
......@@ -1944,7 +1943,7 @@ Section Memory.
M1 M2.
Proof.
revert M2 IN.
induction 𝑚s => M2 IN ; inversion IN; subst; first done.
induction 𝑚s => M2 IN; inversion IN; subst; first done.
etrans; first apply (IH𝑚s _ NEXT).
move => [l t]. case Eq: (M3 !! (l,t)) => [m|]; last done.
erewrite (lookup_mem_addins_old _ _ _ M3); eauto. done.
......
......@@ -291,7 +291,7 @@ Section Wellformedness.
(dom (gset _) L1.(tv).(cur).(rlx))
l L1.(tv).(cur)) as [_ HE].
by rewrite HE.
- destruct (L1.(tv).(rel) !! l) as [t|] eqn:HRel; last done.
- case HRel: (L1.(tv).(rel) !! l)=>[t|] //.
exfalso. apply NIn. apply (tview_wf_rel_dom _ WF), elem_of_dom.
by eexists.
Qed.
......@@ -304,7 +304,7 @@ Section Wellformedness.
set T' := 𝓥.(acq).(rlx) 𝓢.
set V' := mkView T' T'.
have ?: acq 𝓥 V'.
{ constructor; simpl; (etrans; last apply join_sqle_l); [apply WF|done]. }
{ constructor; simpl; [etrans; [by apply WF|]|]; solve_jsl. }
rewrite EQSC; constructor; simpl; last done.
- move => l.
case (decide (l dom (gset _) T'))
......@@ -313,9 +313,9 @@ Section Wellformedness.
destruct (lookup_to_gmap_Some V' (dom (gset _) T') l V')
as [_ HE].
rewrite HE; last done. cbn. etrans; [apply WF|done].
+ destruct (rel 𝓥 !! l) as [t|] eqn:HRel; last done.
+ case HRel: (rel 𝓥 !! l)=>[t|] //.
exfalso. apply NIn. rewrite gmap_join_dom_union elem_of_union. left.
apply (gmap_sqle_dom_proper _ _ (view_sqle_rlx _ _ (tview_wf_cur_acq _ WF))).
eapply gmap_sqle_dom_proper; [apply view_sqle_rlx, tview_wf_cur_acq, WF|].
apply (tview_wf_rel_dom _ WF), elem_of_dom. by eexists.
- etrans; [apply WF|done].
Qed.
......@@ -499,7 +499,7 @@ Section Wellformedness.
[rewrite lookup_insert|by rewrite lookup_insert_ne].
destruct (𝓝1 !! mloc 𝑚) as [tn|] eqn:H𝓝; last done.
destruct (CLOSED _ _ H𝓝) as [mn [tn' [Le Eqmm]]].
cbn. etrans; first apply Le. apply Qclt_le_weak.
transitivity (Some tn')=>//. apply Qclt_le_weak.
by apply (MAX (mkMsg 𝑚.(mloc) tn' mn)).
Qed.
......@@ -558,7 +558,7 @@ Section Wellformedness.
move => 𝑚 In𝑚.
destruct (𝓝 !! 𝑚.(mloc)) as [t|] eqn:H𝓝; last done.
apply CLOSED in H𝓝 as [? [t' [Le Eqt]]].
cbn. etrans; first apply Le. apply Qclt_le_weak.
transitivity (Some t')=>//. apply Qclt_le_weak.
by apply (memory_dealloc_max _ _ _ _ _ MEMALL _ In𝑚 (mkMsg 𝑚.(mloc) t' _) Eqt).
Qed.
......@@ -876,10 +876,10 @@ Section AllocSteps.
apply (FRESH 0); first by omega. rewrite memory_lookup_cell in Eqm.
apply memory_loc_elem_of_dom=>EQ. by rewrite EQ in Eqm. }
econstructor; [exact MA|]. simpl.
econstructor; simpl; [by rewrite HRlx; compute|done|..|done|].
+ rewrite decide_False; [by eauto|by cbv].
econstructor; [by rewrite HRlx; compute|done|..|done|].
+ rewrite ->decide_False; [by eauto|by cbv].
+ rewrite HRel. by eauto.
+ rewrite decide_False; [done|by cbv].
+ rewrite ->decide_False; [done|by cbv].
Qed.
Lemma alloc_progress c1 l n b
......@@ -1060,7 +1060,7 @@ Section AllocSteps.
apply REMOVE. by omega. } clear IH.
econstructor; [exact MA|].
econstructor;
[|done|rewrite decide_False; auto|done|done|rewrite decide_False; auto].
[|done|rewrite ->decide_False; auto|done|done|rewrite ->decide_False; auto].
rewrite -(alloc_helper_cur_old _ _ _ _ MA);
last by (case_match; [case_match|]; apply dealloc_messages_shift_1).
destruct (𝓥1.(cur).(rlx) !! (l >> 0)) as [t0|] eqn:Ht0;
......@@ -1139,7 +1139,7 @@ Section Steps.
destruct (𝓥.(cur).(rlx) !! l) as [ct|] eqn:Eqct; last done.
destruct (closed_view_rlx _ _ (closed_tview_cur _ _ CLOSED ) _ _ Eqct)
as [mt [tt [Lett Eqmt]]].
cbn. etrans; first exact Lett.
cbn. transitivity (Some tt)=>//.
apply (cell_head_top _ _ _ _ MAX), elem_of_dom.
eexists. by rewrite -memory_lookup_cell.
Qed.
......@@ -1189,7 +1189,7 @@ Section Steps.
- have ?: L1.(tv).(cur).(rlx) !! l Some tm.
{ destruct (L1.(tv).(cur).(rlx) !! l) as [ct|] eqn:Eqct; last done.
destruct (closed_view_rlx _ _ (closed_tview_cur _ _ CLOSED ) _ _ Eqct)
as [? [? [Ltt ?]]]. cbn. etrans; [exact Ltt| by eapply MAX]. }
as [? [? [Ltt ?]]]. transitivity (Some x0)=>//. by eapply MAX. }
econstructor; eauto; simpl; done.
- econstructor; [by constructor|done].
Qed.
......@@ -1247,9 +1247,8 @@ Section Steps.
move => V /=. rewrite /write_new_mview.
case_match; last done.
have ?: Some t ({[l := t]}: timeMap) !! l by rewrite lookup_insert.
move => [<-].
case_match; case_match => /=;
rewrite ?lookup_join; do ? (etrans; last apply join_sqle_r); done.
move => [<-]. case_match; case_match => /=;
rewrite ?lookup_join lookup_singleton //; solve_jsl.
Qed.
Lemma write_new_mview_closed o l (t t' : time) v 𝓥 M1 C V'
......@@ -1363,7 +1362,7 @@ Section Steps.
+ eapply strict_transitive_r; first by eauto.
by apply total_not_strict, Qclt_not_le, Qp_lt_sum; exists 1%Qp.
+ rewrite /VR /write_new_mview.
case_match; [by rewrite right_id_L|done].
case_match; [rewrite (right_id_L )|]=>//.
- apply (WriteDRF _ _ _ _ _ otl); first by constructor.
rewrite /write_new_na.
case_match; [done|split; last done].
......@@ -1399,4 +1398,4 @@ Section Steps.
eexists. by eapply (PStepW _ c1 (mkMsg l _ (mkBMes (VVal v) t _))).
Qed.
End Steps.
\ No newline at end of file
End Steps.
......@@ -35,7 +35,7 @@ Lemma interval_sqle_in il ir t:
il ir t il t ir.
Proof. move => [??] [??].
split.
- by eapply Qcle_lt_trans.
- by eapply Qcle_lt_trans with (low il).
- by etrans.
Qed.
......
......@@ -38,35 +38,30 @@ Section ThreadView.
: WellformedResolver (𝓥.(rel) !! l).
Proof. by apply tview_wf_rel. Qed.
Record tview_sqle' 𝓥1 𝓥2 :=
Record tview_le 𝓥1 𝓥2 :=
mkTViewSqle {
tview_sqle_rel : 𝓥1.(rel) 𝓥2.(rel);
tview_sqle_cur : 𝓥1.(cur) 𝓥2.(cur);
tview_sqle_acq : 𝓥1.(acq) 𝓥2.(acq);
}.
Global Instance tview_sqle : Sqle threadView := tview_sqle'.
Global Instance tview_PartialOrder : @PartialOrder threadView ().
Proof.
split; first split.
- repeat split; reflexivity.
- move => ??? [???] [???]. constructor; by etrans.
- move => [???] [???] [???] [???]. f_equal; by apply: anti_symm.
Qed.
Global Instance tview_join : Join threadView :=
Definition tview_join :=
λ 𝓥1 𝓥2, mkTView (𝓥1.(rel) 𝓥2.(rel))
(𝓥1.(cur) 𝓥2.(cur))
(𝓥1.(acq) 𝓥2.(acq)).
Global Instance tview_JSL : JoinSemiLattice threadView.
Proof.
constructor; first eauto with typeclass_instances.
- split; last split; apply join_sqle_l.
- split; last split; apply join_sqle_r.
- move => ??? [???] [???]; split; by eapply join_least.
Program Canonical Structure tview_JSL :=
Make_JSL threadView (=) tview_le tview_join
_ _ _ _ _ _ _ _.
Next Obligation.
split; [by split|] => ??? [???] [???]. constructor; by etrans.
Qed.
Next Obligation.
move => [???] [???] [???] [???]. f_equal; by apply: anti_symm.
Qed.
Next Obligation. split; solve_jsl. Qed.
Next Obligation. split; solve_jsl. Qed.
Next Obligation. move => ??? [???] [???]. split; solve_jsl. Qed.
Notation memory := (memory (VAL:=VAL)).
Implicit Type (M: memory).
......@@ -78,6 +73,10 @@ Section ThreadView.
Global Instance closed_tview : ElemOf threadView memory := closed_tview'.
Class RWR A (R : relation A) : Prop.
Instance sqle_rwr `{Sqle A} : RWR A ().
Global Instance closed_tview_downclosed :
Proper ((@sqle threadView _) ==> (@eq memory) ==> flip impl) ().
Proof.
......@@ -160,22 +159,20 @@ Section ThreadView.
+ rewrite gmap_join_dom_union. etrans; last apply union_subseteq_l.
by apply WF.
- move => l'. etrans; first by apply WF.
case (decide (AcqRel _)) => _ /=; cbn; solve_jsl.
case (decide (AcqRel _)) => _ /=; solve_jsl.
- case (decide (AcqRel _)) => [?|?] /=.
+ rewrite (decide_True).
* do 2 apply join_sqle_mono_r. apply WF.
* by destruct WF as [_ _ _ _ _ ->].
* etrans; by eauto.
+ have ? : cur 𝓥 V acq 𝓥 V by apply join_sqle_mono_r,WF.
case_match; last done. etrans; last apply join_sqle_l. done.
+ have ? : cur 𝓥 V acq 𝓥 V. by destruct WF as [_ _ _ _ _ ->].
case_match; solve_jsl.
Qed.
Lemma read_helper_tview_sqle 𝓥 𝓥' o l t R
(READ: read_helper 𝓥 o l t R 𝓥'):
𝓥 𝓥'.
Proof.
inversion READ. constructor; simpl; [done|..].
- rewrite CUR. clear. case_match; last apply join_sqle_l. solve_jsl.
- rewrite ACQ. case_match; last apply join_sqle_l. solve_jsl.
inversion READ. subst. constructor=>//=; clear; case_match; solve_jsl.
Qed.
Lemma write_helper_tview_wf 𝓥 𝓥' o l t Rr Rw
......@@ -204,15 +201,12 @@ Section ThreadView.
- move => l'. rewrite REL.
case (decide (l' = l)) => [->|?];
[rewrite lookup_insert|rewrite lookup_insert_ne; last auto].
+ cbn.
have ?: Vra cur 𝓥 V.
{ rewrite VRA.
case (decide (AcqRel _)) => _ /=; [by auto|by apply join_sqle_r]. }
+ have ?: Vra cur 𝓥 V.
{ rewrite VRA. clear. case_match; solve_jsl. }
rewrite VEq'. destruct (rel 𝓥 !! l) as [V0|] eqn:Eq0; last auto.
apply join_least; last by auto. etrans; last apply join_sqle_l.
have ?: Some V0 Some (cur 𝓥) by rewrite -Eq0; apply WF. done.
+ etrans; first apply WF. cbn. apply join_sqle_l.
- apply join_sqle_mono_r, WF.
have ?: Some V0 Some (cur 𝓥) by rewrite -Eq0; apply WF. solve_jsl.
+ etrans; first apply WF. solve_jsl.
- by destruct WF as [_ _ _ _ _ ->].
Qed.
Lemma write_helper_tview_sqle 𝓥 𝓥' o l t Rr Rw
......@@ -220,13 +214,10 @@ Section ThreadView.
𝓥 𝓥'.
Proof.
inversion_clear WRITE.
constructor => /=.
- move => l'. rewrite REL VEq'.
case (decide (l' = l)) => [->|?];
constructor; (try solve_jsl) => l'. rewrite /= REL VEq'.
case (decide (l' = l)) => [->|?];
[rewrite lookup_insert|by rewrite lookup_insert_ne].
case (rel 𝓥 !! l) => [?|]; [cbn;apply join_sqle_l|done].
- apply join_sqle_l.
- apply join_sqle_l.
case: (rel 𝓥 !! l) => [?|]; solve_jsl.
Qed.
Lemma sc_fence_helper_tview_wf 𝓥 𝓥' 𝓢 𝓢'
......@@ -361,8 +352,7 @@ Section ThreadView.
Proof.
inversion SC.
have ?: 𝓥.(acq) {| pln := 𝓢'; rlx := 𝓢' |}.
{ rewrite EQSC. constructor; simpl; last apply join_sqle_l.
etrans; last apply join_sqle_l. apply WF. }
{ assert (pln (acq 𝓥) rlx (acq 𝓥)) by apply WF. subst. constructor; solve_jsl. }
constructor; simpl; [|etrans; [apply WF|done]|done].
move => l.
have HD : dom (gset loc) 𝓥.(rel) dom (gset _) 𝓢'.
......@@ -374,14 +364,14 @@ Section ThreadView.
- rewrite lookup_to_gmap (option_guard_True _ _ IN).
etrans; [apply WF|cbn]. etrans; [apply WF|done].
- rewrite lookup_to_gmap (option_guard_False _ _ NIN).
destruct (rel 𝓥 !! l) as [?|] eqn:H𝓥; last done.
case H𝓥: (rel 𝓥 !! l) => [?|//].
exfalso. apply NIN, HD, elem_of_dom. by eexists.
Qed.
Lemma sc_fence_helper_sc_sqle 𝓥 𝓥' 𝓢 𝓢'
(SC: sc_fence_helper 𝓥 𝓢 𝓥' 𝓢') :
𝓢 𝓢'.
Proof. inversion SC. rewrite EQSC. apply join_sqle_r. Qed.
Proof. inversion SC. rewrite EQSC. solve_jsl. Qed.
Lemma sc_fence_helper_closed_tview 𝓥 𝓥' 𝓢 𝓢' M
(SC: sc_fence_helper 𝓥 𝓢 𝓥' 𝓢')
......@@ -450,10 +440,9 @@ Section ThreadView.
induction 𝑚s as [|𝑚 𝑚s IH] => 𝓥3 ALLOC 𝑚'; first by inversion 1.
inversion_clear ALLOC.
move => /elem_of_cons [->|In].
- inversion WRITE. rewrite /= lookup_join VEq /= lookup_singleton.
apply join_sqle_r.
- inversion WRITE. rewrite /= lookup_join VEq /= lookup_singleton. solve_jsl.
- etrans; first apply (IH _ NEXT _ In).
apply (write_helper_tview_sqle _ _ _ _ _ _ _ WRITE).
eapply write_helper_tview_sqle, WRITE.
Qed.
Lemma alloc_helper_cur_old 𝑚s 𝓥1 𝓥2 l
......
......@@ -14,53 +14,37 @@ Section View.
(** View wellformnedness *)
Global Instance view_wf : Wellformed view := λ V, V.(pln) V.(rlx).
(** View order *)
Record view_sqle' V1 V2 :=
(** View join semilattice *)
Record view_le V1 V2 :=
mkViewSqle {
view_sqle_pln : V1.(pln) V2.(pln);
view_sqle_rlx : V1.(rlx) V2.(rlx);
}.
Global Instance view_sqle : Sqle view := view_sqle'.
Program Canonical Structure view_JSL :=
Make_JSL view (=) view_le
(λ V1 V2, mkView (V1.(pln) V2.(pln)) (V1.(rlx) V2.(rlx))) _ _ _ _ _ _ _ _.
Next Obligation. split. move=>[]//. move=>??? [??][??]; split; by etrans. Qed.
Next Obligation. move=>[??][??] [??] [??]. f_equal; solve_jsl. Qed.
Next Obligation. move=>[??][??]. split; solve_jsl. Qed.
Next Obligation. move=>[??][??]//. split; solve_jsl. Qed.
Next Obligation. move=>[??][??][??][??][??]//. split; solve_jsl. Qed.
Global Instance view_PartialOrder : @PartialOrder view ().
Proof.
split; first split.
- split; reflexivity.
- move => ??? [??] [??]; split; by etrans.
- move => [??] [??] [??] [??]. f_equal; by apply: anti_symm.
Qed.
Global Instance view_leibniz_equiv : LeibnizEquiv view.
Proof. move=>?//. Qed.
(** View join *)
Global Instance view_join : Join view :=
λ V1 V2, mkView (V1.(pln) V2.(pln)) (V1.(rlx) V2.(rlx)).
Global Instance view_bottom : @JSLBottom view_JSL .
Proof. split; apply jsl_bottom_sqle. Qed.
Lemma view_join_wf V1 V2 :
wf V1 wf V2 wf (V1 V2).
Proof.
move => W1 W2. rewrite /wf /view_wf. etrans.
apply join_sqle_mono_r; first eauto.
by apply join_sqle_mono_l.
Qed.
Proof. move => W1 W2. rewrite /wf /view_wf. by apply jsl_join_mono. Qed.
Global Instance view_join_wf_R {V1 V2: view} {_: WellformedResolver V1}
{_: WellformedResolver V2}
: WellformedResolver (V1 V2).
Proof. by apply view_join_wf. Qed.
Global Instance view_join_right_empty : RightId eq (: view) join.
Proof. move => [??]. by rewrite /join /view_join /= 2!right_id_L. Qed.
Global Instance view_join_left_empty : LeftId eq (: view) join.
Proof. move => [??]. by rewrite /join /view_join /= 2!left_id_L. Qed.
Global Instance view_JSL : JoinSemiLattice view.
Proof.
constructor; first eauto with typeclass_instances.
- split; apply join_sqle_l.
- split; apply join_sqle_r.
- move => ??? [??] [??]; split ; by eapply join_least.
Qed.
(** View countable *)
Section ViewCountable.
Definition _tm_pair : Type := timeMap * timeMap.
......@@ -78,10 +62,4 @@ Section View.
Global Instance view_countable : Countable view :=
inj_countable _view_to_pair (Some _pair_to_view) _.
Proof. by destruct 0. Qed.
Global Instance view_equiv_sqle_antisymm : AntiSymm (=) ().
Proof.
move => [??] [??] [H11 H12] [H21 H22].
f_equiv; simpl in *; by apply (anti_symm ()).
Qed.
End View.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment