Commit 4dd1bc31 authored by Dan Frumin's avatar Dan Frumin

Make the counter refinement proof more compositional

parent e803a554
......@@ -77,12 +77,17 @@ Section CG_Counter.
(* TODO: those should be accompaied by lemmas; preferably so that
[change] does not change too much *)
Tactic Notation "rel_bind_l" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| [ |- (_ bin_log_related _ _ _ (fill _ ?e) _ _ ) ] =>
reshape_expr e ltac:(fun K e' =>
unify e' efoc; change e with (fill K e'))
| [ |- (_ bin_log_related _ _ _ ?e _ _ ) ] =>
reshape_expr e ltac:(fun K e' =>
unify e' efoc; change e with (fill K e'))
end.
Tactic Notation "rel_bind_r" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| [ |- (_ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
reshape_expr e ltac:(fun K e' =>
......@@ -101,10 +106,7 @@ Section CG_Counter.
iIntros (?) "Hx Hlog".
unfold CG_increment. simpl.
iApply bin_log_related_rec_r; auto. simpl.
(* TODO: rel_bind_r (Load (Loc x)) *)
change ((Store (Loc x) (BinOp Add (#n 1) (Load (Loc x)))))
with (fill [StoreRCtx (LocV x);BinOpRCtx Add (#nv 1)] (Load (Loc x))).
rewrite -fill_app.
rel_bind_r (Load (Loc x)).
iApply (bin_log_related_load_r with "Hx");auto.
iIntros "Hx". rewrite ?fill_app /=.
rel_bind_r (BinOp Add _ _).
......@@ -263,8 +265,78 @@ Section CG_Counter.
Lemma FG_increment_closed (x : expr) :
( f, x.[f] = x) f, (FG_increment x).[f] = FG_increment x.
Proof. intros Hx f. asimpl. unfold FG_increment. rewrite ?Hx; trivial. Qed.
Proof. intros Hx f. asimpl. unfold FG_increment. rewrite ?Hx; trivial. Qed.
Lemma bin_log_FG_increment_l Γ K E x n t τ :
x ↦ᵢ (#nv n) -
(x ↦ᵢ (#nv (S n)) - {E,E;Γ} fill K Unit log t : τ) -
{E,E;Γ} fill K (App (FG_increment (Loc x)) Unit) log t : τ.
Proof.
iIntros "Hx Hlog".
iApply bin_log_related_bind_l.
{ autosubst. }
iApply wp_rec; auto. iNext.
change (Rec
(App
(Rec
(If
(CAS (Loc x).[ren (+4)]
(Var 1) (BinOp Add (#n 1) (Var 1))) Unit
(App (Var 2) (Var 3))))
(Load (Loc x).[ren (+2)]))) with (FG_increment (Loc x)). simpl.
wp_bind (Load (Loc x)).
iApply (wp_load with "[Hx]"); auto. iNext.
simpl. iIntros "Hx".
iApply wp_rec; auto. iNext. simpl.
wp_bind (BinOp _ _ _).
iApply (wp_nat_binop). iNext. iModIntro. simpl.
wp_bind (CAS _ _ _).
iApply (wp_cas_suc with "[Hx]"); auto.
iNext. iIntros "Hx".
iApply wp_if_true. iNext.
iApply wp_value; auto.
iSplit; eauto. by iApply "Hlog".
(* TODO !!!!
Is this actually better than using bin_log_related lemmas?
*)
Qed.
Lemma bin_log_FG_increment_l' Γ K E x n t τ :
x ↦ᵢ (#nv n) -
(x ↦ᵢ (#nv (S n)) - {E,E;Γ} fill K Unit log t : τ) -
{E,E;Γ} fill K (App (FG_increment (Loc x)) Unit) log t : τ.
Proof.
iIntros "Hx Hlog".
iApply (bin_log_related_rec_l Γ E with "[-]"); auto.
iNext.
change (Rec
(App
(Rec
(If
(CAS (Loc x).[ren (+4)]
(Var 1) (BinOp Add (#n 1) (Var 1))) Unit
(App (Var 2) (Var 3))))
(Load (Loc x).[ren (+2)]))) with (FG_increment (Loc x)). simpl.
rel_bind_l (Load (Loc x)). rewrite -fill_app.
iApply (bin_log_related_load_l E E Γ with "[-]"); auto.
iModIntro. iExists (#nv n). iSplit; eauto. iFrame "Hx".
iIntros "Hx". rewrite fill_app /=.
iApply (bin_log_related_rec_l); auto.
iNext. simpl.
rel_bind_l (BinOp Add _ _). rewrite -fill_app.
iApply (bin_log_related_binop_l). rewrite fill_app /=.
iNext. rel_bind_l (CAS _ _ _). rewrite -fill_app.
iApply (bin_log_related_cas_l); auto.
iModIntro. iExists (#nv n). iFrame.
iSplitR.
- iDestruct 1 as %Hfoo. by exfalso.
- iIntros "% Hx". rewrite fill_app /=.
iApply bin_log_related_if_true_l; auto.
iNext. by iApply "Hlog".
Qed.
Global Opaque FG_increment.
Lemma FG_counter_body_type x Γ :
typed Γ x (Tref TNat)
typed Γ (FG_counter_body x)
......@@ -279,8 +351,9 @@ Section CG_Counter.
( f, x.[f] = x)
f, (FG_counter_body x).[f] = FG_counter_body x.
Proof.
intros H1 f. asimpl. unfold FG_counter_body, FG_increment.
rewrite ?H1. by rewrite counter_read_closed.
intros H1 f. asimpl; auto.
rewrite (FG_increment_closed _ H1).
by rewrite counter_read_closed.
Qed.
Lemma FG_counter_type Γ :
......@@ -291,7 +364,9 @@ Section CG_Counter.
Qed.
Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.
Proof. simpl. rewrite counter_read_subst. asimpl.
Transparent FG_increment. asimpl. done. Qed.
Hint Rewrite FG_counter_closed : autosubst.
Definition counterN : namespace := nroot .@ "counter".
......@@ -299,7 +374,7 @@ Section CG_Counter.
(Hclosed : f, e.[upn 2 f] = e)
(Hclosed' : f, e'.[upn 2 f] = e') :
( Δ vv, τ Δ vv -
[] App (Rec e) (of_val (vv.1)) log App (Rec e') (of_val (vv.2)) : τ') -
nil App (Rec e) (of_val (vv.1)) log App (Rec e') (of_val (vv.2)) : τ') -
Γ (Rec e) log (Rec e') : TArrow τ τ'.
Proof.
iIntros "#H".
......@@ -312,31 +387,131 @@ Section CG_Counter.
iSpecialize ("H" $! Δ with "* Hs []").
{ iAlways. iApply interp_env_nil. }
rewrite ?fmap_nil. rewrite ?empty_env_subst.
rewrite /interp_expr.
done.
Qed.
Definition counter_inv l cnt cnt' : iProp Σ :=
( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n))%I.
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
Γ FG_increment (Loc cnt) log CG_locked_increment (Loc cnt') (Loc l) : (TArrow TUnit TUnit).
Proof.
iIntros "#Hinv".
Transparent CG_locked_increment with_lock.
unfold FG_increment, CG_locked_increment, with_lock.
iApply (bin_log_related_arrow); auto.
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ. simpl.
(* fold this stuff back *)
change (Rec
(App
(Rec
(App (Rec (App (Rec (Var 3)) (App release (Loc l))))
(App (CG_increment (Loc cnt')).[ren (+4)] (Var 3))))
(App acquire (Loc l))))
with (CG_locked_increment (Loc cnt') (Loc l)).
change (Rec
(App
(Rec
(If
(CAS (Loc cnt) (Var 1)
(BinOp Add (#n 1) (Var 1))) Unit
(App (Var 2) (Var 3)))) (Load (Loc cnt))))
with (FG_increment (Loc cnt)).
iLöb as "Hlat".
iApply (bin_log_related_rec_l _ _ []); auto. iNext. asimpl.
rel_bind_l (Load (Loc cnt)).
iApply (bin_log_related_load_l).
iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro.
iExists (#nv n). iSplit; eauto. iFrame "Hcnt".
iIntros "Hcnt". simpl.
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
iApply (bin_log_related_rec_l _ _ []); auto. iNext. asimpl.
rel_bind_l (BinOp Add (#n 1) (#n n)).
iApply (bin_log_related_binop_l). iNext. simpl.
rel_bind_l (CAS (Loc cnt) (#n n) (#n (S n))).
iApply (bin_log_related_cas_l); auto.
iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists (#nv m). iFrame "Hcnt".
destruct (decide (n = m)).
+ (* CAS succeeds *) subst. iSplitR; eauto.
{ iDestruct 1 as %Hfoo. by exfalso. }
iIntros "_ Hcnt". simpl.
iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl");
auto. solve_ndisj.
iIntros "Hcnt' Hl".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists (S m). iFrame. }
iApply (bin_log_related_if_true_l _ _ []); auto.
iNext. simpl.
iPoseProof (bin_log_related_unit [] ) as "H".
iExact "H". (* TODO iApply does not work *)
+ (* CAS fails *)
iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. }
iIntros "_ Hcnt". simpl.
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists m. iFrame. }
iApply (bin_log_related_if_false_l [] []); auto.
(* iApply (bin_log_related_bind_l []); auto. *)
(* iApply wp_rec; auto. iNext. simpl. *)
(* wp_bind (Load _). *)
(* iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". *)
(* iApply (wp_load with "Hcnt"). *)
(* iNext. iIntros "Hcnt". simpl. *)
(* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
(* { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } *)
(* iApply wp_rec; auto. iNext. simpl. *)
(* wp_bind (BinOp _ _ _). *)
(* iApply (wp_nat_binop). iNext. iModIntro. *)
(* wp_bind (CAS _ _ _). *)
(* iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose". *)
(* destruct (decide (n = m)). *)
(* + (* CAS succeeds *) subst. *)
(* iApply (wp_cas_suc with "Hcnt"); auto. *)
(* iNext. iIntros "Hcnt". *)
(* iApply wp_if_true. iApply wp_value; auto. *)
(* iApply fupd_mono. *)
(* { iApply uPred.later_intro. } *)
(* iApply fupd_frame_r. *)
(* iApply (uPred.sep_mono_r _ (cnt' ↦ₛ (#nv m) *)
(* l ↦ₛ (#v false) *)
(* [] Unit log Unit : TUnit)%I). *)
(* { simpl. iIntros "[Hcnt' [Hl Hlog]]". *)
(* iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl"); auto. } *)
(* i. *)
Opaque CG_locked_increment with_lock.
Qed.
Lemma FG_CG_counter_refinement :
[] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
unfold FG_counter, CG_counter.
iApply (bin_log_related_alloc_l [] _ _ [AppRCtx (RecV (FG_counter_body (Var 1)))]); auto; simpl. iModIntro.
iIntros (cnt) "Hcnt".
rel_bind_r newlock.
iApply (bin_log_related_newlock_r); auto; simpl.
iIntros (l) "Hl".
iApply (bin_log_related_rec_r [] []); auto. asimpl.
rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
rel_bind_r (Alloc (#n 0)).
rel_bind_l (Alloc _).
iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
iIntros (cnt) "Hcnt".
rel_bind_r (Alloc _).
iApply (bin_log_related_alloc_r); auto.
iIntros (cnt') "Hcnt' /=".
(* establishing the invariant *)
iAssert (( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n) )%I)
iAssert (counter_inv l cnt cnt')
with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. by iFrame. }
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". }
iApply (bin_log_related_rec_l [] []); auto.
iApply (bin_log_related_rec_l [] _ []); auto.
iNext. asimpl.
rewrite counter_read_subst /=.
......@@ -348,9 +523,8 @@ Section CG_Counter.
- Transparent counter_read.
unfold counter_read.
iApply (bin_log_related_rec); auto. iAlways. asimpl.
rel_bind_l (Load (Loc cnt)).
iApply (bin_log_related_load_l).
iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose".
iApply (bin_log_related_load_l _ _ _ []).
iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists (#nv n). iFrame "Hcnt". iSplit; eauto.
iIntros "Hcnt". simpl.
......@@ -359,153 +533,21 @@ Section CG_Counter.
iIntros "Hcnt'".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. by iFrame. }
simpl.
iPoseProof (bin_log_related_nat [TArrow TUnit TNat; TUnit] n) as "H". iFrame "H". (* TODO: iApply does not work in this case *)
- Transparent CG_locked_increment.
unfold CG_locked_increment.
Transparent with_lock.
unfold with_lock.
iApply (bin_log_related_arrow); auto.
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
(* fold this stuff back *)
change (Rec
(App
(Rec
(App (Rec (App (Rec (Var 3)) (App release (Loc l))))
(App (CG_increment (Loc cnt')).[ren (+4)] (Var 3))))
(App acquire (Loc l))))
with (CG_locked_increment (Loc cnt') (Loc l)).
iLöb as "Hlat".
iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl.
rel_bind_l (Load (Loc cnt)).
iApply (bin_log_related_load_l).
iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro.
iExists (#nv n). iSplit; eauto. iFrame "Hcnt".
iIntros "Hcnt". simpl.
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl.
rel_bind_l (BinOp Add (#n 1) (#n n)).
iApply (bin_log_related_binop_l). iNext. simpl.
rel_bind_l (CAS (Loc cnt) (#n n) (#n (S n))).
iApply (bin_log_related_cas_l); auto.
iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists (#nv m). iFrame "Hcnt".
destruct (decide (n = m)).
+ (* CAS succeeds *) subst. iSplitR; eauto.
{ iDestruct 1 as %Hfoo. by exfalso. }
iIntros "_ Hcnt". simpl.
iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl");
auto. solve_ndisj.
iIntros "Hcnt' Hl".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists (S m). iFrame. }
iApply (bin_log_related_if_true_l _ []); auto.
iNext. simpl. iPoseProof (bin_log_related_unit [] ) as "H".
iExact "H". (* TODO iApply does not work *)
+ (* CAS fails *)
iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. }
iIntros "_ Hcnt". simpl.
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists m. iFrame. }
iApply (bin_log_related_if_false_l [] []); auto.
simpl.
iApply (bin_log_related_val); auto.
intros. simpl. eauto.
- simpl. change ((Rec
(App
(Rec
(If
(CAS (Loc cnt) (ids 1)
(BinOp Add (#n 1) (ids 1))) Unit
(App (ids 2) (ids 3)))) (Load (Loc cnt)))))
with (FG_increment (Loc cnt)).
Opaque FG_increment.
iApply (FG_CG_increment_refinement with "Hinv").
Qed.
(* iIntros (Δ [|??] ρ) "#Hspec #HΓ"; iIntros (j K) "Hj"; last first. *)
(* { iDestruct (interp_env_length with "HΓ") as %[=]. } *)
(* iClear "HΓ". cbn -[FG_counter CG_counter]. *)
(* rewrite ?empty_env_subst /CG_counter /FG_counter. *)
(* iApply fupd_wp. *)
(* tp_bind j newlock. *)
(* tp_apply j steps_newlock. *)
(* iDestruct "Hj" as (l) "[Hj Hl]". *)
(* tp_rec j. *)
(* asimpl. rewrite CG_locked_increment_subst /=. *)
(* rewrite counter_read_subst /=. *)
(* tp_alloc j as cnt' "Hcnt'". tp_normalise j. *)
(* tp_rec j. tp_normalise j. *)
(* asimpl. rewrite CG_locked_increment_subst /=. *)
(* rewrite counter_read_subst /=. *)
(* iModIntro. wp_bind (Alloc _). *)
(* iApply wp_alloc; eauto. iNext. *)
(* iIntros (cnt) "Hcnt /=". *)
(* (* establishing the invariant *) *)
(* iAssert (( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n) )%I) *)
(* with "[Hl Hcnt Hcnt']" as "Hinv". *)
(* { iExists _. by iFrame. } *)
(* iApply fupd_wp. *)
(* iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial. *)
(* { iNext; iExact "Hinv". } *)
(* (* splitting increment and read *) *)
(* iApply wp_rec; trivial. iNext. asimpl. *)
(* rewrite counter_read_subst /=. *)
(* iApply wp_value; simpl. *)
(* { by rewrite counter_read_to_val. } *)
(* iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl. *)
(* rewrite CG_locked_increment_of_val counter_read_of_val. *)
(* iFrame "Hj". *)
(* iExists (_, _), (_, _); simpl; repeat iSplit; trivial. *)
(* - (* refinement of increment *) *)
(* iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj". *)
(* rewrite CG_locked_increment_of_val /=. *)
(* destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=. *)
(* iLöb as "Hlat". *)
(* iApply wp_rec; trivial. asimpl. iNext. *)
(* (* fine-grained reads the counter *) *)
(* wp_bind (Load _). *)
(* iApply wp_atomic; eauto. *)
(* iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose". *)
(* iApply (wp_load with "[Hcnt]"); [iNext; by iFrame|]. *)
(* iNext. iIntros "Hcnt". *)
(* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
(* { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } *)
(* iApply wp_rec; trivial. asimpl. iNext. *)
(* (* fine-grained performs increment *) *)
(* wp_bind (BinOp Add _ _). *)
(* iApply wp_nat_binop; simpl. *)
(* iNext. iModIntro. *)
(* wp_bind (CAS _ _ _). *)
(* iApply wp_atomic; eauto. *)
(* iInv counterN as (n') ">[Hl [Hcnt Hcnt']]" "Hclose". *)
(* (* performing CAS *) *)
(* destruct (decide (n = n')) as [|Hneq]; subst. *)
(* + (* CAS succeeds *) *)
(* (* In this case, we perform increment in the coarse-grained one *) *)
(* tp_apply j steps_CG_locked_increment with "Hcnt' Hl" *)
(* as "[Hcnt' Hl]". *)
(* iApply (wp_cas_suc with "[Hcnt]"); auto. *)
(* iNext. iIntros "Hcnt". *)
(* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
(* { iNext. iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. } *)
(* simpl. *)
(* iApply wp_if_true. iNext. iApply wp_value; trivial. *)
(* iExists UnitV; iFrame; auto. *)
(* + (* CAS fails *) *)
(* (* In this case, we perform a recursive call *) *)
(* iApply (wp_cas_fail _ _ _ (#nv n') with "[Hcnt]"); auto; *)
(* [inversion 1; subst; auto | ]. *)
(* iNext. iIntros "Hcnt". *)
(* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
(* { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". } *)
(* iApply wp_if_false. iNext. by iApply "Hlat". *)
(* - (* refinement of read *) *)
(* iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj". *)
(* rewrite ?counter_read_of_val. *)
(* iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=. *)
(* Transparent counter_read. *)
(* unfold counter_read at 2. *)
(* iApply wp_rec; trivial. simpl. *)
(* iNext. *)
(* iApply wp_atomic; eauto. *)
(* iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose". *)
(* tp_apply j steps_counter_read with "Hcnt'" as "Hcnt'". *)
(* iApply (wp_load with "[Hcnt]"); eauto. *)
(* iNext. iIntros "Hcnt". *)
(* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
(* { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". } *)
(* iExists (#nv _); eauto. *)
End CG_Counter.
Theorem counter_ctx_refinement :
......
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