From 4443b5c3c25132fa94f18b2d0e5945b80107d079 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 6 Dec 2016 19:55:43 +0100 Subject: [PATCH] try another approach to taming simpl --- heap_lang/lib/counter.v | 20 +++++++++----------- heap_lang/lib/ticket_lock.v | 20 ++++++++++---------- heap_lang/lifting.v | 10 ++++++++++ heap_lang/wp_tactics.v | 2 +- 4 files changed, 30 insertions(+), 22 deletions(-) diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 4391887a..097bd7fb 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -4,12 +4,12 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import frac auth. From iris.heap_lang Require Import proofmode notation. -Definition newcounter : val := λ: <>, ref #0. -Definition incr : val := +Definition newcounter : val := locked (λ: <>, ref #0)%V. +Definition incr : val := locked ( rec: "incr" "l" := let: "n" := !"l" in - if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". -Definition read : val := λ: "l", !"l". + if: CAS "l" "n" (#1 + "n") then #() else "incr" "l")%V. +Definition read : val := locked (λ: "l", !"l")%V. (** Monotone counter *) Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }. @@ -36,7 +36,7 @@ Section mono_proof. heapN ⊥ N → {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}. Proof. - iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". + iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl". iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done. iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]"). { iNext. iExists 0%nat. by iFrame. } @@ -72,7 +72,7 @@ Section mono_proof. {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}. Proof. iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)". - rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. iDestruct (own_valid_2 with "Hγ Hγf") as %[?%mnat_included _]%auth_valid_discrete_2. iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". @@ -113,7 +113,7 @@ Section contrib_spec. {{{ heap_ctx }}} newcounter #() {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}. Proof. - iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". + iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl". iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat)))) as (γ) "[Hγ Hγ']"; first done. iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]"). @@ -147,7 +147,7 @@ Section contrib_spec. {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". - rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. iDestruct (own_valid_2 with "Hγ Hγf") as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. @@ -159,12 +159,10 @@ Section contrib_spec. {{{ n, RET #n; ccounter γ 1 n }}}. Proof. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". - rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. + rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2. apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. by iApply "HΦ". Qed. End contrib_spec. - -Global Opaque newcounter incr get. diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v index eab626e5..8e16f24e 100644 --- a/heap_lang/lib/ticket_lock.v +++ b/heap_lang/lib/ticket_lock.v @@ -7,23 +7,24 @@ From iris.heap_lang.lib Require Export lock. Import uPred. Definition wait_loop: val := - rec: "wait_loop" "x" "lk" := + ssreflect.locked (rec: "wait_loop" "x" "lk" := let: "o" := !(Fst "lk") in if: "x" = "o" then #() (* my turn *) - else "wait_loop" "x" "lk". + else "wait_loop" "x" "lk")%V. -Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0). +Definition newlock : val := + ssreflect.locked (λ: <>, ((* owner *) ref #0, (* next *) ref #0))%V. Definition acquire : val := - rec: "acquire" "lk" := + ssreflect.locked (rec: "acquire" "lk" := let: "n" := !(Snd "lk") in if: CAS (Snd "lk") "n" ("n" + #1) then wait_loop "n" "lk" - else "acquire" "lk". + else "acquire" "lk")%V. -Definition release : val := λ: "lk", - (Fst "lk") <- !(Fst "lk") + #1. +Definition release : val := + ssreflect.locked (λ: "lk", (Fst "lk") <- !(Fst "lk") + #1)%V. (** The CMRAs we need. *) Class tlockG Σ := @@ -76,7 +77,7 @@ Section proof. heapN ⊥ N → {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}. Proof. - iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=. + iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock. unlock. wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln". iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']". { by rewrite -auth_both_op. } @@ -144,7 +145,7 @@ Section proof. iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst. iDestruct "Hγ" as (o) "Hγo". - rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E. + rewrite /release. unlock. wp_let. wp_proj. wp_proj. wp_bind (! _)%E. iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". wp_load. iDestruct (own_valid_2 with "Hauth Hγo") as @@ -168,7 +169,6 @@ Section proof. End proof. Typeclasses Opaque is_lock issued locked. -Global Opaque newlock acquire release wait_loop. Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ := {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec; diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index eb07aaa0..ee50b4a8 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -111,6 +111,16 @@ Proof. intros; inv_head_step; eauto. Qed. +Lemma wp_rec_locked E f x erec (e1 e2 : expr) Φ `{!Closed (f :b: x :b: []) erec} : + e1 = of_val \$ locked (RecV f x erec) → + is_Some (to_val e2) → + ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}. +Proof. + intros -> [v2 ?]. unlock. rewrite -(wp_lift_pure_det_head_step' (App _ _) + (subst' x e2 (subst' f (Rec f x erec) erec))); eauto. + intros; inv_head_step; eauto. +Qed. + Lemma wp_un_op E op e v v' Φ : to_val e = Some v → un_op_eval op v = Some v' → diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v index 26856a3a..bc647d8e 100644 --- a/heap_lang/wp_tactics.v +++ b/heap_lang/wp_tactics.v @@ -50,7 +50,7 @@ Tactic Notation "wp_rec" := match eval hnf in e' with App ?e1 _ => (* hnf does not reduce through an of_val *) (* match eval hnf in e1 with Rec _ _ _ => *) - wp_bind_core K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish + wp_bind_core K; etrans; [|(eapply wp_rec; wp_done) || (eapply wp_rec_locked; wp_done)]; simpl_subst; wp_finish (* end *) end) || fail "wp_rec: cannot find 'Rec' in" e | _ => fail "wp_rec: not a 'wp'" end. -- GitLab