Commit 5cabd278 authored by Robbert Krebbers's avatar Robbert Krebbers

Explicit namespaces for counter, lock and spawn.

parent 6e487530
......@@ -5,6 +5,8 @@ From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
Definition counterN : namespace := nroot .@ "counter".
Definition newcounter : val := λ: <>, ref #0.
Definition inc : val :=
rec: "inc" "l" :=
......@@ -26,19 +28,17 @@ 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.
( γ, heap_ctx auth_ctx γ counterN (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) Φ :
heapN N
Lemma newcounter_spec (R : iProp) Φ :
heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
iIntros "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) counterN _ (O:mnat) with "[Hl]")
as (γ) "[#? Hγ]"; try by auto.
iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
Qed.
......@@ -47,13 +47,13 @@ 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 (γ) "(#Hh & #Hγ & Hγf)".
wp_focus (! _)%E.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op. wp_focus (CAS _ _ _).
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
......@@ -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,9 +73,9 @@ 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 (γ) "(#Hh & #Hγ & Hγf)".
rewrite /read. wp_let.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. }
......
......@@ -3,6 +3,8 @@ From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
Definition lockN : namespace := nroot .@ "lock".
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "acquire" "l" :=
......@@ -25,11 +27,10 @@ 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.
( γ, heap_ctx inv lockN (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.
( γ, heap_ctx inv lockN (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,39 +44,38 @@ 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) Φ :
heapN N
Lemma newlock_spec (R : iProp) Φ :
heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
iIntros "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
iPvs (inv_alloc lockN _ (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 (γ) "[#Hh #?]".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as ([]) "[Hl HR]".
iInv lockN as ([]) "[Hl HR]".
- wp_cas_fail. iPvsIntro; iSplitL "Hl".
+ iNext. iExists true; eauto.
+ 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γ)".
rewrite /release. wp_let. iInv N as (b) "[Hl _]".
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(#Hh & #? & Hγ)".
rewrite /release. wp_let. iInv lockN as (b) "[Hl _]".
wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
Qed.
End proof.
......@@ -12,16 +12,16 @@ Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Global Opaque par.
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Context `{!heapG Σ, !spawnG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Lemma par_spec (Ψ1 Ψ2 : val iProp) e (f1 f2 : val) (Φ : val iProp) :
heapN N to_val e = Some (f1,f2)%V
to_val e = Some (f1,f2)%V
(heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}.
Proof.
iIntros (??) "(#Hh&Hf1&Hf2&HΦ)".
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
......@@ -32,12 +32,11 @@ Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp) :
heapN N
(heap_ctx WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }}
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP e1 || e2 {{ Φ }}.
Proof.
iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
iFrame "Hh H". iSplitL "H1"; by wp_let.
Qed.
End proof.
......@@ -3,6 +3,8 @@ From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
Definition spawnN : namespace := nroot .@ "spawn".
Definition spawn : val :=
λ: "f",
let: "c" := ref NONE in
......@@ -28,7 +30,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Context `{!heapG Σ, !spawnG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp :=
......@@ -36,8 +38,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp) : iProp :=
(heapN N γ, heap_ctx own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I.
( γ, heap_ctx own γ (Excl ()) inv spawnN (spawn_inv γ l Ψ))%I.
Typeclasses Opaque join_handle.
......@@ -51,19 +52,18 @@ Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) :
to_val e = Some f
heapN N
heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
iIntros (<-%of_to_val) "(#Hh & Hf & HΦ)". rewrite /spawn.
wp_let. wp_alloc l as "Hl". wp_let.
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
iPvs (inv_alloc spawnN _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]".
iInv spawnN as (v') "[Hl _]".
wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (SOMEV v). iFrame. eauto.
Qed.
......@@ -71,8 +71,8 @@ Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
rewrite /join_handle; iIntros "[H Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv spawnN as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ Hv").
......
......@@ -41,8 +41,8 @@ Section client.
iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs".
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "Hy Hs".
- (* The original thread, the sender. *)
wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
......@@ -51,8 +51,8 @@ Section client.
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par N (λ _, True%I) (λ _, True%I)); eauto.
iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]];
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]];
iApply worker_safe; by iSplit.
Qed.
End client.
......
......@@ -77,8 +77,7 @@ Proof.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iFrame "Hh". iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par _ (λ _, True)%I workers_post);
try iFrame "Hh"; first done.
wp_let. wp_apply (wp_par (λ _, True)%I workers_post); iFrame "Hh".
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
......@@ -88,8 +87,8 @@ Proof.
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par _ (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); try iFrame "Hh"; first done.
wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); iFrame "Hh".
iSplitL "H1"; [|iSplitL "H2"].
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
......
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