Commit a709fc36 authored by Robbert Krebbers's avatar Robbert Krebbers

Make lock and counter consistent with spawn.

parent e67a4876
......@@ -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] /=".
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment