From 752493b6c35e8fb61d4c2fbad34641eaeecd494a Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 29 Mar 2018 12:50:49 +0200 Subject: [PATCH] Better log. atomic spec. for weak increment --- theories/examples/ticket_lock.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v index a91ee00..59cd5db 100644 --- a/theories/examples/ticket_lock.v +++ b/theories/examples/ticket_lock.v @@ -319,13 +319,13 @@ Section refinement. cf wkIncr specification from (da Rocha Pinto, Dinsdale-Young, Gardner) Parameter type: nat Precondition: λn, x ↦ᵢ n - Postcondition λ_, ∃ n, x ↦ᵢ n + Postcondition λ_, ∃ n, x ↦ᵢ (n+1) *) Lemma wkincr_atomic_l R1 R2 Δ Γ E K x t τ : R2 -∗ □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗ - ((∃ n : nat, x ↦ᵢ #n ∗ R1 n) ={E,⊤}=∗ True) ∧ - (∀ m, (∃ n : nat, x ↦ᵢ #n) ∗ R1 m -∗ R2 -∗ + (x ↦ᵢ #n ∗ R1 n ={E,⊤}=∗ True) ∧ + ((∃ n : nat, x ↦ᵢ #(n + 1)) ∗ R1 n -∗ R2 -∗ {E;Δ;Γ} ⊨ fill K Unit ≤log≤ t : τ)) -∗ ({Δ;Γ} ⊨ fill K (wkincr #x) ≤log≤ t : τ). Proof. @@ -337,7 +337,7 @@ Section refinement. iMod "H" as (n) "[Hx [HR1 [Hrev _]]]". iModIntro. iExists _; iFrame. iNext. iIntros "Hx". iMod ("Hrev" with "[HR1 Hx]") as "_"; simpl. - { iExists _. iFrame. } + { iFrame. } rel_op_l. rel_store_l_atomic. iMod "H2" as (m) "[Hx [HR1 [_ Hmod]]]". iModIntro. @@ -364,15 +364,15 @@ Section refinement. openI. iModIntro. iExists _; iFrame. rewrite {1}/R. iSplitR "Hcl". - { iExists _,_; by iFrame. } clear o n b. + { iExists _,_; by iFrame. } iSplit. - - iDestruct 1 as (o) "[Hlo HR]". - unfold R. iDestruct "HR" as (n b) "HR". + - iIntros "[Hlo HR]". + unfold R. iDestruct "HR" as (n' b') "HR". iApply "Hcl". iNext. iExists _,_,_; by iFrame. - - iIntros (?) "[Hlo HR] _". - iDestruct "Hlo" as (o) "Hlo". - unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)". + - iIntros "[Hlo HR] _". + iDestruct "Hlo" as (o') "Hlo". + unfold R. iDestruct "HR" as (n' b') "(Hln & Hissued & Hl' & Hticket)". rel_apply_r (bin_log_related_release_r with "Hl'"). { solve_ndisj. } iIntros "Hl'". -- GitLab