From a709fc366fe8c5e0e57a100bec1dd2ef574ff1e0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 20 Jul 2016 11:03:23 +0200 Subject: [PATCH] Make lock and counter consistent with spawn. --- heap_lang/lib/counter.v | 14 +++++++------- heap_lang/lib/lock.v | 20 ++++++++++---------- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 579e923..bd7c6a9 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -20,20 +20,20 @@ Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ. Proof. destruct H; split; apply _. Qed. Section proof. -Context `{!heapG Σ, !counterG Σ}. +Context `{!heapG Σ, !counterG Σ} (N : namespace). Local Notation iProp := (iPropG heap_lang Σ). Definition counter_inv (l : loc) (n : mnat) : iProp := (l ↦ #n)%I. Definition counter (l : loc) (n : nat) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ - auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I. + (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ + auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I. (** The main proofs. *) Global Instance counter_persistent l n : PersistentP (counter l n). Proof. apply _. Qed. -Lemma newcounter_spec N (R : iProp) Φ : +Lemma newcounter_spec (R : iProp) Φ : heapN ⊥ N → heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}. Proof. @@ -47,7 +47,7 @@ Lemma inc_spec l j (Φ : val → iProp) : counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}. Proof. iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. - iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)". + iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)". wp_focus (! _)%E. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV. iIntros "{\$Hγ \$Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv. @@ -62,7 +62,7 @@ Proof. rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia. rewrite Nat2Z.inj_succ -Z.add_1_l. iIntros "{\$Hl} Hγf". wp_if. - iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto. + iPvsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto. iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia. - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]). iPvsIntro. iExists j; iSplit; [done|iIntros "{\$Hl} Hγf"]. @@ -73,7 +73,7 @@ Lemma read_spec l j (Φ : val → iProp) : counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i) ⊢ WP read #l {{ Φ }}. Proof. - iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)". + iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)". rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV. iIntros "{\$Hγ \$Hγf}"; iIntros (j') "[% Hl] /=". diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v index 777abe5..bc755b1 100644 --- a/heap_lang/lib/lock.v +++ b/heap_lang/lib/lock.v @@ -18,18 +18,18 @@ Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ. Proof. destruct H. split. apply: inGF_inG. Qed. Section proof. -Context `{!heapG Σ, !lockG Σ}. +Context `{!heapG Σ, !lockG Σ} (N : namespace). Local Notation iProp := (iPropG heap_lang Σ). Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp := (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I. Definition is_lock (l : loc) (R : iProp) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ l R))%I. + (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ l R))%I. Definition locked (l : loc) (R : iProp) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ - inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I. + (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ + inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I. Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l). Proof. solve_proper. Qed. @@ -43,9 +43,9 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R). Proof. apply _. Qed. Lemma locked_is_lock l R : locked l R ⊢ is_lock l R. -Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed. +Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&?&_)"; eauto. Qed. -Lemma newlock_spec N (R : iProp) Φ : +Lemma newlock_spec (R : iProp) Φ : heapN ⊥ N → heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}. Proof. @@ -54,13 +54,13 @@ Proof. iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done. { iIntros ">". iExists false. by iFrame. } - iPvsIntro. iApply "HΦ". iExists N, γ; eauto. + iPvsIntro. iApply "HΦ". iExists γ; eauto. Qed. Lemma acquire_spec l R (Φ : val → iProp) : is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}. Proof. - iIntros "[Hl HΦ]". iDestruct "Hl" as (N γ) "(%&#?&#?)". + iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)". iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. iInv N as ([]) "[Hl HR]". - wp_cas_fail. iPvsIntro; iSplitL "Hl". @@ -68,13 +68,13 @@ Proof. + wp_if. by iApply "IH". - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl". + iNext. iExists true; eauto. - + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto. + + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto. Qed. Lemma release_spec R l (Φ : val → iProp) : locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}. Proof. - iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)". + iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)". rewrite /release. wp_let. iInv N as (b) "[Hl _]". wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame. Qed. -- GitLab