Commit e67a4876 authored by Robbert Krebbers's avatar Robbert Krebbers

Partially revert "Explicit namespaces for counter, lock and spawn."

In order to improve flexibility, I have reverted the changes in commit
5cabd278 to counter, lock and spawn because an explicit namespace may be in
the way of modularity, for example, if the interfaces of these libraries will
expose namespaces through view shifts in the future.

Exposure of namespaces in the case of par is very unlikely, so to that end,
par remains to use an explicit namespace.
parent 247eecb1
...@@ -5,8 +5,6 @@ From iris.proofmode Require Import invariants ghost_ownership coq_tactics. ...@@ -5,8 +5,6 @@ From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Import uPred. Import uPred.
Definition counterN : namespace := nroot .@ "counter".
Definition newcounter : val := λ: <>, ref #0. Definition newcounter : val := λ: <>, ref #0.
Definition inc : val := Definition inc : val :=
rec: "inc" "l" := rec: "inc" "l" :=
...@@ -28,17 +26,19 @@ Local Notation iProp := (iPropG heap_lang Σ). ...@@ -28,17 +26,19 @@ Local Notation iProp := (iPropG heap_lang Σ).
Definition counter_inv (l : loc) (n : mnat) : iProp := (l #n)%I. Definition counter_inv (l : loc) (n : mnat) : iProp := (l #n)%I.
Definition counter (l : loc) (n : nat) : iProp := Definition counter (l : loc) (n : nat) : iProp :=
( γ, heap_ctx auth_ctx γ counterN (counter_inv l) auth_own γ (n:mnat))%I. ( N γ, heapN N heap_ctx
auth_ctx γ N (counter_inv l) auth_own γ (n:mnat))%I.
(** The main proofs. *) (** The main proofs. *)
Global Instance counter_persistent l n : PersistentP (counter l n). Global Instance counter_persistent l n : PersistentP (counter l n).
Proof. apply _. Qed. Proof. apply _. Qed.
Lemma newcounter_spec (R : iProp) Φ : Lemma newcounter_spec N (R : iProp) Φ :
heapN N
heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}. heap_ctx ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof. Proof.
iIntros "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) counterN _ (O:mnat) with "[Hl]") iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
as (γ) "[#? Hγ]"; try by auto. as (γ) "[#? Hγ]"; try by auto.
iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10. iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
Qed. Qed.
...@@ -47,13 +47,13 @@ Lemma inc_spec l j (Φ : val → iProp) : ...@@ -47,13 +47,13 @@ Lemma inc_spec l j (Φ : val → iProp) :
counter l j (counter l (S j) - Φ #()) WP inc #l {{ Φ }}. counter l j (counter l (S j) - Φ #()) WP inc #l {{ Φ }}.
Proof. Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(#Hh & #Hγ & Hγf)". iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E. wp_focus (! _)%E.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv. iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"]. wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op. wp_focus (CAS _ _ _). wp_let; wp_op. wp_focus (CAS _ _ _).
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv. iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj]. destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro. - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
...@@ -62,7 +62,7 @@ Proof. ...@@ -62,7 +62,7 @@ Proof.
rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia. rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
rewrite Nat2Z.inj_succ -Z.add_1_l. rewrite Nat2Z.inj_succ -Z.add_1_l.
iIntros "{$Hl} Hγf". wp_if. iIntros "{$Hl} Hγf". wp_if.
iPvsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto. iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto.
iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia. iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
- wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]). - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"]. iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
...@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) : ...@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) :
counter l j ( i, (j i)%nat counter l i - Φ #i) counter l j ( i, (j i)%nat counter l i - Φ #i)
WP read #l {{ Φ }}. WP read #l {{ Φ }}.
Proof. Proof.
iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(#Hh & #Hγ & Hγf)". iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let. rewrite /read. wp_let.
iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV.
iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=". iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit. wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. } { iPureIntro; apply mnat_local_update; abstract lia. }
......
...@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership. ...@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Import uPred. Import uPred.
Definition lockN : namespace := nroot .@ "lock".
Definition newlock : val := λ: <>, ref #false. Definition newlock : val := λ: <>, ref #false.
Definition acquire : val := Definition acquire : val :=
rec: "acquire" "l" := rec: "acquire" "l" :=
...@@ -27,10 +25,11 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp := ...@@ -27,10 +25,11 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I. ( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (l : loc) (R : iProp) : iProp := Definition is_lock (l : loc) (R : iProp) : iProp :=
( γ, heap_ctx inv lockN (lock_inv γ l R))%I. ( N γ, heapN N heap_ctx inv N (lock_inv γ l R))%I.
Definition locked (l : loc) (R : iProp) : iProp := Definition locked (l : loc) (R : iProp) : iProp :=
( γ, heap_ctx inv lockN (lock_inv γ l R) own γ (Excl ()))%I. ( N γ, 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). Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -44,38 +43,39 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R). ...@@ -44,38 +43,39 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed. Proof. apply _. Qed.
Lemma locked_is_lock l R : locked l R is_lock l R. Lemma locked_is_lock l R : locked l R is_lock l R.
Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&_)"; eauto. Qed. Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec (R : iProp) Φ : Lemma newlock_spec N (R : iProp) Φ :
heapN N
heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}. heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof. Proof.
iIntros "(#Hh & HR & HΦ)". rewrite /newlock. iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl". wp_seq. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc lockN _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done. iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame. } { iIntros ">". iExists false. by iFrame. }
iPvsIntro. iApply "HΦ". iExists γ; eauto. iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
Qed. Qed.
Lemma acquire_spec l R (Φ : val iProp) : Lemma acquire_spec l R (Φ : val iProp) :
is_lock l R (locked l R - R - Φ #()) WP acquire #l {{ Φ }}. is_lock l R (locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof. Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "[#Hh #?]". iIntros "[Hl HΦ]". iDestruct "Hl" as (N γ) "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv lockN as ([]) "[Hl HR]". iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iPvsIntro; iSplitL "Hl". - wp_cas_fail. iPvsIntro; iSplitL "Hl".
+ iNext. iExists true; eauto. + iNext. iExists true; eauto.
+ wp_if. by iApply "IH". + wp_if. by iApply "IH".
- wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl". - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+ iNext. iExists true; eauto. + iNext. iExists true; eauto.
+ wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto. + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto.
Qed. Qed.
Lemma release_spec R l (Φ : val iProp) : Lemma release_spec R l (Φ : val iProp) :
locked l R R Φ #() WP release #l {{ Φ }}. locked l R R Φ #() WP release #l {{ Φ }}.
Proof. Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(#Hh & #? & Hγ)". iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv lockN as (b) "[Hl _]". rewrite /release. wp_let. iInv N as (b) "[Hl _]".
wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame. wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
Qed. Qed.
End proof. End proof.
...@@ -2,6 +2,8 @@ From iris.heap_lang Require Export spawn. ...@@ -2,6 +2,8 @@ From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Import uPred. Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val := Definition par : val :=
λ: "fs", λ: "fs",
let: "handle" := spawn (Fst "fs") in let: "handle" := spawn (Fst "fs") in
...@@ -23,7 +25,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) : ...@@ -23,7 +25,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
Proof. Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)". iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj. rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh". wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _). iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let. iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros (w) "H1". wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
......
...@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership. ...@@ -3,8 +3,6 @@ From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Import uPred. Import uPred.
Definition spawnN : namespace := nroot .@ "spawn".
Definition spawn : val := Definition spawn : val :=
λ: "f", λ: "f",
let: "c" := ref NONE in let: "c" := ref NONE in
...@@ -30,7 +28,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed. ...@@ -30,7 +28,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
Context `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp := Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp) : iProp :=
...@@ -38,7 +36,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp := ...@@ -38,7 +36,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I. v, lv = SOMEV v (Ψ v own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val iProp) : iProp := Definition join_handle (l : loc) (Ψ : val iProp) : iProp :=
( γ, heap_ctx own γ (Excl ()) inv spawnN (spawn_inv γ l Ψ))%I. (heapN N γ, heap_ctx own γ (Excl ())
inv N (spawn_inv γ l Ψ))%I.
Typeclasses Opaque join_handle. Typeclasses Opaque join_handle.
...@@ -52,18 +51,19 @@ Proof. solve_proper. Qed. ...@@ -52,18 +51,19 @@ Proof. solve_proper. Qed.
(** The main proofs. *) (** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) : Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) :
to_val e = Some f to_val e = Some f
heapN N
heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l) heap_ctx WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. 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. wp_let. wp_alloc l as "Hl". wp_let.
iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc spawnN _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done. iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists NONEV. iFrame; eauto. } { iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf". wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto. - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv". - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv spawnN as (v') "[Hl _]". iInv N as (v') "[Hl _]".
wp_store. iPvsIntro. iSplit; [iNext|done]. wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (SOMEV v). iFrame. eauto. iExists (SOMEV v). iFrame. eauto.
Qed. Qed.
...@@ -71,8 +71,8 @@ Qed. ...@@ -71,8 +71,8 @@ Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) : Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}. join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof. Proof.
rewrite /join_handle; iIntros "[H Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)". 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]". iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|]. - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ Hv"). wp_match. iApply ("IH" with "Hγ Hv").
......
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