diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v index d923178cd18aec9e7f27e3651cef038a16579701..716bee1826eb387bcf86da475d2361dd39ddcb94 100644 --- a/theories/concurrent_stacks/concurrent_stack1.v +++ b/theories/concurrent_stacks/concurrent_stack1.v @@ -1,183 +1,171 @@ -From iris.base_logic Require Import base_logic. -From iris.proofmode Require Import tactics. From iris.base_logic.lib Require Import invariants. -From iris.program_logic Require Export weakestpre hoare. -From iris.heap_lang Require Export lang. -From iris.algebra Require Import agree list. -From iris.heap_lang Require Import assert proofmode notation. - -From iris_examples.concurrent_stacks Require Import spec. - +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Import notation proofmode. Set Default Proof Using "Type". -(** Stack 1: No helping, bag spec. *) - -Definition mk_stack : val := - λ: "_", - let: "r" := ref NONEV in - (rec: "pop" "n" := - match: !"r" with - NONE => NONE - | SOME "hd" => - if: CAS "r" (SOME "hd") (Snd !"hd") - then SOME (Fst !"hd") - else "pop" "n" - end, - rec: "push" "n" := - let: "r'" := !"r" in - let: "r''" := SOME (Alloc ("n", "r'")) in - if: CAS "r" "r'" "r''" - then #() - else "push" "n"). +Definition new_stack : val := λ: "_", ref NONEV. +Definition push : val := + rec: "push" "s" "v" := + let: "tail" := ! "s" in + let: "new" := SOME (ref ("v", "tail")) in + if: CAS "s" "tail" "new" then #() else "push" "s" "v". +Definition pop : val := + rec: "pop" "s" := + match: !"s" with + NONE => NONEV + | SOME "l" => + let: "pair" := !"l" in + if: CAS "s" (SOME "l") (Snd "pair") + then SOME (Fst "pair") + else "pop" "s" + end. Section stacks. - Context `{!heapG Σ}. + Context `{!heapG Σ} (N : namespace). Implicit Types l : loc. - Definition oloc_to_val (h : option loc) : val := - match h with - | None => NONEV - | Some l => SOMEV #l - end. - Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val. - Proof. rewrite /Inj /oloc_to_val=>??. repeat case_match; congruence. Qed. + Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I + (at level 20, format "l ↦{-} v") : bi_scope. + + Lemma partial_mapsto_duplicable l v : + l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v. + Proof. + iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto. + Qed. - Definition is_stack_pre (P : val → iProp Σ) (F : option loc -c> iProp Σ) : - option loc -c> iProp Σ := λ v, - (match v with - | None => True - | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) ∗ P h ∗ ▷ F t - end)%I. + Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) : + val -c> iProp Σ := λ v, + (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I. - Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P). + Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P). Proof. - rewrite /is_stack_pre => n f f' Hf v. + rewrite /is_list_pre => n f f' Hf v. repeat (f_contractive || f_equiv). apply Hf. Qed. - Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P). - Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed. - Definition is_stack P := unseal (is_stack_aux P). - Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P). - - Definition stack_inv P l := - (∃ ol, l ↦ oloc_to_val ol ∗ is_stack P ol)%I. + Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P). + Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed. + Definition is_list P := unseal (is_list_aux P). + Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P). + Lemma is_list_unfold (P : val → iProp Σ) v : + is_list P v ⊣⊢ is_list_pre P (is_list P) v. + Proof. + rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)). + Qed. - Lemma is_stack_unfold (P : val → iProp Σ) v : - is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v. + (* TODO: shouldn't have to explicitly return is_list *) + Lemma is_list_unboxed (P : val → iProp Σ) v : + is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v. Proof. - rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)). + iIntros "Hstack"; iSplit; last done; + iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]"; + last iDestruct "Hstack" as (l h t) "(-> & _)"; done. Qed. - Lemma is_stack_copy (P : val → iProp Σ) ol : - is_stack P ol -∗ is_stack P ol ∗ - (match ol with None => True | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) end). + Lemma is_list_disj (P : val → iProp Σ) v : + is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V). Proof. iIntros "Hstack". - iDestruct (is_stack_unfold with "Hstack") as "Hstack". destruct ol; last first. - - iSplitL; try iApply is_stack_unfold; auto. - - iDestruct "Hstack" as (q h t) "[[Hl1 Hl2] [HP Hrest]]". - iSplitR "Hl2"; try iApply is_stack_unfold; simpl; eauto 10 with iFrame. + iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq. + - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto. + - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)". + iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq. + rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame. Qed. - (* Per-element invariant (i.e., bag spec). *) - Theorem stack_works P Φ : - ▷ (∀ (f₁ f₂ : val), - (□ WP f₁ #() {{ v, (∃ v', v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) - -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) - -∗ Φ (f₁, f₂)%V)%I - -∗ WP mk_stack #() {{ Φ }}. + Definition stack_inv P v := + (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_list P v')%I. + + Definition is_stack (P : val → iProp Σ) v := + inv N (stack_inv P v). + + Theorem mk_stack_spec P : + WP new_stack #() {{ s, is_stack P s }}%I. Proof. - iIntros "HΦ". + iApply wp_fupd. wp_lam. - wp_alloc l as "Hl". - pose proof (nroot .@ "N") as N. - rewrite -wp_fupd. - iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack". - { iExists None; iFrame; auto. - iApply is_stack_unfold. auto. } - wp_pures. + wp_alloc ℓ as "Hl". + iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv". + { iNext; iExists ℓ, NONEV; iFrame; + by iSplit; last (iApply is_list_unfold; iLeft). } + done. + Qed. + + Theorem push_spec P s v : + {{{ is_stack P s ∗ P v }}} push s v {{{ RET #(); True }}}. + Proof. + iIntros (Φ) "[#Hstack HP] HΦ". + iLöb as "IH". + wp_lam. wp_lam. wp_bind (Load _). + iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst. + wp_load. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _, _; by iFrame. } + iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_let. wp_bind (CAS _ _ _). + iInv N as (ℓ'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq. + destruct (decide (v' = v'')) as [ -> |]. + - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + wp_cas_suc. + iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_". + { iNext; iExists _, (InjRV #ℓ'); iFrame; iSplit; first done; + rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. } + iModIntro. + wp_if. + by iApply "HΦ". + - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + wp_cas_fail. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _, _; by iFrame. } + iModIntro. + wp_if. + iApply ("IH" with "HP HΦ"). + Qed. + + Theorem pop_works P s : + {{{ is_stack P s }}} pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}. + Proof. + iIntros (Φ) "#Hstack HΦ". + iLöb as "IH". + wp_lam. wp_bind (Load _). + iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst. + wp_load. + iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]". + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _, _; by iFrame. } iModIntro. - iApply "HΦ". - - iIntros "!#". - iLöb as "IH". - wp_rec. - wp_bind (! #l)%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (v') "[Hl' Hstack]". + iDestruct "Hdisj" as "[-> | Heq]". + - wp_match. + iApply "HΦ"; by iLeft. + - iDestruct "Heq" as (l h t) "[-> Hl]". + wp_match. wp_bind (Load _). + iInv N as (ℓ' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq. + iDestruct "Hl" as (q) "Hl". wp_load. - destruct v' as [l'|]; simpl; last first. - + iMod ("Hclose" with "[Hl' Hstack]") as "_". - { rewrite /stack_inv. eauto with iFrame. } - iModIntro. wp_match. wp_pures. by iRight. - + iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]". - iDestruct "Hmy" as (q h t) "Hl". - iMod ("Hclose" with "[Hl' Hstack]") as "_". - { rewrite /stack_inv. eauto with iFrame. } - iModIntro. wp_match. - wp_load. wp_pures. - wp_bind (CAS _ _ _). - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (v'') "[Hl'' Hstack]". - destruct (decide (oloc_to_val v'' = oloc_to_val (Some l'))) as [->%oloc_to_val_inj|Hne]. - * simpl. wp_cas_suc. - iDestruct (is_stack_unfold with "Hstack") as "Hstack". - iDestruct "Hstack" as (q' h' t') "[Hl' [HP Hstack]]". - iDestruct (mapsto_agree with "Hl Hl'") as %[= <- <-%oloc_to_val_inj]. - iMod ("Hclose" with "[Hl'' Hstack]"). - { iExists _. auto with iFrame. } - iModIntro. - wp_if. - wp_load. - wp_pures. - eauto. - * simpl in Hne. wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack]"). - { iExists v''; iFrame; auto. } - iModIntro. - wp_if. - iApply "IH". - - iIntros (v) "!# HP". - iLöb as "IH". - wp_rec. - wp_bind (! _)%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (v') "[Hl' Hstack]". - wp_load. - iMod ("Hclose" with "[Hl' Hstack]"). - { iExists v'. iFrame. } + iMod ("Hclose" with "[Hl' Hlist]") as "_". + { iNext; iExists _, _; by iFrame. } iModIntro. - wp_let. - wp_alloc r'' as "Hr''". - wp_pures. wp_bind (CAS _ _ _). - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (v'') "[Hl'' Hstack]". - wp_cas as ->%oloc_to_val_inj|_. - + destruct v'; by right. - + iMod ("Hclose" with "[Hl'' Hr'' HP Hstack]"). - iExists (Some r''). - iFrame; auto. - iNext. - iApply is_stack_unfold. - simpl. - iExists _, _, v'. iFrame. + wp_let. wp_proj. wp_bind (CAS _ _ _). + iInv N as (ℓ'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq. + destruct (decide (v'' = InjRV #l)) as [-> |]. + * rewrite is_list_unfold. + iDestruct "Hlist" as "[>% | H]"; first done. + iDestruct "H" as (ℓ''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq. + iDestruct "Hl''" as (q') "Hl''". + wp_cas_suc. + iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq. + iMod ("Hclose" with "[Hl' Hlist]") as "_". + { iNext; iExists ℓ'', _; by iFrame. } iModIntro. wp_if. - done. - + iMod ("Hclose" with "[Hl'' Hstack]"). - iExists v''; iFrame; auto. + wp_proj. + iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame. + * wp_cas_fail. + iMod ("Hclose" with "[Hl' Hlist]") as "_". + { iNext; iExists ℓ'', _; by iFrame. } iModIntro. wp_if. - iApply "IH". - done. + iApply ("IH" with "HΦ"). Qed. End stacks. - -Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ := - {| spec.mk_bag := mk_stack |}. -Next Obligation. - iIntros (??? P Φ) "_ HΦ". iApply stack_works. - iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. -Qed. diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v index d7023b9bfe2708be884f2f1afa8a733d61b20175..0fb9abae7b025b90ff46846b2648af87a54aef69 100644 --- a/theories/concurrent_stacks/concurrent_stack2.v +++ b/theories/concurrent_stacks/concurrent_stack2.v @@ -1,15 +1,9 @@ -(** THIS FILE CURRENTLY DOES NOT COMPILE because it has not been ported to the -stricter CAS requirements yet. *) -From iris.program_logic Require Export weakestpre hoare. -From iris.heap_lang Require Export lang proofmode notation. +From iris.heap_lang Require Import notation proofmode. From iris.algebra Require Import excl. - -From iris_examples.concurrent_stacks Require Import spec. - +From iris.base_logic.lib Require Import invariants. +From iris.program_logic Require Export weakestpre. Set Default Proof Using "Type". -(** Stack 2: With helping, bag spec. *) - Definition mk_offer : val := λ: "v", ("v", ref #0). Definition revoke_offer : val := @@ -17,49 +11,49 @@ Definition revoke_offer : val := Definition take_offer : val := λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE. -Definition mailbox : val := - λ: "_", - let: "r" := ref NONEV in - (rec: "put" "v" := - let: "off" := mk_offer "v" in - "r" <- SOME "off";; - revoke_offer "off", - rec: "get" "n" := - let: "offopt" := !"r" in - match: "offopt" with - NONE => NONE - | SOME "x" => take_offer "x" - end - ). - -Definition mk_stack : val := - λ: "_", - let: "mailbox" := mailbox #() in - let: "put" := Fst "mailbox" in - let: "get" := Snd "mailbox" in - let: "r" := ref NONEV in - (rec: "pop" "n" := - match: "get" #() with - NONE => - (match: !"r" with - NONE => NONE - | SOME "hd" => - if: CAS "r" (SOME "hd") (Snd "hd") - then SOME (Fst "hd") - else "pop" "n" - end) - | SOME "x" => SOME "x" - end, - rec: "push" "n" := - match: "put" "n" with - NONE => #() - | SOME "n" => - let: "r'" := !"r" in - let: "r''" := SOME ("n", "r'") in - if: CAS "r" "r'" "r''" - then #() - else "push" "n" - end). +Definition mk_mailbox : val := λ: "_", ref NONEV. +Definition put : val := + λ: "r" "v", + let: "off" := mk_offer "v" in + "r" <- SOME "off";; + revoke_offer "off". + +Definition get : val := + λ: "r", + let: "offopt" := !"r" in + match: "offopt" with + NONE => NONE + | SOME "x" => take_offer "x" + end. + +Definition mk_stack : val := λ: "_", (mk_mailbox #(), ref NONEV). +Definition push : val := + rec: "push" "p" "v" := + let: "mailbox" := Fst "p" in + let: "s" := Snd "p" in + match: put "mailbox" "v" with + NONE => #() + | SOME "v'" => + let: "tail" := ! "s" in + let: "new" := SOME (ref ("v'", "tail")) in + if: CAS "s" "tail" "new" then #() else "push" "p" "v'" + end. +Definition pop : val := + rec: "pop" "p" := + let: "mailbox" := Fst "p" in + let: "s" := Snd "p" in + match: get "mailbox" with + NONE => + match: !"s" with + NONE => NONEV + | SOME "l" => + let: "pair" := !"l" in + if: CAS "s" (SOME "l") (Snd "pair") + then SOME (Fst "pair") + else "pop" "p" + end + | SOME "x" => SOME "x" + end. Definition channelR := exclR unitR. Class channelG Σ := { channel_inG :> inG Σ channelR }. @@ -68,350 +62,333 @@ Instance subG_channelΣ {Σ} : subG channelΣ Σ → channelG Σ. Proof. solve_inG. Qed. Section side_channel. - Context `{!heapG Σ, !channelG Σ}. + Context `{!heapG Σ, !channelG Σ} (N : namespace). Implicit Types l : loc. + Definition revoke_tok γ := own γ (Excl ()). + Definition stages γ (P : val → iProp Σ) l v := ((l ↦ #0 ∗ P v) ∨ (l ↦ #1) - ∨ (l ↦ #2 ∗ own γ (Excl ())))%I. + ∨ (l ↦ #2 ∗ revoke_tok γ))%I. Definition is_offer γ (P : val → iProp Σ) (v : val) : iProp Σ := - (∃ v' l, ⌜v = (v', #l)%V⌝ ∗ ∃ ι, inv ι (stages γ P l v'))%I. + (∃ v' l, ⌜v = (v', #l)%V⌝ ∗ inv N (stages γ P l v'))%I. - Definition mailbox_inv (P : val → iProp Σ) (v : val) : iProp Σ := - (∃ l, ⌜v = #l⌝ ∗ (l ↦ NONEV ∨ (∃ v' γ, l ↦ SOMEV v' ∗ is_offer γ P v')))%I. + Lemma mk_offer_works P v : + {{{ P v }}} mk_offer v {{{ o γ, RET o; is_offer γ P o ∗ revoke_tok γ }}}. + Proof. + iIntros (Φ) "HP HΦ". + rewrite -wp_fupd. + wp_lam. wp_alloc l as "Hl". + iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. + iMod (inv_alloc N _ (stages γ P l v) with "[Hl HP]") as "#Hinv". + { iNext; iLeft; iFrame. } + iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto. + Qed. (* A partial specification for revoke that will be useful later *) - Lemma revoke_works N γ P l v : - inv N (stages γ P l v) ∗ own γ (Excl ()) -∗ - WP revoke_offer (v, #l) - {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}. + Lemma revoke_works γ P v : + {{{ is_offer γ P v ∗ revoke_tok γ }}} + revoke_offer v + {{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}}. Proof. - iIntros "[#Hinv Hγ]". - wp_let. - wp_proj. - wp_bind (CAS _ _ _). + iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]". + wp_let. wp_proj. wp_bind (CAS _ _ _). iInv N as "Hstages" "Hclose". - iDestruct "Hstages" as "[H | [H | H]]". - - iDestruct "H" as "[Hl HP]". - wp_cas_suc. - iMod ("Hclose" with "[Hl Hγ]"). - iRight; iRight; iFrame. + iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]". + - wp_cas_suc. + iMod ("Hclose" with "[Hl Hγ]") as "_". + { iRight; iRight; iFrame. } iModIntro. - wp_if. - wp_proj. - iLeft. - iExists v; iSplit; auto. + wp_if. wp_proj. + by iApply "HΦ"; iLeft; iExists _; iSplit. - wp_cas_fail. - iMod ("Hclose" with "[H]"). - iRight; iLeft; auto. + iMod ("Hclose" with "[H]") as "_". + { iRight; iLeft; auto. } iModIntro. wp_if. - iRight; auto. - - iDestruct "H" as "[Hl H]". - wp_cas_fail. - by iDestruct (own_valid_2 with "H Hγ") as %?. + by iApply "HΦ"; iRight. + - wp_cas_fail. + iDestruct (own_valid_2 with "H Hγ") as %[]. Qed. (* A partial specification for take that will be useful later *) - Lemma take_works γ N P v l : - inv N (stages γ P l v) -∗ - WP take_offer (v, LitV l)%V - {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}. + Lemma take_works γ P o : + {{{ is_offer γ P o }}} + take_offer o + {{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}}. Proof. - iIntros "#Hinv". - wp_lam. - wp_proj. - wp_bind (CAS _ _ _). + iIntros (Φ) "H HΦ"; iDestruct "H" as (v l) "[-> #Hinv]". + wp_lam. wp_proj. wp_bind (CAS _ _ _). iInv N as "Hstages" "Hclose". - iDestruct "Hstages" as "[H | [H | H]]". - - iDestruct "H" as "[H HP]". - wp_cas_suc. - iMod ("Hclose" with "[H]"). - iRight; iLeft; done. + iDestruct "Hstages" as "[[H HP] | [H | [Hl Hγ]]]". + - wp_cas_suc. + iMod ("Hclose" with "[H]") as "_". + { by iRight; iLeft. } iModIntro. - wp_if. - wp_proj. - iLeft. - auto. + wp_if. wp_proj. + iApply "HΦ"; iLeft; auto. - wp_cas_fail. - iMod ("Hclose" with "[H]"). - iRight; iLeft; done. + iMod ("Hclose" with "[H]") as "_". + { by iRight; iLeft. } iModIntro. wp_if. - auto. - - iDestruct "H" as "[Hl Hγ]". - wp_cas_fail. + iApply "HΦ"; auto. + - wp_cas_fail. iMod ("Hclose" with "[Hl Hγ]"). - iRight; iRight; iFrame. + { iRight; iRight; iFrame. } iModIntro. wp_if. - auto. + iApply "HΦ"; auto. Qed. End side_channel. Section mailbox. - Context `{!heapG Σ}. + Context `{!heapG Σ, channelG Σ} (N : namespace). Implicit Types l : loc. - Theorem mailbox_works {channelG0 : channelG Σ} (P : val → iProp Σ) (Φ : val → iProp Σ) : - (∀ (v₁ v₂ : val), - ⌜Closed [] v₁⌝ - ∗ ⌜Closed [] v₂⌝ - ∗ (∀ (v : val), □ (P v -∗ WP v₁ v {{v', - (∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝}})) - ∗ (□ (WP v₂ #() {{v', (∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝}})) - -∗ Φ (v₁, v₂)%V) - -∗ WP mailbox #() {{ Φ }}. + Definition Noffer := N .@ "offer". + + Definition mailbox_inv (P : val → iProp Σ) (l : loc) : iProp Σ := + (l ↦ NONEV ∨ (∃ v' γ, l ↦ SOMEV v' ∗ is_offer Noffer γ P v'))%I. + + Definition is_mailbox (P : val → iProp Σ) (v : val) : iProp Σ := + (∃ l, ⌜v = #l⌝ ∗ inv N (mailbox_inv P l))%I. + + Theorem mk_mailbox_works (P : val → iProp Σ) : + {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}. Proof. - iIntros "HΦ". - pose proof (nroot .@ "N") as N. + iIntros (Φ) "_ HΦ". rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl". - wp_let. - iMod (inv_alloc N _ (mailbox_inv P #l) with "[Hl]") as "#Hinv". - iExists l; iSplit; try iLeft; auto. + iMod (inv_alloc N _ (mailbox_inv P l) with "[Hl]") as "#Hinv". + { by iNext; iLeft. } iModIntro. - iApply "HΦ"; repeat iSplit; try (iPureIntro; apply _). - * iIntros (v) "!# HP". - wp_rec. - wp_bind (mk_offer v). - pose proof (nroot .@ "N'") as N'. - rewrite -wp_fupd. - wp_lam. - iMod (own_alloc (Excl ())) as (γ) "Hγ". done. - wp_alloc l' as "Hl'". - iMod (inv_alloc N' _ (stages γ P l' v) with "[HP Hl']") as "#Hinv'". - iLeft; iFrame. + iApply "HΦ"; iExists _; eauto. + Qed. + + Theorem get_works (P : val → iProp Σ) mailbox : + {{{ is_mailbox P mailbox }}} + get mailbox + {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v}}}. + Proof. + iIntros (Φ) "H HΦ". iDestruct "H" as (l) "[-> #Hinv]". + wp_lam. wp_bind (Load _). + iInv N as "[Hnone | Hsome]" "Hclose". + - wp_load. + iMod ("Hclose" with "[Hnone]") as "_". + { by iNext; iLeft. } + iModIntro. + wp_let. wp_match. + iApply "HΦ"; auto. + - iDestruct "Hsome" as (v' γ) "[Hl #Hoffer]". + wp_load. + iMod ("Hclose" with "[Hl]") as "_". + { by iNext; iRight; iExists _, _; iFrame. } + iModIntro. + wp_let. wp_match. + iApply (take_works with "Hoffer"). + iNext; iIntros (offer) "[Hsome | Hnone]". + * iDestruct "Hsome" as (v'') "[-> HP]". + iApply ("HΦ" with "[HP]"); iRight; auto. + * iApply "HΦ"; iLeft; auto. + Qed. + + Theorem put_works (P : val → iProp Σ) (mailbox v : val) : + {{{ is_mailbox P mailbox ∗ P v }}} + put mailbox v + {{{ o, RET o; (∃ v', ⌜o = SOMEV v'⌝ ∗ P v') ∨ ⌜o = NONEV⌝ }}}. + Proof. + iIntros (Φ) "[Hmailbox HP] HΦ"; iDestruct "Hmailbox" as (l) "[-> #Hmailbox]". + wp_lam. wp_let. wp_apply (mk_offer_works with "HP"). + iIntros (offer γ) "[#Hoffer Hrevoke]". + wp_let. wp_bind (Store _ _). + iInv N as "[HNone | HSome]" "Hclose". + - wp_store. + iMod ("Hclose" with "[HNone]") as "_". + { by iNext; iRight; iExists _, _; iFrame. } iModIntro. wp_let. - wp_bind (#l <- _)%E. - iInv N as "Hmailbox" "Hclose". - iDestruct "Hmailbox" as (l'') "[>% H]". - injection H; intros; subst. - iDestruct "H" as "[H | H]"; - [idtac | iDestruct "H" as (v' γ') "[Hl H]"]; - wp_store; - [iMod ("Hclose" with "[H]") | iMod ("Hclose" with "[Hl H]")]; - try (iExists l''; iSplit; try iRight; auto; - iExists (v, #l')%V, γ; iFrame; - iExists v, l'; auto); - iModIntro; - wp_let; - iApply (revoke_works with "[Hγ Hinv]"); auto. - * iIntros "!#". - wp_rec. - wp_bind (! _)%E. - iInv N as "Hmailbox" "Hclose". - iDestruct "Hmailbox" as (l') "[>% H]". - injection H; intros; subst. - iDestruct "H" as "[H | H]". - + wp_load. - iMod ("Hclose" with "[H]"). - iExists l'; iSplit; auto. - iModIntro. - wp_let. - wp_match. - iRight; auto. - + iDestruct "H" as (v' γ) "[Hl' #Hoffer]". - wp_load. - iMod ("Hclose" with "[Hl' Hoffer]"). - { iExists l'; iSplit; auto. - iRight; iExists v', γ; by iSplit. } - iModIntro. - wp_let. - wp_match. - iDestruct "Hoffer" as (v'' l'') "[% Hoffer]". - iDestruct "Hoffer" as (ι) "Hinv'". - subst. - iApply take_works; auto. + wp_apply (revoke_works with "[Hrevoke]"); first by iFrame. + iIntros (v') "H"; iDestruct "H" as "[HSome | HNone]". + * iApply ("HΦ" with "[HSome]"); by iLeft. + * iApply ("HΦ" with "[HNone]"); by iRight. + - iDestruct "HSome" as (v' γ') "[Hl #Hoffer']". + wp_store. + iMod ("Hclose" with "[Hl]") as "_". + { by iNext; iRight; iExists _, _; iFrame. } + iModIntro. + wp_let. + wp_apply (revoke_works with "[Hrevoke]"); first by iFrame. + iIntros (v'') "H"; iDestruct "H" as "[HSome | HNone]". + * iApply ("HΦ" with "[HSome]"); by iLeft. + * iApply ("HΦ" with "[HNone]"); by iRight. Qed. End mailbox. Section stack_works. - Context `{!heapG Σ}. + Context `{!heapG Σ, channelG Σ} (N : namespace). Implicit Types l : loc. - Definition is_stack_pre (P : val → iProp Σ) (F : val -c> iProp Σ) : + Definition Nmailbox := N .@ "mailbox". + + Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I + (at level 20, format "l ↦{-} v") : bi_scope. + + Lemma partial_mapsto_duplicable l v : + l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v. + Proof. + iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto. + Qed. + + Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) : val -c> iProp Σ := λ v, - (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V ∗ P h ∗ ▷ F t)%I. + (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I. - Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P). + Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P). Proof. - rewrite /is_stack_pre => n f f' Hf v. + rewrite /is_list_pre => n f f' Hf v. repeat (f_contractive || f_equiv). apply Hf. Qed. - Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P). - Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed. - Definition is_stack P := unseal (is_stack_aux P). - Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P). + Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P). + Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed. + Definition is_list P := unseal (is_list_aux P). + Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P). - Definition stack_inv P v := - (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack P v')%I. + Lemma is_list_unfold (P : val → iProp Σ) v : + is_list P v ⊣⊢ is_list_pre P (is_list P) v. + Proof. + rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)). + Qed. - Lemma is_stack_unfold (P : val → iProp Σ) v : - is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v. + (* TODO: shouldn't have to explicitly return is_list *) + Lemma is_list_unboxed (P : val → iProp Σ) v : + is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v. Proof. - rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)). + iIntros "Hstack"; iSplit; last done; + iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]"; + last iDestruct "Hstack" as (l h t) "(-> & _)"; done. Qed. - Lemma is_stack_disj (P : val → iProp Σ) v : - is_stack P v -∗ is_stack P v ∗ (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V). + Lemma is_list_disj (P : val → iProp Σ) v : + is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V). Proof. iIntros "Hstack". - iDestruct (is_stack_unfold with "Hstack") as "[#Hstack|Hstack]". - - iSplit; try iApply is_stack_unfold; iLeft; auto. - - iDestruct "Hstack" as (h t) "[#Heq rest]". - iSplitL; try iApply is_stack_unfold; iRight; auto. + iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq. + - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto. + - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)". + iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq. + rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame. Qed. - (* Per-element invariant (i.e., bag spec). *) - Theorem stack_works {channelG0 : channelG Σ} P Φ : - ▷ (∀ (f₁ f₂ : val), - (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) - -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) - -∗ Φ (f₁, f₂)%V)%I - -∗ WP mk_stack #() {{ Φ }}. + Definition stack_inv P l := (∃ v, l ↦ v ∗ is_list P v)%I. + Definition is_stack P v := + (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox Nmailbox P mailbox ∗ inv N (stack_inv P l))%I. + + Theorem mk_stack_works P : + WP mk_stack #() {{ v, is_stack P v }}%I. Proof. - iIntros "HΦ". + rewrite -wp_fupd. wp_lam. - wp_bind (mailbox _). - iApply (mailbox_works P). - iIntros (put get) "[% [% [#Hput #Hget]]]". - wp_let; wp_proj; wp_let; wp_proj; wp_let; wp_alloc l' as "Hl'". - pose proof (nroot .@ "N") as N. - iMod (inv_alloc N _ (stack_inv P #l') with "[Hl']") as "#Hisstack". - { iExists l', NONEV; iFrame; iSplit; auto. iApply is_stack_unfold; iLeft; done. } - wp_let. - iApply "HΦ". - (* The verification of pop *) - - iIntros "!#". - iLöb as "IH". - wp_rec; wp_bind (get _). - (* Switch from proving WP put #() {{ P }} to - * Q -∗ P where Q is the spec we have already assumed for P - *) - iApply wp_wand; auto. - iIntros (v) "Hv". - iDestruct "Hv" as "[H | H]". - * iDestruct "H" as (v') "[% HP]". - subst. - (* This is just some technical fidgetting to get wp_match to behave. - * It is safe to ignore - *) - assert (to_val v' = Some v') by apply to_of_val. - assert (is_Some (to_val v')) by (exists v'; auto). - assert (to_val (InjRV v') = Some (InjRV v')) by apply to_of_val. - assert (is_Some (to_val (InjRV v'))) by (exists (InjRV v'); auto). - wp_match. - iLeft; iExists v'; auto. - * iDestruct "H" as "%"; subst. - wp_match; wp_bind (! #l')%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v'') "[>% [Hl' Hstack]]". - injection H1; intros; subst. - wp_load. - iDestruct (is_stack_disj with "Hstack") as "[Hstack #Heq]". - iMod ("Hclose" with "[Hl' Hstack]"). - { iExists l'', v''; iFrame; auto. } + wp_apply mk_mailbox_works; first done. + iIntros (mailbox) "#Hmailbox". + wp_alloc l as "Hl". + iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv". + { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. } + iModIntro. + iExists _, _; auto. + Qed. + + Theorem push_works P s v : + {{{ is_stack P s ∗ P v }}} push s v {{{ RET #(); True }}}. + Proof. + iIntros (Φ) "[Hstack HP] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)". + iLöb as "IH" forall (v). + wp_lam. wp_let. wp_proj. wp_let. wp_proj. wp_let. + wp_apply (put_works _ P with "[HP]"); first by iFrame. + iIntros (result) "Hopt". + iDestruct "Hopt" as "[HSome | ->]". + - iDestruct "HSome" as (v') "[-> HP]". + wp_match. wp_bind (Load _). + iInv N as (v'') "[Hl Hlist]" "Hclose". + wp_load. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; iFrame. } + iModIntro. + wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _). + iInv N as (list) "(Hl & Hlist)" "Hclose". + destruct (decide (v'' = list)) as [ -> |]. + * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + wp_cas_suc. + iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_". + { iNext; iExists (SOMEV _); iFrame. + rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. } + iModIntro. + wp_if. + by iApply "HΦ". + * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + wp_cas_fail. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; by iFrame. } iModIntro. - iDestruct "Heq" as "[H | H]". - + iRewrite "H"; wp_match; iRight; auto. - + iDestruct "H" as (h t) "H"; iRewrite "H". - (* For technical reasons, wp_match gets confused by this - * position. Hence the assertions. They can be safely ignored - *) - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. fold of_val. - (* Now back to our regularly scheduled verification *) - wp_bind (CAS _ _ _); wp_proj. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l''' v''') "[>% [Hl'' Hstack]]". - injection H4; intros; subst. - (* Case on whether or not the stack has been updated *) - destruct (decide (v''' = InjRV (h, t)%V)). - ++ (* If nothing has changed, the cas succeeds *) - wp_cas_suc. - iDestruct (is_stack_unfold with "Hstack") as "[Hstack | Hstack]". - subst. - iDestruct "Hstack" as "%"; discriminate. - iDestruct "Hstack" as (h' t') "[% [HP Hstack]]". - subst. - injection H5. - intros. - subst. - iMod ("Hclose" with "[Hl'' Hstack]"). - { iExists l''', t'; iFrame; auto. } - iModIntro. - wp_if; wp_proj; iLeft; auto. - ++ (* The case in which we fail *) - wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack]"). - iExists l''', v'''; iFrame; auto. - iModIntro. - wp_if. - (* Now we use our IH to loop *) - iApply "IH". - (* The verification of push. This is actually markedly simpler. *) - - iIntros (v) "!# HP". - simpl in *. - fold of_val in *. - (* We grab an IH to be used in the case that we loop *) - iLöb as "IH" forall (v). - wp_rec. - wp_bind (put _). - (* Switch from proving WP put #() {{ P }} to - * Q -∗ P where Q is the spec we have already assumed for put - *) - iApply (wp_wand with "[HP]"). - iApply "Hput"; auto. - iIntros (v') "Hv'". - iDestruct "Hv'" as "[H | H]". - * iDestruct "H" as (v'') "[% HP]"; subst. - wp_match. - (* Push the substitution through the term *) - wp_bind (! _)%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v') "[>% [Hl' Hstack]]"; simplify_eq. + wp_if. + iApply ("IH" with "HP HΦ"). + - wp_match. + by iApply "HΦ". + Qed. + + Theorem pop_works P s : + {{{ is_stack P s }}} pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}. + Proof. + iIntros (Φ) "Hstack HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hstack)". + iLöb as "IH". + wp_lam. wp_proj. wp_let. wp_proj. wp_lam. + wp_apply get_works; first done. + iIntros (ov) "[-> | HSome]". + - wp_match. wp_bind (Load _). + iInv N as (list) "[Hl Hlist]" "Hclose". + wp_load. + iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]". + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; by iFrame. } + iModIntro. + iDestruct "Hdisj" as "[-> | Heq]". + * wp_match. + iApply "HΦ"; by iLeft. + * iDestruct "Heq" as (l' h t) "[-> Hl']". + wp_match. wp_bind (Load _). + iInv N as (v') "[>Hl Hlist]" "Hclose". + iDestruct "Hl'" as (q) "Hl'". wp_load. - iMod ("Hclose" with "[Hl' Hstack]"). - { by (iExists l'', v'; iFrame). } + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; by iFrame. } iModIntro. - wp_let; wp_let; wp_bind (CAS _ _ _). - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l''' v''') "[>% [Hl'' Hstack]]"; simplify_eq. - (* Now we case to see if the stack is unchanged *) - destruct (decide (v''' = v'%V)). - + wp_cas_suc. - iMod ("Hclose" with "[Hl'' HP Hstack]"). - { iExists l''', (InjRV (v'', v')%V). - iSplit; iFrame; auto. - iApply is_stack_unfold; iRight. - iExists v'', v'; iFrame; iSplit; subst; auto. } + wp_let. wp_proj. wp_bind (CAS _ _ _). + iInv N as (v'') "[Hl Hlist]" "Hclose". + destruct (decide (v'' = InjRV #l')) as [-> |]. + + rewrite is_list_unfold. + iDestruct "Hlist" as "[>% | H]"; first done. + iDestruct "H" as (l'' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq. + iDestruct "Hl''" as (q') "Hl''". + wp_cas_suc. + iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; by iFrame. } iModIntro. - wp_if. - done. + wp_if. wp_proj. + iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame. + wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack]"). - iExists l''', v'''; iFrame; auto. + iMod ("Hclose" with "[Hl Hlist]") as "_". + { iNext; iExists _; by iFrame. } iModIntro. wp_if. - iApply ("IH" with "HP"). - * (* This is the case that our sidechannel offer succeeded *) - iDestruct "H" as "%"; subst. - wp_match. - done. + iApply ("IH" with "HΦ"). + - iDestruct "HSome" as (v) "[-> HP]". + wp_match. + iApply "HΦ"; iRight; iExists _; auto. Qed. End stack_works. - -Program Definition is_concurrent_bag `{!heapG Σ, !channelG Σ} : concurrent_bag Σ := - {| spec.mk_bag := mk_stack |}. -Next Obligation. - iIntros (???? P Φ) "_ HΦ". iApply stack_works. - iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. -Qed. diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v index f2dba8bb7c89b8fc73b070b454cd54a4a66406da..3cdb5e32d67b6741eb78fd3d159719d541bd3edc 100644 --- a/theories/concurrent_stacks/concurrent_stack3.v +++ b/theories/concurrent_stacks/concurrent_stack3.v @@ -1,223 +1,189 @@ From iris.program_logic Require Export weakestpre hoare. From iris.heap_lang Require Export lang proofmode notation. -From iris.algebra Require Import excl. - -From iris_examples.concurrent_stacks Require Import spec. - Set Default Proof Using "Type". -(** Stack 3: No helping, view-shift spec. *) - -Definition mk_stack : val := - λ: "_", - let: "r" := ref NONEV in - (rec: "pop" "n" := - (match: !"r" with - NONE => NONE - | SOME "hd" => - if: CAS "r" (SOME "hd") (Snd !"hd") - then SOME (Fst !"hd") - else "pop" "n" - end), - rec: "push" "n" := - let: "r'" := !"r" in - let: "r''" := SOME (Alloc ("n", "r'")) in - if: CAS "r" "r'" "r''" - then #() - else "push" "n"). +Definition mk_stack : val := λ: "_", ref NONEV. +Definition push : val := + rec: "push" "s" "v" := + let: "tail" := ! "s" in + let: "new" := SOME (ref ("v", "tail")) in + if: CAS "s" "tail" "new" then #() else "push" "s" "v". +Definition pop : val := + rec: "pop" "s" := + match: !"s" with + NONE => NONEV + | SOME "l" => + let: "pair" := !"l" in + if: CAS "s" (SOME "l") (Snd "pair") + then SOME (Fst "pair") + else "pop" "s" + end. Section stack_works. - Context `{!heapG Σ}. + Context `{!heapG Σ} (N : namespace). Implicit Types l : loc. - Fixpoint is_stack xs v : iProp Σ := + Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I + (at level 20, format "l ↦{-} v") : bi_scope. + + Lemma partial_mapsto_duplicable l v : + l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v. + Proof. + iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto. + Qed. + + Lemma partial_mapsto_agree l v1 v2 : + l ↦{-} v1 -∗ l ↦{-} v2 -∗ ⌜v1 = v2⌝. + Proof. + iIntros "H1 H2". + iDestruct "H1" as (?) "H1". + iDestruct "H2" as (?) "H2". + iApply (mapsto_agree with "H1 H2"). + Qed. + + Fixpoint is_list xs v : iProp Σ := (match xs with | [] => ⌜v = NONEV⌝ - | x :: xs => ∃ q (l : loc) (t : val), ⌜v = SOMEV #l ⌝ ∗ l ↦{q} (x, t) ∗ is_stack xs t + | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t end)%I. - Definition stack_inv P v := - (∃ l v' xs, ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack xs v' ∗ P xs)%I. - - Lemma is_stack_disj xs v : - is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ q (l : loc) (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{q} (h, t)). + Lemma is_list_disj xs v : + is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V). Proof. - iIntros "Hstack". - destruct xs. - - iSplit; try iLeft; auto. - - simpl. iDestruct "Hstack" as (q l t) "[-> [[Hl Hl'] Hstack]]". - iSplitR "Hl"; eauto 10 with iFrame. + destruct xs; auto. + iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)". + iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]". + iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto. Qed. - Lemma is_stack_unboxed xs v : - is_stack xs v -∗ ⌜val_is_unboxed v⌝. + + Lemma is_list_unboxed xs v : + is_list xs v -∗ ⌜val_is_unboxed v⌝ ∗ is_list xs v. Proof. - iIntros "Hstack". iDestruct (is_stack_disj with "Hstack") as "[_ [->|Hdisj]]". - - done. - - iDestruct "Hdisj" as (???? ->) "_". done. + iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]". + iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]". Qed. - Lemma is_stack_uniq : ∀ xs ys v, - is_stack xs v ∗ is_stack ys v -∗ ⌜xs = ys⌝. + Lemma is_list_empty xs : + is_list xs (InjLV #()) -∗ ⌜xs = []⌝. Proof. - induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto. - - iDestruct "Hstack1" as "%". - iDestruct "Hstack2" as (???) "[% _]". - subst. - discriminate. - - iDestruct "Hstack2" as "%". - iDestruct "Hstack1" as (???) "[% _]". - subst. - discriminate. - - simpl. iDestruct "Hstack1" as (q1 l1 t) "[% [Hl1 Hstack1]]". - iDestruct "Hstack2" as (q2 l2 t') "[% [Hl2 Hstack2]]". - subst; injection H0; intros; subst; clear H0. - iDestruct (mapsto_agree with "Hl1 Hl2") as %[= -> ->]. - iDestruct (IHxs with "[Hstack1 Hstack2]") as "%". by iFrame. - subst; auto. + destruct xs; iIntros "Hstack"; auto. + iDestruct "Hstack" as (? ?) "(% & H)"; discriminate. Qed. - Lemma is_stack_empty : ∀ xs, - is_stack xs NONEV -∗ ⌜xs = []⌝. + Lemma is_list_cons xs l h t : + l ↦{-} (h, t)%V -∗ + is_list xs (InjRV #l) -∗ + ∃ ys, ⌜xs = h :: ys⌝. Proof. - iIntros (xs) "Hstack". - destruct xs; auto. - iDestruct "Hstack" as (?? t) "[% rest]". - discriminate. + destruct xs; first by iIntros "? %". + iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq. + iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto. Qed. - Lemma is_stack_cons : ∀ xs l, - is_stack xs (SOMEV #l) -∗ - is_stack xs (SOMEV #l) ∗ ∃ q h t ys, ⌜xs = h :: ys⌝ ∗ l ↦{q} (h, t). + + Definition stack_inv P l := + (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I. + + Definition is_stack P v := + (∃ l, ⌜v = #l⌝ ∗ inv N (stack_inv P l))%I. + + Theorem mk_stack_works P : + {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack P v }}}. Proof. - iIntros ([|x xs] l) "Hstack". - - iDestruct "Hstack" as "%"; discriminate. - - simpl. iDestruct "Hstack" as (q l' t') "[% [[Hl Hl'] Hstack]]". - injection H; intros; subst; clear H. - iSplitR "Hl'"; eauto 10 with iFrame. + iIntros (Φ) "HP HΦ". + rewrite -wp_fupd. + wp_let. wp_alloc l as "Hl". + iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv". + { by iNext; iExists _, []; iFrame. } + iModIntro; iApply "HΦ"; iExists _; auto. Qed. - (* Whole-stack invariant (P). However: - - The resources for the successful and failing pop must be disjoint. - Instead, there should be a normal conjunction between them. - Open question: How does this relate to a logically atomic spec? *) - Theorem stack_works ι P Q Q' Q'' (Φ : val → iProp Σ) : - ▷ (∀ (f₁ f₂ : val), - (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) ∧ (* pop *) - (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗ - WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) - -∗ (∀ (v : val), (* push *) - □ ((∀ vs, P vs ={⊤∖↑ι}=∗ P (v :: vs) ∗ Q'') -∗ - WP f₂ v {{ v, Q'' }})) - -∗ Φ (f₁, f₂)%V)%I - -∗ P [] - -∗ WP mk_stack #() {{ Φ }}. + Theorem push_works P s v Ψ : + {{{ is_stack P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}} + push s v + {{{ RET #(); Ψ #() }}}. Proof. - iIntros "HΦ HP". - rename ι into N. - wp_rec. - wp_alloc l as "Hl". - iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack". - { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. } - wp_pures. - iApply "HΦ". - - iIntros "!# Hcont". - iLöb as "IH". - wp_rec. - wp_bind (! _)%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l' v' xs) "[>% [Hl' [Hstack HP]]]". - injection H; intros; subst; clear H. - wp_load. - iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto. - iDestruct "H" as "[% | H]". - * subst. - iDestruct (is_stack_empty with "Hstack") as "%". - subst. - iDestruct "Hcont" as "[_ Hfail]". - iMod ("Hfail" with "HP") as "[HQ' HP]". - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', (InjLV #()), []; iSplit; iFrame; auto. } - iModIntro. - wp_pures. - iRight; auto. - * iDestruct "H" as (q l h t) "[% Hl]". - subst. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', _, xs; iSplit; iFrame; auto. } - iModIntro. - - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. + iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (l) "[-> #Hinv]". + iLöb as "IH". + wp_lam. wp_lam. wp_bind (Load _). + iInv N as (list xs) "(Hl & Hlist & HP)" "Hclose". + wp_load. + iMod ("Hclose" with "[Hl Hlist HP]") as "_". + { iNext; iExists _, _; iFrame. } + clear xs. + iModIntro. + wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _). + iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose". + iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + destruct (decide (list = list')) as [ -> |]. + - wp_cas_suc. + iMod ("Hupd" with "HP") as "[HP HΨ]". + iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_". + { iNext; iExists (SOMEV _), (v :: xs); iFrame; iExists _, _; iFrame; auto. } + iModIntro. + wp_if. + by iApply ("HΦ" with "HΨ"). + - wp_cas_fail. + iMod ("Hclose" with "[Hl HP Hlist]"). + { iExists _, _; iFrame. } + iModIntro. + wp_if. + iApply ("IH" with "Hupd HΦ"). + Qed. - wp_load. - wp_pures. - wp_bind (CAS _ _ _). - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v' ys) "[>% [Hl'' [Hstack HP]]]". - injection H1; intros; subst; clear H1. - assert (Decision (v' = InjRV #l%V)) as Heq by apply val_eq_dec. - destruct Heq. - + subst. - wp_cas_suc. destruct ys as [|y ys]; simpl. - { iDestruct "Hstack" as %?. done. } - iDestruct "Hstack" as (q'' l' t'') "[% [Hl' Hstack]]". - injection H1; intros; subst; clear H1. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "[HP]") as "> [HQ HP]"; auto. - iDestruct (mapsto_agree with "Hl Hl'") as %[= -> ->]. - iMod ("Hclose" with "[Hl'' Hl' Hstack HP]"). - { iExists l''. eauto 10 with iFrame. } - iModIntro. - wp_if. - wp_load. - wp_pures. - iLeft; iExists _; auto. - + wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', v', ys; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hcont"). - - iIntros (v) "!# Hpush". - iLöb as "IH". - wp_rec. - wp_bind (! _)%E. - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l' v' ys) "[>% [Hl' [Hstack HP]]]". - injection H; intros; subst; clear H. + Theorem pop_works P s Ψ : + {{{ is_stack P s ∗ + (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗ + (P [] ={⊤ ∖ ↑ N}=∗ P [] ∗ Ψ NONEV) }}} + pop s + {{{ v, RET v; Ψ v }}}. + Proof. + iIntros (Φ) "(Hstack & Hupdcons & Hupdnil) HΦ". + iDestruct "Hstack" as (l) "[-> #Hinv]". + iLöb as "IH". + wp_lam. wp_bind (Load _). + iInv N as (v xs) "(Hl & Hlist & HP)" "Hclose". + wp_load. + iDestruct (is_list_disj with "Hlist") as "[Hlist H]". + iDestruct "H" as "[-> | HSome]". + - iDestruct (is_list_empty with "Hlist") as %->. + iMod ("Hupdnil" with "HP") as "[HP HΨ]". + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } + iModIntro. + wp_match. + iApply ("HΦ" with "HΨ"). + - iDestruct "HSome" as (l' h t) "[-> Hl']". + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } + iModIntro. + wp_match. wp_bind (Load _). + iInv N as (v xs') "(Hl & Hlist & HP)" "Hclose". + iDestruct "Hl'" as (q) "Hl'". wp_load. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', v', ys; iSplit; iFrame; auto. } + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } iModIntro. - wp_let. - wp_alloc lp as "Hlp". - wp_pures. - wp_bind (CAS _ _ _). - iInv N as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v'' xs) "[>% [Hl'' [Hstack HP]]]". - injection H; intros; subst; clear H. - iDestruct (is_stack_unboxed with "Hstack") as "#>%". - assert (Decision (v' = v''%V)) as Heq by apply val_eq_dec. - destruct Heq. - + subst. wp_cas_suc. - iDestruct ("Hpush" with "[HP]") as "> [HP HQ]"; auto. - iMod ("Hclose" with "[Hl'' Hlp Hstack HP]"). - { iExists l'', _, _. iFrame. simpl. eauto 10 with iFrame. } + wp_let. wp_proj. wp_bind (CAS _ _ _). + iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose". + destruct (decide (v' = (SOMEV #l'))) as [ -> |]. + * wp_cas_suc. + iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _. + simplify_eq. + iMod ("Hupdcons" with "HP") as "[HP HΨ]". + iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq. + iDestruct "Hl''" as (q') "Hl''". + iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq. + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } iModIntro. wp_if. - done. - + wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', v'', xs; iSplit; iFrame; auto. } + wp_proj. + iApply ("HΦ" with "HΨ"). + * wp_cas_fail. + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } iModIntro. wp_if. - iApply ("IH" with "Hpush"). + iApply ("IH" with "Hupdcons Hupdnil HΦ"). Qed. End stack_works. - -Program Definition is_concurrent_stack `{!heapG Σ} : concurrent_stack Σ := - {| spec.mk_stack := mk_stack |}. -Next Obligation. - iIntros (??????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). - iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. -Qed. diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v index e3565fafb82a59ce0c5257d41288de80451dbeea..7cf19331d666075f4561d9d157d78743a0bbf7c7 100644 --- a/theories/concurrent_stacks/concurrent_stack4.v +++ b/theories/concurrent_stacks/concurrent_stack4.v @@ -1,15 +1,7 @@ -(** THIS FILE CURRENTLY DOES NOT COMPILE because it has not been ported to the -stricter CAS requirements yet. *) From iris.program_logic Require Export weakestpre hoare. From iris.heap_lang Require Export lang proofmode notation. From iris.algebra Require Import excl. -From iris_examples.concurrent_stacks Require Import spec. - -Set Default Proof Using "Type". - -(** Stack 3: Helping, view-shift spec. *) - Definition mk_offer : val := λ: "v", ("v", ref #0). Definition revoke_offer : val := @@ -17,616 +9,422 @@ Definition revoke_offer : val := Definition take_offer : val := λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE. -Definition mailbox : val := - λ: "_", - let: "r" := ref NONEV in - (rec: "put" "v" := - let: "off" := mk_offer "v" in - "r" <- SOME "off";; - revoke_offer "off", - rec: "get" "n" := - let: "offopt" := !"r" in - match: "offopt" with - NONE => NONE - | SOME "x" => if: CAS (Snd "x") #0 #1 then SOME (Fst "x") else NONE - end - ). - -Definition mk_stack : val := - λ: "_", - let: "mailbox" := mailbox #() in - let: "put" := Fst "mailbox" in - let: "get" := Snd "mailbox" in - let: "r" := ref NONEV in - (rec: "pop" "n" := - match: "get" #() with - NONE => - (match: !"r" with - NONE => NONE - | SOME "hd" => - if: CAS "r" (SOME "hd") (Snd "hd") - then SOME (Fst "hd") - else "pop" "n" - end) - | SOME "x" => SOME "x" - end, - rec: "push" "n" := - match: "put" "n" with - NONE => #() - | SOME "n" => - let: "r'" := !"r" in - let: "r''" := SOME ("n", "r'") in - if: CAS "r" "r'" "r''" - then #() - else "push" "n" - end). +Definition mk_mailbox : val := λ: "_", ref NONEV. +Definition put : val := + λ: "r" "v", + let: "off" := mk_offer "v" in + "r" <- SOME "off";; + revoke_offer "off". +Definition get : val := + λ: "r", + let: "offopt" := !"r" in + match: "offopt" with + NONE => NONE + | SOME "x" => take_offer "x" + end. + +Definition mk_stack : val := λ: "_", (mk_mailbox #(), ref NONEV). +Definition push : val := + rec: "push" "p" "v" := + let: "mailbox" := Fst "p" in + let: "s" := Snd "p" in + match: put "mailbox" "v" with + NONE => #() + | SOME "v'" => + let: "tail" := ! "s" in + let: "new" := SOME (ref ("v'", "tail")) in + if: CAS "s" "tail" "new" then #() else "push" "p" "v'" + end. +Definition pop : val := + rec: "pop" "p" := + let: "mailbox" := Fst "p" in + let: "s" := Snd "p" in + match: get "mailbox" with + NONE => + match: !"s" with + NONE => NONEV + | SOME "l" => + let: "pair" := !"l" in + if: CAS "s" (SOME "l") (Snd "pair") + then SOME (Fst "pair") + else "pop" "p" + end + | SOME "x" => SOME "x" + end. Definition channelR := exclR unitR. -Class channelG Σ := { channel_inG :> inG Σ channelR }. -Definition channelΣ : gFunctors := #[GFunctor channelR]. -Instance subG_channelΣ {Σ} : subG channelΣ Σ → channelG Σ. -Proof. solve_inG. Qed. +Class channelG Σ := {channel_inG :> inG Σ channelR}. -Section side_channel. +Section proofs. Context `{!heapG Σ, !channelG Σ} (N : namespace). Implicit Types l : loc. - Definition stages γ (P : list val → iProp Σ) (Q : iProp Σ) l (v : val):= - ((l ↦ #0 ∗ (∀ vs, P vs ={⊤ ∖ ↑N}=∗ P (v :: vs) ∗ Q)) - ∨ (l ↦ #1 ∗ Q) - ∨ (l ↦ #1 ∗ own γ (Excl ())) - ∨ (l ↦ #2 ∗ own γ (Excl ())))%I. + Definition Nside_channel := N .@ "side_channel". + Definition Nstack := N .@ "stack". + Definition Nmailbox := N .@ "mailbox". - Definition is_offer γ (P : list val → iProp Σ) Q (v : val) : iProp Σ := - (∃ v' l, ⌜v = (v', #l)%V⌝ ∗ inv (N .@ "offer_inv")(stages γ P Q l v'))%I. + Definition inner_mask : coPset := ⊤ ∖ ↑Nside_channel ∖ ↑Nstack. - Definition mailbox_inv (P : list val → iProp Σ) Q (v : val) : iProp Σ := - (∃ l, ⌜v = #l⌝ ∗ (l ↦ NONEV ∨ (∃ v' γ, l ↦ SOMEV v' ∗ is_offer γ P Q v')))%I. -End side_channel. -Section stack_works. - Context `{!heapG Σ}. + Lemma inner_mask_includes : + ⊤ ∖ ↑ N ⊆ inner_mask. + Proof. solve_ndisj. Qed. - Implicit Types l : loc. + Definition revoke_tok γ := own γ (Excl ()). + Definition can_push P Q v : iProp Σ := + (∀ (xs : list val), P xs ={inner_mask}=∗ P (v :: xs) ∗ Q #())%I. + Definition access_inv (P : list val → iProp Σ) : iProp Σ := + (|={⊤ ∖ ↑Nside_channel, inner_mask}=> ∃ vs, (▷ P vs) ∗ + ((▷ P vs) ={inner_mask, ⊤ ∖ ↑Nside_channel}=∗ True))%I. + + Definition stages γ P Q l (v : val) := + ((l ↦ #0 ∗ can_push P Q v) ∨ + (l ↦ #1 ∗ Q #()) ∨ + (l ↦ #1 ∗ revoke_tok γ) ∨ + (l ↦ #2 ∗ revoke_tok γ))%I. + + Definition is_offer γ P Q (v : val) : iProp Σ := + (∃ v' l, ⌜v = (v', #l)%V⌝ ∗ inv Nside_channel (stages γ P Q l v'))%I. + + Lemma mk_offer_works P Q v : + {{{ can_push P Q v }}} + mk_offer v + {{{ o γ, RET o; is_offer γ P Q o ∗ revoke_tok γ }}}. + Proof. + iIntros (Φ) "HP HΦ". + rewrite -wp_fupd. + wp_lam. wp_alloc l as "Hl". + iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. + iMod (inv_alloc Nside_channel _ (stages γ P Q l v) with "[Hl HP]") as "#Hinv". + { iNext; iLeft; iFrame. } + iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto. + Qed. + + Lemma revoke_works γ P Q v : + {{{ is_offer γ P Q v ∗ revoke_tok γ }}} + revoke_offer v + {{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ can_push P Q v'') ∨ (⌜v' = InjLV #()⌝ ∗ (Q #())) }}}. + Proof. + iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]". + wp_let. wp_proj. wp_bind (CAS _ _ _). + iInv Nside_channel as "Hstages" "Hclose". + iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]". + - wp_cas_suc. + iMod ("Hclose" with "[Hl Hγ]") as "_". + { iNext; iRight; iRight; iFrame. } + iModIntro. + wp_if. wp_proj. + by iApply "HΦ"; iLeft; iExists _; iFrame. + - wp_cas_fail. + iMod ("Hclose" with "[Hl Hγ]") as "_". + { iNext; iRight; iRight; iLeft; iFrame. } + iModIntro. + wp_if. + iApply ("HΦ" with "[HQ]"); iRight; auto. + - wp_cas_fail. + iDestruct (own_valid_2 with "H Hγ") as %[]. + - wp_cas_fail. + iDestruct (own_valid_2 with "H Hγ") as %[]. + Qed. + + Lemma take_works γ P Q o Ψ : + let do_pop : iProp Σ := + (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v))%I in + {{{ is_offer γ P Q o ∗ access_inv P ∗ do_pop }}} + take_offer o + {{{ v', RET v'; + (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ Ψ v') ∨ (⌜v' = InjLV #()⌝ ∗ do_pop) }}}. + Proof. + simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]". + wp_lam. wp_proj. wp_bind (CAS _ _ _). + iInv Nside_channel as "Hstages" "Hclose". + iDestruct "Hstages" as "[[Hl Hpush] | [[Hl HQ] | [[Hl Hγ] | [Hl Hγ]]]]". + - iMod "Hopener" as (xs) "[HP Hcloser]". + wp_cas_suc. + iMod ("Hpush" with "HP") as "[HP HQ]". + iMod ("Hupd" with "HP") as "[HP HΨ]". + iMod ("Hcloser" with "HP") as "_". + iMod ("Hclose" with "[Hl HQ]") as "_". + { iRight; iLeft; iFrame. } + iApply fupd_intro_mask; first done. + wp_if. wp_proj. + iApply "HΦ"; iLeft; auto. + - wp_cas_fail. + iMod ("Hclose" with "[Hl HQ]") as "_". + { iRight; iLeft; iFrame. } + iModIntro. + wp_if. + iApply "HΦ"; auto. + - wp_cas_fail. + iMod ("Hclose" with "[Hl Hγ]"). + { iRight; iRight; iFrame. } + iModIntro. + wp_if. + iApply "HΦ"; auto. + - wp_cas_fail. + iMod ("Hclose" with "[Hl Hγ]"). + { iRight; iRight; iFrame. } + iModIntro. + wp_if. + iApply "HΦ"; auto. + Qed. + + Definition mailbox_inv P l : iProp Σ := + (l ↦ NONEV ∨ (∃ v' γ Q, l ↦ SOMEV v' ∗ is_offer γ P Q v'))%I. + + Definition is_mailbox P v : iProp Σ := + (∃ l, ⌜v = #l⌝ ∗ inv Nmailbox (mailbox_inv P l))%I. + + Lemma mk_mailbox_works P : + {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}. + Proof. + iIntros (Φ) "_ HΦ". + rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl". + iMod (inv_alloc Nmailbox _ (mailbox_inv P l) with "[Hl]") as "#Hinv". + { iNext; by iLeft. } + iModIntro. + iApply "HΦ"; iExists _; auto. + Qed. - Fixpoint is_stack xs v : iProp Σ := + Lemma get_works P Ψ mailbox : + let do_pop : iProp Σ := + (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v))%I in + {{{ is_mailbox P mailbox ∗ access_inv P ∗ do_pop }}} + get mailbox + {{{ ov, RET ov; (∃ v, ⌜ov = SOMEV v⌝ ∗ Ψ ov) ∨ (⌜ov = NONEV⌝ ∗ do_pop) }}}. + Proof. + simpl; iIntros (Φ) "[Hmail [Hopener Hpush]] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]". + wp_lam. wp_bind (Load _). + iInv Nmailbox as "[Hnone | Hsome]" "Hclose". + - wp_load. + iMod ("Hclose" with "[Hnone]") as "_". + { by iLeft. } + iModIntro. + wp_let. wp_match. + iApply "HΦ"; iRight; by iFrame. + - iDestruct "Hsome" as (v' γ Q) "[Hl #Hoffer]". + wp_load. + iMod ("Hclose" with "[Hl Hoffer]") as "_". + { iNext; iRight; iExists _, _, _; by iFrame. } + iModIntro. + wp_let. wp_match. wp_apply (take_works with "[Hpush Hopener]"); by iFrame. + Qed. + + Lemma put_works P Q mailbox v : + {{{ is_mailbox P mailbox ∗ can_push P Q v }}} + put mailbox v + {{{ o, RET o; (∃ v', ⌜o = SOMEV v'⌝ ∗ can_push P Q v') ∨ (⌜o = NONEV⌝ ∗ Q #()) }}}. + Proof. + iIntros (Φ) "[Hmail Hpush] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]". + wp_lam. wp_let. wp_apply (mk_offer_works with "Hpush"). + iIntros (o γ) "[#Hoffer Hrev]". + wp_let. wp_bind (Store _ _). + iInv Nmailbox as "[Hnone | Hsome]" "Hclose". + - wp_store. + iMod ("Hclose" with "[Hnone]") as "_". + { iNext; iRight; iExists _, _, _; by iFrame. } + iModIntro. + wp_let. + wp_apply (revoke_works with "[Hrev]"); first auto. + iIntros (v') "H"; iApply "HΦ"; auto. + - iDestruct "Hsome" as (? ? ?) "[Hl _]". wp_store. + iMod ("Hclose" with "[Hl]") as "_". + { iNext; iRight; iExists _, _, _; by iFrame. } + iModIntro. + wp_let. + wp_apply (revoke_works with "[Hrev]"); first auto. + iIntros (v') "H"; iApply "HΦ"; auto. + Qed. + + Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I + (at level 20, format "l ↦{-} v") : bi_scope. + + Lemma partial_mapsto_duplicable l v : + l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v. + Proof. + iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto. + Qed. + + Lemma partial_mapsto_agree l v1 v2 : + l ↦{-} v1 -∗ l ↦{-} v2 -∗ ⌜v1 = v2⌝. + Proof. + iIntros "H1 H2". + iDestruct "H1" as (?) "H1". + iDestruct "H2" as (?) "H2". + iApply (mapsto_agree with "H1 H2"). + Qed. + + Fixpoint is_list xs v : iProp Σ := (match xs with | [] => ⌜v = NONEV⌝ - | x :: xs => ∃ (t : val), ⌜v = SOMEV (x, t)%V⌝ ∗ is_stack xs t + | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t end)%I. - Definition stack_inv P v := - (∃ l v' xs, ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack xs v' ∗ P xs)%I. - - Lemma is_stack_disj xs v : - is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ (h t : val), ⌜v = SOMEV (h, t)%V⌝). + Lemma is_list_disj xs v : + is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V). Proof. - iIntros "Hstack". - destruct xs. - - iSplit; try iLeft; auto. - - iSplit; auto; iRight; iDestruct "Hstack" as (t) "[% Hstack]"; - iExists v0, t; auto. + destruct xs; auto. + iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)". + iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]". + iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto. Qed. - Lemma is_stack_uniq : ∀ xs ys v, - is_stack xs v ∗ is_stack ys v -∗ ⌜xs = ys⌝. + Lemma is_list_unboxed xs v : + is_list xs v -∗ ⌜val_is_unboxed v⌝ ∗ is_list xs v. Proof. - induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto. - - iDestruct "Hstack1" as "%". - iDestruct "Hstack2" as (t) "[% Hstack2]". - subst. - discriminate. - - iDestruct "Hstack2" as "%". - iDestruct "Hstack1" as (t) "[% Hstack1]". - subst. - discriminate. - - iDestruct "Hstack1" as (t) "[% Hstack1]". - iDestruct "Hstack2" as (t') "[% Hstack2]". - subst; injection H0; intros; subst. - iDestruct (IHxs with "[Hstack1 Hstack2]") as "%". - by iSplitL "Hstack1". - subst; auto. + iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]". + iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]". Qed. - Lemma is_stack_empty : ∀ xs, - is_stack xs (InjLV #()) -∗ ⌜xs = []⌝. + Lemma is_list_empty xs : + is_list xs (InjLV #()) -∗ ⌜xs = []⌝. Proof. - iIntros (xs) "Hstack". - destruct xs; auto. - iDestruct "Hstack" as (t) "[% rest]". - discriminate. + destruct xs; iIntros "Hstack"; auto. + iDestruct "Hstack" as (? ?) "(% & H)"; discriminate. Qed. - Lemma is_stack_cons : ∀ xs h t, - is_stack xs (InjRV (h, t)%V) -∗ - is_stack xs (InjRV (h, t)%V) ∗ ∃ ys, ⌜xs = h :: ys⌝. + + Lemma is_list_cons xs l h t : + l ↦{-} (h, t)%V -∗ + is_list xs (InjRV #l) -∗ + ∃ ys, ⌜xs = h :: ys⌝. Proof. - destruct xs; iIntros (h t) "Hstack". - - iDestruct "Hstack" as "%"; discriminate. - - iSplit; [auto | iExists xs]. - iDestruct "Hstack" as (t') "[% Hstack]". - injection H; intros; subst; auto. + destruct xs; first by iIntros "? %". + iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq. + iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto. Qed. - (* Whole-stack invariant (P). *) - Theorem stack_works {channelG0 : channelG Σ} N P Q Q' Q'' (Φ : val → iProp Σ) : - ▷ (∀ (f₁ f₂ : val), - (□(((∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs) - ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗ - WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) - ∧ (∀ (v : val), - □ ((∀ vs, P vs ={⊤ ∖ ↑ N}=∗ P (v :: vs) ∗ Q'') -∗ WP f₂ v {{ v, Q'' }}))) - -∗ Φ (f₁, f₂)%V)%I - -∗ P [] - -∗ WP mk_stack #() {{ Φ }}. + Definition stack_inv P l := + (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I. + + Definition is_stack P v := + (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox P mailbox ∗ inv Nstack (stack_inv P l))%I. + + Theorem mk_stack_works (P : list val → iProp Σ) : + {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack P v }}}. Proof. - iIntros "HΦ HP". - wp_let. - wp_let. - wp_alloc m as "Hm". - iMod (inv_alloc (N .@ "mailbox_inv") _ (mailbox_inv N P Q'' #m) with "[Hm]") as "#Imailbox". - iExists m; iSplit; auto. - wp_let. - wp_let. - wp_proj. - wp_let. - wp_proj. + iIntros (Φ) "HP HΦ". + rewrite -wp_fupd. wp_let. + wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox". wp_alloc l as "Hl". - iMod (inv_alloc (N .@ "stack_inv") _ (stack_inv P #l) with "[Hl HP]") as "#Istack". - { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. } - wp_let. - iApply "HΦ"; iSplit. - - iIntros "!# Hcont". - iLöb as "IH". - wp_rec. - wp_rec. - wp_bind (! _)%E. - iInv (N .@ "mailbox_inv") as "Hmail" "Hclose". - iDestruct "Hmail" as (m') "[>% H]". - injection H; intros; subst. - iDestruct "H" as "[Hm' | H]". - * wp_load. - iMod ("Hclose" with "[Hm']"). - { iExists m'; iSplit; auto. } - iModIntro. - wp_let. - wp_match. - wp_match. - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l' v' xs) "[>% [Hl' [Hstack HP]]]". - injection H0; intros; subst. - wp_load. - iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto. - iDestruct "H" as "[% | H]". - + subst. - iDestruct (is_stack_empty with "Hstack") as "%". - subst. - iDestruct "Hcont" as "[_ Hfail]". - iDestruct ("Hfail" with "HP") as "Hfail". - iDestruct (fupd_mask_mono with "Hfail") as "Hfail"; - last iMod "Hfail" as "[HQ' HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', (InjLV #()), []; iSplit; iFrame; auto. } - iModIntro. - wp_match. - iRight; auto. - + iDestruct "H" as (h t) "%". - subst. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', (InjRV (h, t)), xs; iSplit; iFrame; auto. } - iModIntro. + iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv". + { by iNext; iExists _, []; iFrame. } + iModIntro; iApply "HΦ"; iExists _; auto. + Qed. - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. - unfold subst; simpl; fold of_val. - - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v' ys) "[>% [Hl'' [Hstack HP]]]". - injection H3; intros; subst. - assert (Decision (v' = InjRV (h, t)%V)) as Heq by apply val_eq_dec. - destruct Heq. - ++ wp_cas_suc. - subst. - iDestruct (is_stack_cons with "Hstack") as "[Hstack H]". - iDestruct "H" as (ys') "%"; subst. - iDestruct "Hstack" as (t') "[% Hstack]". - injection H4; intros; subst. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "HP") as "Hsucc". - iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc"; - last iMod "Hsucc" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', t', ys'; iSplit; iFrame; auto. } - iModIntro. - wp_if. - wp_proj. - iLeft; iExists h; auto. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', v', ys; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hcont"). - * iDestruct "H" as (v' γ') "[Hm' Hstages]". - wp_load. - iDestruct "Hstages" as (v'' l') "[% #Hstages]". - iMod ("Hclose" with "[Hm' Hstages]"). - { iExists m'. iSplit; auto; iRight. - iExists v', γ'; iFrame. iExists v'', l'; iSplit; auto. } - iModIntro. - wp_let. - wp_match. - unfold take_offer. - subst. - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "offer_inv") as "Hstage" "Hclose". - iDestruct "Hstage" as "[H | [H | [H | H]]]". - + iDestruct "H" as "[Hl' Hmove]". - iInv (N .@ "stack_inv") as "Hstack" "Hclose2". - wp_cas_suc. - iDestruct "Hstack" as (l'' v' xs) "[% [Hl'' [Hstack HP]]]". - iDestruct ("Hmove" with "HP") as "Hmove". - iDestruct (fupd_mask_mono with "Hmove") as "Hmove"; - last iMod "Hmove" as "[HP HQ'']"; first solve_ndisj. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "HP") as "Hsucc". - iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc"; - last (iMod "Hsucc" as "[HQ HP]"); first solve_ndisj. - iMod ("Hclose2" with "[Hl'' Hstack HP]"). - { iExists l'', v', xs; iSplit; iFrame; auto. } - iModIntro. - iMod ("Hclose" with "[Hl' HQ'']"). - { iRight; iLeft; iFrame. } - iModIntro. - wp_if. - wp_proj. - - assert (to_val v'' = Some v'') by apply to_of_val. - assert (is_Some (to_val v'')) by (exists v''; auto). - assert (to_val (InjRV v'') = Some (InjRV v'')) by apply to_of_val. - assert (is_Some (to_val (InjRV v''))) by (exists (InjRV v''); auto). - wp_match. - iLeft; iExists v''; iFrame; auto. - + iDestruct "H" as "[Hl' HQ'']". - wp_cas_fail. - iMod ("Hclose" with "[Hl' HQ'']"). - { iRight; iLeft; iFrame. } - iModIntro. - wp_if. - wp_match. - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v''' xs) "[>% [Hl' [Hstack HP]]]"; simplify_eq. - wp_load. - iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto. - iDestruct "H" as "[% | H]". - ** subst. - iDestruct (is_stack_empty with "Hstack") as "%". - subst. - iDestruct "Hcont" as "[_ Hfail]". - iDestruct ("Hfail" with "HP") as "Hfail". - iDestruct (fupd_mask_mono with "Hfail") as "Hfail"; - last iMod "Hfail" as "[HQ' HP]"; first by solve_ndisj. - - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjLV #()), []; iSplit; iFrame; auto. } - iModIntro. - wp_match. - iRight; auto. - ** iDestruct "H" as (h t) "%". - subst. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjRV (h, t)), xs; iSplit; iFrame; auto. } - iModIntro. - - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. - unfold subst; simpl; fold of_val. - - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l''' v''' ys) "[>% [Hl''' [Hstack HP]]]"; simplify_eq. - destruct (decide (v''' = InjRV (h, t)%V)). - ++ wp_cas_suc. - subst. - iDestruct (is_stack_cons with "Hstack") as "[Hstack H]". - iDestruct "H" as (ys') "%"; subst. - iDestruct "Hstack" as (t') "[% Hstack]"; simplify_eq. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "HP") as "Hsucc". - iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc"; - last iMod "Hsucc" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', t', ys'; iSplit; iFrame; auto. } - iModIntro. - wp_if. - wp_proj. - iLeft; iExists h; auto. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', v''', ys; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hcont"). - + iDestruct "H" as "[Hl' Hγ']". - wp_cas_fail. - iMod ("Hclose" with "[Hl' Hγ']"). - { iRight; iRight; iLeft; iFrame. } - iModIntro. - wp_if. - wp_match. - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v''' xs) "[>% [Hl' [Hstack HP]]]"; simplify_eq. - wp_load. - iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto. - iDestruct "H" as "[% | H]". - ** subst. - iDestruct (is_stack_empty with "Hstack") as "%". - subst. - iDestruct "Hcont" as "[_ Hfail]". - iDestruct ("Hfail" with "HP") as "Hfail". - iDestruct (fupd_mask_mono with "Hfail") as "Hfail"; - last iMod "Hfail" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjLV #()), []; iSplit; iFrame; auto. } - iModIntro. - wp_match. - iRight; auto. - ** iDestruct "H" as (h t) "%". - subst. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjRV (h, t)), xs; iSplit; iFrame; auto. } - iModIntro. - - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. - unfold subst; simpl; fold of_val. - - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l''' v''' ys) "[>% [Hl''' [Hstack HP]]]"; simplify_eq. - destruct (decide (v''' = InjRV (h, t)%V)). - ++ wp_cas_suc. - subst. - iDestruct (is_stack_cons with "Hstack") as "[Hstack H]". - iDestruct "H" as (ys') "%"; subst. - iDestruct "Hstack" as (t') "[% Hstack]"; simplify_eq. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "HP") as "Hsucc". - iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc"; - last iMod "Hsucc" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', t', ys'; iSplit; iFrame; auto. } - iModIntro. - wp_if. - wp_proj. - iLeft; iExists h; auto. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', v''', ys; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hcont"). - - + iDestruct "H" as "[Hl' Hγ']". - wp_cas_fail. - iMod ("Hclose" with "[Hl' Hγ']"). - { iRight; iRight; iRight; iFrame. } - iModIntro. - wp_if. - wp_match. - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v''' xs) "[>% [Hl' [Hstack HP]]]"; simplify_eq. - wp_load. - iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto. - iDestruct "H" as "[% | H]". - ** subst. - iDestruct (is_stack_empty with "Hstack") as "%". - subst. - iDestruct "Hcont" as "[_ Hfail]". - iDestruct ("Hfail" with "HP") as "Hfail". - iDestruct (fupd_mask_mono with "Hfail") as "Hfail"; - last iMod "Hfail" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjLV #()), []; iSplit; iFrame; auto. } - iModIntro. - wp_match. - iRight; auto. - ** iDestruct "H" as (h t) "%". - subst. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l'', (InjRV (h, t)), xs; iSplit; iFrame; auto. } - iModIntro. - - assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val. - assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto). - wp_match. - unfold subst; simpl; fold of_val. - - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l''' v''' ys) "[>% [Hl''' [Hstack HP]]]"; simplify_eq. - destruct (decide (v''' = InjRV (h, t)%V)). - ++ wp_cas_suc. - subst. - iDestruct (is_stack_cons with "Hstack") as "[Hstack H]". - iDestruct "H" as (ys') "%"; subst. - iDestruct "Hstack" as (t') "[% Hstack]"; simplify_eq. - iDestruct "Hcont" as "[Hsucc _]". - iDestruct ("Hsucc" with "HP") as "Hsucc". - iDestruct (fupd_mask_mono with "Hsucc") as "Hsucc"; - last iMod "Hsucc" as "[HQ HP]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', t', ys'; iSplit; iFrame; auto. } - iModIntro. - wp_if. - wp_proj. - iLeft; iExists h; auto. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl''' Hstack HP]"). - { iExists l''', v''', ys; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hcont"). - - iIntros (v) "!# Hpush". - iLöb as "IH". - wp_rec. - wp_rec. - wp_lam. - wp_alloc s as "Hs". - wp_let. - wp_bind (_ <- _)%E. - iInv (N .@ "mailbox_inv") as "Hmail" "Hclose". - iDestruct "Hmail" as (m') "[>% Hmail]"; simplify_eq. - iMod (own_alloc (Excl ())) as (γ) "Hγ". done. - iMod (inv_alloc (N .@ "offer_inv") _ (stages N γ P Q'' s v) with "[Hs Hpush]") as "#Istages". - { iLeft; iFrame; auto. } - iDestruct "Hmail" as "[H | H]". - * wp_store. - iMod ("Hclose" with "[H]"). - { iExists m'. iSplit; auto; iRight; iExists (v, #s)%V, γ. - iFrame. iExists v, s; iSplit; auto. } - iModIntro. - wp_let. - wp_lam. - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "offer_inv") as "Hstages" "Hclose". - iDestruct "Hstages" as "[H | [H | [H | H]]]". - + iDestruct "H" as "[Hs Hpush]". - wp_cas_suc. - iMod ("Hclose" with "[Hs Hγ]"). - { iRight; iRight; iRight; iFrame. } - iModIntro. - wp_if. - wp_proj. - wp_match. - - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l' v' ys) "[>% [Hl' [Hstack HP]]]"; simplify_eq. - wp_load. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', v', ys; iSplit; iFrame; auto. } - iModIntro. - wp_let. - wp_let. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v'' xs) "[>% [Hl'' [Hstack HP]]]"; simplify_eq. - destruct (decide (v' = v''%V)). - ++ wp_cas_suc. - iDestruct ("Hpush" with "HP") as "Hpush". - iDestruct (fupd_mask_mono with "Hpush") as "Hpush"; - last iMod "Hpush" as "[HP HQ]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', (InjRV (v, v')), (v :: xs); iSplit; iFrame; auto. - iExists v'; iSplit; subst; auto. } - iModIntro. - wp_if. - done. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', v'', xs; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hpush"). - + iDestruct "H" as "[Hs HQ'']". - wp_cas_fail. - iMod ("Hclose" with "[Hs Hγ]"). - { iRight; iRight; iLeft. iFrame. } - iModIntro. - wp_if. - wp_match. - done. - + iDestruct "H" as "[Hs Hγ']". - wp_cas_fail. - by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. - + iDestruct "H" as "[Hs Hγ']". - wp_cas_fail. - by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. - * iDestruct "H" as (v' γ') "[Hm Hoffer]". - wp_store. - iMod ("Hclose" with "[Hm]"). - { iExists m'. iSplit; auto; iRight; iExists (v, #s)%V, γ. - iFrame. iExists v, s; iSplit; auto. } + Theorem push_works P s v Ψ : + {{{ is_stack P s ∗ ∀ xs, P xs ={inner_mask}=∗ P (v :: xs) ∗ Ψ #()}}} + push s v + {{{ RET #(); Ψ #() }}}. + Proof. + iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)". + iLöb as "IH" forall (v). + wp_lam. wp_lam. wp_proj. wp_let. wp_proj. wp_let. + wp_apply (put_works with "[Hupd]"); first auto. iIntros (o) "H". + iDestruct "H" as "[Hsome | [-> HΨ]]". + - iDestruct "Hsome" as (v') "[-> Hupd]". + wp_match. + wp_bind (Load _). + iInv Nstack as (list xs) "(Hl & Hlist & HP)" "Hclose". + wp_load. + iMod ("Hclose" with "[Hl Hlist HP]") as "_". + { iNext; iExists _, _; iFrame. } + clear xs. iModIntro. - wp_let. - wp_lam. - wp_proj. - wp_bind (CAS _ _ _). - iInv (N .@ "offer_inv") as "Hstages" "Hclose". - iDestruct "Hstages" as "[H | [H | [H | H]]]". - + iDestruct "H" as "[Hs Hpush]". - wp_cas_suc. - iMod ("Hclose" with "[Hs Hγ]"). - { iRight; iRight; iRight; iFrame. } + wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _). + iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose". + iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]". + destruct (decide (list = list')) as [ -> |]. + * wp_cas_suc. + iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj. + iMod ("Hupd" with "HP") as "[HP HΨ]". + iMod "Hupd'" as "_". + iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_". + { iNext; iExists (SOMEV _), (v' :: xs); iFrame; iExists _, _; iFrame; auto. } + iModIntro. + wp_if. + by iApply ("HΦ" with "HΨ"). + * wp_cas_fail. + iMod ("Hclose" with "[Hl HP Hlist]"). + { iExists _, _; iFrame. } iModIntro. wp_if. - wp_proj. + iApply ("IH" with "Hupd HΦ"). + - wp_match. iApply ("HΦ" with "HΨ"). + Qed. + Theorem pop_works P s Ψ : + {{{ is_stack P s ∗ + (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v)) ∗ + (P [] ={inner_mask}=∗ P [] ∗ Ψ NONEV) }}} + pop s + {{{ v, RET v; Ψ v }}}. + Proof. + iIntros (Φ) "(Hstack & Hupdcons & Hupdnil) HΦ". + iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)". + iLöb as "IH". + wp_lam. wp_proj. wp_let. wp_proj. wp_let. + wp_apply (get_works _ (λ v, Ψ v) with "[Hupdcons]"). + { iSplitR; first done. + iFrame. + iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose". + iModIntro. + iExists xs; iSplitL "HP"; first auto. + iIntros "HP". + iMod ("Hclose" with "[HP Hl Hlist]") as "_". + { iNext; iExists _, _; iFrame. } + auto. } + iIntros (ov) "[Hsome | [-> Hupdcons]]". + - iDestruct "Hsome" as (v) "[-> HΨ]". + wp_match. + iApply ("HΦ" with "HΨ"). + - wp_match. wp_bind (Load _). + iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose". + wp_load. + iDestruct (is_list_disj with "Hlist") as "[Hlist H]". + iDestruct "H" as "[-> | HSome]". + * iDestruct (is_list_empty with "Hlist") as %->. + iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj. + iMod ("Hupdnil" with "HP") as "[HP HΨ]". + iMod "Hupd'" as "_". + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } + iModIntro. wp_match. - wp_bind (! _)%E. - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l' v'' ys) "[>% [Hl' [Hstack HP]]]"; simplify_eq. - wp_load. - iMod ("Hclose" with "[Hl' Hstack HP]"). - { iExists l', v'', ys; iSplit; iFrame; auto. } + iApply ("HΦ" with "HΨ"). + * iDestruct "HSome" as (l' h t) "[-> Hl']". + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } iModIntro. - wp_let. - wp_let. - wp_bind (CAS _ _ _). - iInv (N .@ "stack_inv") as "Hstack" "Hclose". - iDestruct "Hstack" as (l'' v''' xs) "[>% [Hl'' [Hstack HP]]]"; simplify_eq. - destruct (decide (v'' = v'''%V)). - ++ wp_cas_suc. - iDestruct ("Hpush" with "HP") as "Hpush". - iDestruct (fupd_mask_mono with "Hpush") as "Hpush"; - last iMod "Hpush" as "[HP HQ]"; first by solve_ndisj. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', (InjRV (v, v'')), (v :: xs); iSplit; iFrame; auto. - iExists v''; iSplit; subst; auto. } - iModIntro. - wp_if. - done. - ++ wp_cas_fail. - iMod ("Hclose" with "[Hl'' Hstack HP]"). - { iExists l'', v''', xs; iSplit; iFrame; auto. } - iModIntro. - wp_if. - iApply ("IH" with "Hpush"). - + iDestruct "H" as "[Hs HQ'']". - wp_cas_fail. - iMod ("Hclose" with "[Hs Hγ]"). - { iRight; iRight; iLeft. iFrame. } + wp_match. wp_bind (Load _). + iInv Nstack as (v xs') "(Hl & Hlist & HP)" "Hclose". + iDestruct "Hl'" as (q) "Hl'". + wp_load. + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } iModIntro. - wp_if. - wp_match. - done. - + iDestruct "H" as "[Hs Hγ']". - wp_cas_fail. - by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. - + iDestruct "H" as "[Hs Hγ']". - wp_cas_fail. - by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. + wp_let. wp_proj. wp_bind (CAS _ _ _). + iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose". + destruct (decide (v' = (SOMEV #l'))) as [ -> |]. + + wp_cas_suc. + iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _. + simplify_eq. + iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj. + iMod ("Hupdcons" with "HP") as "[HP HΨ]". + iMod "Hupd'" as "_". + iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq. + iDestruct "Hl''" as (q') "Hl''". + iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq. + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } + iModIntro. + wp_if. wp_proj. + iApply ("HΦ" with "HΨ"). + + wp_cas_fail. + iMod ("Hclose" with "[Hlist Hl HP]") as "_". + { iNext; iExists _, _; iFrame. } + iModIntro. + wp_if. + iApply ("IH" with "Hupdcons Hupdnil HΦ"). Qed. -End stack_works. - -Program Definition is_concurrent_stack `{!heapG Σ, !channelG Σ} : concurrent_stack Σ := - {| spec.mk_stack := mk_stack |}. -Next Obligation. - iIntros (???????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). - iNext. iIntros (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#". -Qed. +End proofs. diff --git a/theories/concurrent_stacks/spec.v b/theories/concurrent_stacks/spec.v deleted file mode 100644 index d88aac3a2611ddd571b2d1c3cc2d71c524b09372..0000000000000000000000000000000000000000 --- a/theories/concurrent_stacks/spec.v +++ /dev/null @@ -1,34 +0,0 @@ -From stdpp Require Import namespaces. -From iris.program_logic Require Export weakestpre. -From iris.heap_lang Require Export proofmode notation. - -(** General (HoCAP-style) spec for a concurrent bag ("per-elemt spec") *) -Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag { - mk_bag : val; - mk_bag_spec (N : namespace) (P : val → iProp Σ) : - {{{ True }}} - mk_bag #() - {{{ (f₁ f₂ : val), RET (f₁, f₂); - (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) - ∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) - }}} -}. -Arguments concurrent_bag _ {_}. - -(** General (HoCAP-style) spec for a concurrent stack *) - -Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack { - mk_stack : val; - mk_stack_spec (N : namespace) (P : list val → iProp Σ) - (Q : val → iProp Σ) (Q' Q'' : iProp Σ) : - {{{ P [] }}} - mk_stack #() - {{{ (f₁ f₂ : val), RET (f₁, f₂); - (□ ( (∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs) - ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗ - WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) - ∗ (∀ (v : val), - □ ((∀ vs, P vs ={⊤ ∖ ↑ N}=∗ P (v :: vs) ∗ Q'') -∗ WP f₂ v {{ v, Q'' }})) - }}} -}. -Arguments concurrent_stack _ {_}.