From b97a821229568430f4355c460548d0ddfd3ed489 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 28 Mar 2018 20:07:04 +0200 Subject: [PATCH] Update the counter increment atomic rule --- theories/examples/counter.v | 41 +++++++++++++++------------------ theories/examples/ticket_lock.v | 31 ++++++++++++------------- theories/examples/various.v | 40 ++++++++++++++++---------------- 3 files changed, 53 insertions(+), 59 deletions(-) diff --git a/theories/examples/counter.v b/theories/examples/counter.v index ec7d8e0..2e8b28a 100644 --- a/theories/examples/counter.v +++ b/theories/examples/counter.v @@ -126,10 +126,10 @@ Section CG_Counter. Lemma bin_log_FG_increment_logatomic R P Γ E K x t τ : P -∗ □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗ - ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧ - (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗ - {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) - -∗ ({Δ;Γ} ⊨ fill K (FG_increment #x) ≤log≤ t : τ). + ((x ↦ᵢ #n ∗ R n ={E,⊤}=∗ True) ∧ + (x ↦ᵢ #(S n) ∗ R n -∗ P -∗ + {E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ))) + -∗ {Δ;Γ} ⊨ fill K (FG_increment #x) ≤log≤ t : τ. Proof. iIntros "HP #H". iLöb as "IH". @@ -140,18 +140,15 @@ Section CG_Counter. iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro. iExists #n. iFrame. iNext. iIntros "Hx". iDestruct "Hrev" as "[Hrev _]". - iMod ("Hrev" with "[HR Hx]") as "_". - { iExists _. iFrame. } simpl. - rel_rec_l. - rel_op_l. - rel_cas_l_atomic. + iMod ("Hrev" with "[HR Hx]") as "_"; first iFrame. + rel_rec_l. rel_op_l. rel_cas_l_atomic. iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl. destruct (decide (n = n')); subst. - iExists #n'. iFrame. iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. } iIntros "_ !> Hx". simpl. iDestruct "HQ" as "[_ HQ]". - iSpecialize ("HQ" \$! n' with "[Hx HR]"). { iFrame. } + iSpecialize ("HQ" with "[\$Hx \$HR]"). rel_if_true_l. by iApply "HQ". - iExists #n'. iFrame. iSplitL; eauto; last first. @@ -159,8 +156,7 @@ Section CG_Counter. iIntros "_ !> Hx". simpl. rel_if_false_l. iDestruct "HQ" as "[HQ _]". - iMod ("HQ" with "[Hx HR]"). - { iExists _; iFrame. } + iMod ("HQ" with "[\$Hx \$HR]"). rewrite /FG_increment. unlock. simpl. by iApply "IH". Qed. @@ -169,15 +165,14 @@ Section CG_Counter. Lemma bin_log_counter_read_atomic_l R P Γ E K x t τ : P -∗ □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗ - ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧ - (∀ m : nat, x ↦ᵢ #m ∗ R m -∗ P -∗ - {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) + (x ↦ᵢ #n ∗ R n ={E,⊤}=∗ True) ∧ + (x ↦ᵢ #n ∗ R n -∗ P -∗ + {E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ)) -∗ {Δ;Γ} ⊨ fill K ((counter_read \$/ LitV (Loc x)) #()) ≤log≤ t : τ. Proof. iIntros "HP #H". unfold counter_read. unlock. simpl. - rel_rec_l. - rel_load_l_atomic. + rel_rec_l. rel_load_l_atomic. iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro. iExists _; iFrame "Hx". iNext. iIntros "Hx". @@ -196,12 +191,12 @@ Section CG_Counter. True%I); first done. iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro. iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')". - iExists _; iFrame. clear n. + iExists _; iFrame. iSplit. - - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". + - iIntros "(Hcnt & Hl & Hcnt')". iApply ("Hcl" with "[-]"). iNext. iExists _. iFrame. - - iIntros (m) "(Hcnt & Hl & Hcnt') _". + - iIntros "(Hcnt & Hl & Hcnt') _". rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl"). { solve_ndisj. } iIntros "Hcnt' Hl". @@ -229,11 +224,11 @@ Section CG_Counter. True%I); first done. iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". iModIntro. - iExists n. iFrame "Hcnt Hcnt' Hl". clear n. + iExists n. iFrame "Hcnt Hcnt' Hl". iSplit. - - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose". + - iIntros "(Hcnt & Hl & Hcnt')". iApply "Hclose". iNext. iExists n. by iFrame. - - iIntros (m) "(Hcnt & Hl & Hcnt') _ /=". + - iIntros "(Hcnt & Hl & Hcnt') _ /=". rel_apply_r (bin_log_counter_read_r with "Hcnt'"). { solve_ndisj. } iIntros "Hcnt'". diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v index cd06961..a91ee00 100644 --- a/theories/examples/ticket_lock.v +++ b/theories/examples/ticket_lock.v @@ -196,8 +196,8 @@ Section refinement. Lemma acquire_l_logatomic R P γ Δ Γ E K lo ln t τ : P -∗ □ (|={⊤,E}=> ∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o ∗ - ((∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o) ={E,⊤}=∗ True) ∧ - (∀ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ ticket γ o ∗ R o -∗ P -∗ + (∀ o : nat, (∃ n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o) ={E,⊤}=∗ True) ∧ + (∀ o : nat, (∃ n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ ticket γ o ∗ R o) -∗ P -∗ {E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ)) -∗ ({Δ;Γ} ⊨ fill K (acquire (#lo, #ln)) ≤log≤ t : τ). Proof. @@ -213,33 +213,32 @@ Section refinement. { iExists _. iFrame. } iSplit. - iDestruct "Hrest" as "[H _]". - iDestruct 1 as (n') "[Hln Ho]". + iIntros "[Hln Ho]". iDestruct "Ho" as (o') "[Ho HR]". iApply "H". - iExists _, _. iFrame. + iExists _. iFrame. - iDestruct "Hrest" as "[H _]". - iIntros (n') "[Hln Ho] HP". + iIntros "[Hln Ho] HP". iDestruct "Ho" as (o') "[Ho [Hissued HR]]". iMod (issueNewTicket with "Hissued") as "[Hissued Hm]". iMod ("H" with "[-HP Hm]") as "_". - { iExists _,_. iFrame. } - rel_let_l. clear o n o'. - rel_rec_l. + { iExists _. iFrame. } clear o o'. + rel_let_l. rel_rec_l. iLöb as "IH". unlock wait_loop. simpl. rel_rec_l. rel_proj_l. rel_load_l_atomic. - iMod "H2" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro. + iMod "H2" as (o n') "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro. iExists _. iFrame. iNext. iIntros "Hlo". rel_op_l. case_decide; subst; rel_if_l. (* Whether the ticket is called out *) + iDestruct "Hrest" as "[_ H]". iApply ("H" with "[-HP] HP"). - { iFrame. } + { iExists _. iFrame. } + iDestruct "Hrest" as "[H _]". iMod ("H" with "[-HP Hm]") as "_". - { iExists _,_; iFrame. } + { iExists _. iFrame. } rel_rec_l. iApply ("IH" with "HP Hm"). Qed. @@ -263,12 +262,12 @@ Section refinement. { iExists _. iFrame. } clear b o n. iSplit. - - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)". + - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Hrest)". iDestruct "Hrest" as (b) "[Hl' Ht]". iApply ("Hcl" with "[-]"). iNext. iExists _,_,_. by iFrame. - - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _". - iDestruct "Hrest" as (b) "[Hl' Ht']". + - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Ht & Hrest)". + iIntros "_". iDestruct "Hrest" as (b) "[Hl' Ht']". destruct b. { iDestruct (ticket_nondup with "Ht Ht'") as %[]. } rel_apply_r (bin_log_related_acquire_r with "Hl'"). @@ -293,10 +292,10 @@ Section refinement. openI. iModIntro. iExists _; iFrame. iSplit. - - iDestruct 1 as (m) "[Hln ?]". + - iIntros "[Hln ?]". iApply ("Hcl" with "[-]"). iNext. iExists _,_,_; by iFrame. - - iIntros (m) "[Hln Hissued] _". + - iIntros "[Hln Hissued] _". iMod (issueNewTicket with "Hissued") as "[Hissued Hm]". iMod ("Hcl" with "[-Hm]") as "_". { iNext. iExists _,_,_; by iFrame. } diff --git a/theories/examples/various.v b/theories/examples/various.v index 3c64eaf..90c4c62 100644 --- a/theories/examples/various.v +++ b/theories/examples/various.v @@ -395,21 +395,21 @@ Section refinement. - iSplitL "Hc2 Ht". { iLeft. iFrame. } iSplit. - { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]"; + { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]"; iApply ("Hcl" with "[-]"); iNext. - + iExists m. iLeft. iFrame. - + iExists (m-1). iRight. + + iExists n. iLeft. iFrame. + + iExists (n-1). iRight. rewrite minus_Sn_m // /= -minus_n_O. iFrame. } - { iIntros (m) "[Hc1 Hc] _". + { iIntros "[Hc1 Hc] _". iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]"; (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj); iIntros "Hc2". - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists (S m). iFrame. iLeft; iFrame. } + { iNext. iExists (S n). iFrame. iLeft; iFrame. } rel_finish. - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists m. + { iNext. iExists n. rewrite minus_Sn_m // /= -minus_n_O. iFrame. iRight; iFrame. } rel_finish. } @@ -418,23 +418,21 @@ Section refinement. iDestruct "Ht" as "[\$ \$]". iPureIntro. omega. } iSplit. - { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]"; + { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]"; iApply ("Hcl" with "[-]"); iNext. - + iExists m. iLeft. iFrame. - + iExists (m-1). iRight. - rewrite minus_Sn_m // /= -minus_n_O. - iFrame. } - { iIntros (m) "[Hc1 Hc] _". + + iExists (S n). iLeft. iFrame. + + iExists n. iRight. iFrame. + assert (S n - 1 = n) as -> by omega. done. } + { iIntros "[Hc1 Hc] _". iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]"; (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj); iIntros "Hc2". - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists (S m). iFrame. iLeft; iFrame. } + { iNext. iExists (S (S n)). iFrame. iLeft; iFrame. } rel_finish. - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists m. - rewrite minus_Sn_m // /= -minus_n_O. - iFrame. iRight; iFrame. } + { iNext. iExists (S n). iRight. iFrame. + by rewrite -minus_n_O. } rel_finish. } Qed. @@ -560,16 +558,18 @@ Section refinement. { 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". + - iIntros. iApply "Hcl". iApply close_i6. + iNext. iExists _; iFrame. + - iIntros "[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". + - iIntros. iApply "Hcl". iApply close_i6. + iNext. iExists _; iFrame. + - iIntros "[Hc1 Hc2] Ht". rel_seq_l. iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht"). } -- 2.26.2