From 0cc65541038e41ee3cd1ed9752225dcb2e067a6e Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 19 Oct 2017 09:59:34 +0200 Subject: [PATCH] Generalize the logatomic rule for the counter increment --- theories/examples/counter.v | 15 ++-- theories/examples/various.v | 137 +++++++++++++++++++++--------------- 2 files changed, 87 insertions(+), 65 deletions(-) diff --git a/theories/examples/counter.v b/theories/examples/counter.v index 2c9a7ca..6d3ccb6 100644 --- a/theories/examples/counter.v +++ b/theories/examples/counter.v @@ -123,14 +123,15 @@ Section CG_Counter. (* A logically atomic specification for a fine-grained increment with a baked in frame. *) (* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *) - Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ : + Lemma bin_log_FG_increment_logatomic R P Γ E1 E2 K x t τ : + P -∗ □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗ ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧ - (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ + (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗ {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ)) -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ). Proof. - iIntros "#H". + iIntros "HP #H". iLöb as "IH". rewrite {2}/FG_increment. unlock. simpl. rel_rec_l. @@ -152,7 +153,7 @@ Section CG_Counter. iIntros "_ !> Hx". simpl. iDestruct "HQ" as "[_ HQ]". iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. } - rel_if_true_l. done. + rel_if_true_l. by iApply "HQ". - iExists #n'. iFrame. iSplitL; eauto; last first. { iDestruct 1 as %Hfoo. exfalso. simplify_eq. } @@ -162,7 +163,7 @@ Section CG_Counter. iMod ("HQ" with "[Hx HR]"). { iExists _; iFrame. } rewrite /FG_increment. unlock. simpl. - iApply "IH". + by iApply "IH". Qed. (* A similar atomic specification for the counter_read fn *) @@ -197,7 +198,7 @@ Section CG_Counter. { unfold CG_increment. unlock; simpl_subst/=. solve_closed. } iAlways. iIntros (v v') "[% %]"; simpl in *; subst. - iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]"). + iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I True%I _ _ _ [] cnt with "[Hinv]"); auto. iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro. iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". @@ -207,7 +208,7 @@ Section CG_Counter. iMod ("Hcl" with "[-]"). { iNext. iExists _. iFrame. } done. - - iIntros (m) "[Hcnt [Hl Hcnt']]". + - iIntros (m) "[Hcnt [Hl Hcnt']] _". iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. } iIntros "Hcnt' Hl". iMod ("Hcl" with "[-]"). diff --git a/theories/examples/various.v b/theories/examples/various.v index ce3a5f8..0fa5054 100644 --- a/theories/examples/various.v +++ b/theories/examples/various.v @@ -331,7 +331,7 @@ Section refinement. iApply bin_log_related_unit. } rel_rec_l. rel_apply_l (bin_log_FG_increment_logatomic _ - (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I). + (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I True%I); first done. iAlways. iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl"; iModIntro; iExists _; iFrame. @@ -344,7 +344,7 @@ Section refinement. + iExists (m-1). iRight. rewrite minus_Sn_m // /= -minus_n_O. iFrame. } - { iIntros (m) "[Hc1 Hc]". + { iIntros (m) "[Hc1 Hc] _". iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]". - unlock FG_increment. simpl. rel_rec_r. rel_rec_r. @@ -377,7 +377,7 @@ Section refinement. + iExists (m-1). iRight. rewrite minus_Sn_m // /= -minus_n_O. iFrame. } - { iIntros (m) "[Hc1 Hc]". + { iIntros (m) "[Hc1 Hc] _". iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]". - unlock FG_increment. simpl. rel_rec_r. rel_rec_r. @@ -416,6 +416,63 @@ Section refinement. iApply profiled_g; eauto. Qed. + Lemma close_i6 c1 c2 γ γ' `{oneshotG Σ} `{inG Σ (exclR unitR)} : + ((∃ n : nat, c1 ↦ᵢ #n + ∗ (c2 ↦ₛ #n ∗ pending γ + ∨ c2 ↦ₛ #(n - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝)) + -∗ i6 c1 c2 γ γ')%I. + Proof. + iDestruct 1 as (m) "[Hc1 Hc2]". + iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]"; + [iExists m; iLeft | iExists (m - 1); iRight]; iFrame. + rewrite minus_Sn_m // /= -minus_n_O; done. + Qed. + + Lemma refinement6_helper Δ Γ f'1 f'2 g1 g2 c1 c2 γ γ' m `{oneshotG Σ} `{inG Σ (exclR unitR)} : + inv shootN (i6 c1 c2 γ γ') -∗ + ⟦ τg ⟧ Δ (g1, g2) -∗ + ⟦ τf ⟧ Δ (f'1, f'2) -∗ + (▷ i6 c1 c2 γ γ' ={⊤ ∖ ↑shootN,⊤}=∗ True) -∗ + c1 ↦ᵢ #(S m) -∗ + (c2 ↦ₛ #m ∗ pending γ + ∨ c2 ↦ₛ #(m - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ m⌝) -∗ + own γ' (Excl ()) -∗ + {⊤ ∖ ↑shootN,⊤;Δ;Γ} ⊨ + (g1 #() ;; f'1 (λ: <>, (FG_increment #c1) #() ;; g1 #()) ;; #() ;; ! #c1) + ≤log≤ + (g2 #() ;; + f'2 (λ: <>, (FG_increment #c2) #() ;; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat. + Proof. + iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht". + iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first. + { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo. + inversion Hfoo. } + iApply fupd_logrel. + iMod (shoot γ with "Hp") as "#Hs". + iMod ("Hcl" with "[-]") as "_". + { iNext. iExists m. iRight. iFrame. done. } + iModIntro. + iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto. + { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]"). + iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. + iApply bin_log_related_unit. } + iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto. + { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]"). + iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. + by iApply profiled_g'. } + rel_seq_l. rel_seq_r. + rel_load_l_atomic. clear m. + iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl"; + iModIntro; iExists _; iFrame. + { iExFalso. by iApply shot_not_pending. } + iNext. iIntros "Hc1". + rel_load_r. rel_op_r. + iMod ("Hcl" with "[-]") as "_". + { iNext. iExists m. iRight. iFrame. } + rewrite Nat.add_1_r. + iApply bin_log_related_nat. + Qed. + Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} Γ : Γ ⊨ (λ: "f" "g" "f'", @@ -463,63 +520,27 @@ Section refinement. iApply profiled_g'; eauto. } rel_seq_l. rel_bind_l (FG_increment _). rel_rec_l. - (* rel_apply_l (bin_log_FG_increment_logatomic _ *) - (* (fun (n : nat) => own γ' (Excl ()) ∗ (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ ⌜1 ≤ n⌝))%I). *) - unlock {2}FG_increment. simpl. - (* rel_rec_l. TODO: doesn't work :( *) - iLöb as "IH". - rel_pure_l (App (Rec "inc" _ _) _). - rel_load_l_atomic. + rel_apply_l (bin_log_FG_increment_logatomic _ + (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I with "Ht'"). + iAlways. iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl"; iModIntro; iExists _; iFrame; last first. - { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo. - inversion Hfoo. } - iNext. iIntros "Hc1". - iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_". - { iNext. iExists n. iLeft. iFrame. } - (* rel_let_l. TODO: doesn't work :( *) - rel_pure_l (App (Lam "c" _) _). - rel_op_l. - rel_cas_l_atomic. - iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl"; - iModIntro; iExists _; iFrame; last first. - { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo. - inversion Hfoo. } - iSplit. - - iIntros (?). - iNext. iIntros "Hc1". - iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_". - { iNext. iExists m. iLeft. iFrame. } - rel_if_l. - by iApply "IH". - - iIntros (?); simplify_eq/=. - iNext. iIntros "Hc1". - iApply fupd_logrel. - iMod (shoot γ with "Ht") as "#Hs". - iMod ("Hcl" with "[Hc1 Hc2 Hs Ht']") as "_". - { iNext. iExists n. iRight. iFrame. done. } - iModIntro. - rel_if_l. - rel_seq_l. - iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto. - { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]"). - iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. - iApply bin_log_related_unit. } - iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto. - { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]"). - iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. - by iApply profiled_g'. } - rel_seq_l. rel_seq_r. - rel_load_l_atomic. - iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl"; - iModIntro; iExists _; iFrame. - { iExFalso. by iApply shot_not_pending. } - iNext. iIntros "Hc1". - rel_load_r. rel_op_r. - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists m. iRight. iFrame. } - rewrite Nat.add_1_r. - iApply bin_log_related_nat. + { iSplitL "Hc2 Ht Ht'2". + { iRight. simpl. rewrite -minus_n_O. iFrame. iPureIntro. omega. } + iSplit. + - iIntros. iApply "Hcl". by iApply close_i6. + - iIntros (m) "[Hc1 Hc2] Ht". + rel_seq_l. + iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht"). + } + { iSplitL "Hc2 Ht". + { iLeft. by iFrame. } + iSplit. + - iIntros. iApply "Hcl". by iApply close_i6. + - iIntros (m) "[Hc1 Hc2] Ht". + rel_seq_l. + iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht"). + } Qed. End refinement. -- GitLab