Commit 7ab22ba1 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify ghost threadpool construction.

parent 740e2a90
......@@ -19,7 +19,6 @@ Class heapG Σ := HeapG {
Definition heapΣ : gFunctors := authΣ heapUR.
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
(* Definition of_heap : heapUR state := omap (maybe DecAgree snd). *)
Section definitions.
Context `{heapG Σ}.
......@@ -36,7 +35,6 @@ Section definitions.
Proof. apply _. Qed.
Global Instance heap_mapsto_timeless l q v : TimelessP (heap_mapsto l q v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
......@@ -68,31 +66,10 @@ Section lang_rules.
Local Hint Resolve to_of_val.
(** Conversion to heaps and back *)
(* Global Instance of_heap_proper : Proper (() ==> (=)) of_heap. *)
(* Proof. solve_proper. Qed. *)
(* Lemma from_to_heap σ : of_heap (to_heap σ) = σ. *)
(* Proof. *)
(* apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l). *)
(* Qed. *)
Lemma to_heap_valid σ : to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma lookup_to_heap_None σ l : σ !! l = None to_heap σ !! l = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
(* Lemma of_heap_insert l v h : *)
(* of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h). *)
(* Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed. *)
(* Lemma of_heap_singleton_op l q v h : *)
(* ({[l := (q, DecAgree v)]} h) *)
(* of_heap ({[l := (q, DecAgree v)]} h) = <[l:=v]> (of_heap h). *)
(* Proof. *)
(* intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|]. *)
(* - move: (Hv l). rewrite /of_heap lookup_insert *)
(* lookup_omap (lookup_op _ h) lookup_singleton. *)
(* case _:(h !! l)=>[[q' [v'|]]|] //=; last by move=> [??]. *)
(* move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp. *)
(* - rewrite /of_heap lookup_insert_ne // !lookup_omap. *)
(* by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L. *)
(* Qed. *)
Lemma heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_heap σ σ !! l = Some v.
Proof.
......@@ -105,28 +82,9 @@ Section lang_rules.
Proof.
intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
Qed.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
(* Lemma of_heap_None h l : h of_heap h !! l = None h !! l = None. *)
(* Proof. *)
(* move=> /(_ l). rewrite /of_heap lookup_omap. *)
(* by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto. *)
(* Qed. *)
Lemma heap_store_valid l h v1 v2 :
({[l := (1%Qp, DecAgree v1)]} h)
({[l := (1%Qp, DecAgree v2)]} h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
by case: (h !! l)=> [x|] // /Some_valid /exclusive_l.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
(* Lemma of_empty_heap : of_heap = . *)
(* Proof. unfold of_heap; apply map_eq => i; rewrite !lookup_omap; f_equal. Qed. *)
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v l {q2} v ⊣⊢ l {q1+q2} v.
......
......@@ -365,18 +365,18 @@ Section fundamental.
rewrite {2}[ τ Δ (v, v')]interp_EqType_agree; trivial.
iMod "Hv'" as %Hv'; subst.
destruct (decide (v' = w)) as [|Hneq]; subst.
- iMod (step_cas_suc _ _ j K l' (of_val w') w' w (of_val u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} !>".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
- iAssert ( (w' = w))%I as ">%".
{ rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
iMod (step_cas_suc _ _ j K l' (of_val w') w' w (of_val u') u'
with "[$Hs $Hu $Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
iApply (wp_cas_suc with "[Hv1]"); eauto using to_of_val; first solve_ndisj.
iNext. iIntros "Hv1". iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
iExists (#v true); iFrame; eauto.
- iMod (step_cas_fail _ _ j K l' 1 v' (of_val w') w' (of_val u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} !>".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
-iAssert ( (v' w'))%I as ">%".
{ rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
iMod (step_cas_fail _ _ j K l' 1 v' (of_val w') w' (of_val u') u'
with "[$Hs $Hu $Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
iApply (wp_cas_fail with "[Hv1]"); eauto using to_of_val; first solve_ndisj.
iNext. iIntros "Hv1". iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
......
......@@ -18,7 +18,6 @@ Class heapIG Σ := HeapIG {
}.
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR state := omap (maybe DecAgree snd).
Section definitionsI.
Context `{heapIG Σ}.
......@@ -69,13 +68,8 @@ Section lang_rules.
(** Conversion to heaps and back *)
Lemma to_heap_valid σ : to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
Proof.
apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
Qed.
Lemma lookup_to_heap_None σ l : σ !! l = None to_heap σ !! l = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
Lemma heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_heap σ σ !! l = Some v.
Proof.
......@@ -91,19 +85,6 @@ Section lang_rules.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
Lemma heap_store_valid l h v1 v2 :
({[l := (1%Qp, DecAgree v1)]} h)
({[l := (1%Qp, DecAgree v2)]} h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
by case: (h !! l)=> [x|] // /Some_valid/exclusive_l.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
Lemma to_empty_heap : to_heap .
Proof. intros i. unfold to_heap. by rewrite lookup_fmap ?lookup_empty. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v : l ↦ᵢ{q1} v l ↦ᵢ{q2} v ⊣⊢ l ↦ᵢ{q1+q2} v.
......
This diff is collapsed.
......@@ -16,28 +16,26 @@ Proof.
eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iMod (auth_alloc to_heap ownP heapN _ with "[Hσ]")
as (γh) "[#Hh1 Hh2]"; auto; first done.
iMod (own_alloc ( (to_cfg ([e'], ) : cfgUR)
(({[ 0 := Excl' e' ]} : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ rewrite -auth_both_op auth_valid_discrete /= prod_included /= to_empty_heap.
eauto using to_cfg_valid. }
iMod (inv_alloc specN _ ( ρ', own γc ( ρ') ( ([e'], ) →⋆ of_cfg ρ'))%I
with "[Hcfg1]") as "#Hcfg"; trivial.
{ iNext. iExists _. iIntros "{$Hcfg1} !%". rewrite from_to_cfg; constructor. }
iMod (own_alloc ( (to_tpool [e'], )
(({[ 0 := Excl e' ]} : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
set (Hcfg := CFGSG _ (HeapIG _ _ _ γh) _ γc).
iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg".
{ iNext. iExists [e'], . rewrite {2}/to_heap fin_maps.map_fmap_empty. auto. }
rewrite -(empty_env_subst e).
iApply wp_fupd; iApply wp_wand_r; iSplitL; [iApply (bin_log_related_alt
(Hlog (CFGSG _ (HeapIG _ _ _ γh) _ γc)) [] [] ([e'], ) 0 [])|]; simpl.
(Hlog _) [] [] ([e'], ) 0 [])|]; simpl.
{ rewrite /heapI_ctx /spec_ctx /auth_ctx /tpool_mapsto /auth_own /=.
rewrite empty_env_subst -interp_env_nil. by iFrame "Hh1 Hcfg Hcfg2". }
iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (ρ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /auth.auth_own /=.
iCombine "Hj" "Hown" as "Hown".
iDestruct (own_valid with "Hown") as %[[[tp h] Hρ] [Htp ?]]%auth_valid_discrete.
move: Hρ; rewrite /= right_id pair_op left_id leibniz_equiv_iff=> ?; simplify_eq/=.
iMod ("Hclose" with "[-]").
{ iDestruct "Hown" as "[Ho1 Ho2]". rewrite /auth_inv; eauto. }
iIntros "!> !%". exists (of_tpool tp), (of_heap h), v2.
destruct tp as [|[[]|]]; by inversion_clear Htp.
iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
iMod ("Hclose" with "[-]") as "_"; [iExists (_ :: tp'), σ; auto|].
iIntros "!> !%"; eauto.
Qed.
Lemma binary_soundness Σ `{irisPreG lang Σ, authG Σ heapUR, authG Σ cfgUR}
......
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