diff --git a/_CoqProject b/_CoqProject index 161ef1c80907fb2b43fcc30c7681066eb3ebc861..66680018374f54f310f3b47ec1cc91c3aa98b9f5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -82,3 +82,4 @@ theories/hocap/concurrent_runners.v theories/hocap/parfib.v theories/logatom_stack/stack.v +theories/logatom_stack/spec.v diff --git a/theories/logatom_stack/spec.v b/theories/logatom_stack/spec.v new file mode 100644 index 0000000000000000000000000000000000000000..263a61e8b3c650985cdbd3f0ee54ae3c4c2ebcab --- /dev/null +++ b/theories/logatom_stack/spec.v @@ -0,0 +1,41 @@ +From stdpp Require Import namespaces. +From iris.heap_lang Require Export lifting notation. +From iris.program_logic Require Export atomic. +Set Default Proof Using "Type". + +(** A general logically atomic interface for a stack. *) +Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack { + (* -- operations -- *) + new_stack : val; + push : val; + pop : val; + (* -- other data -- *) + name : Type; + (* -- predicates -- *) + is_stack (N : namespace) (γs : name) (v : val) : iProp Σ; + stack_content (γs : name) (l : list val) : iProp Σ; + (* -- predicate properties -- *) + is_stack_persistent N γs v : Persistent (is_stack N γs v); + stack_content_timeless γs l : Timeless (stack_content γs l); + stack_content_exclusive γs l1 l2 : + stack_content γs l1 -∗ stack_content γs l2 -∗ False; + (* -- operation specs -- *) + new_stack_spec N : + {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}}; + push_spec N γs s e v : + IntoVal e v → + is_stack N γs s -∗ + <<< ∀ l, stack_content γs l >>> + push (s, e) @ ⊤∖↑N + <<< stack_content γs (v::l), RET #() >>>; + pop_spec N γs s : + is_stack N γs s -∗ + <<< ∀ l, stack_content γs l >>> + pop s @ ⊤∖↑N + <<< stack_content γs (tail l), + RET match l with [] => NONEV | v :: _ => SOMEV v end >>>; +}. +Arguments atomic_stack _ {_}. + +Existing Instance is_stack_persistent. +Existing Instance stack_content_timeless. diff --git a/theories/logatom_stack/stack.v b/theories/logatom_stack/stack.v index 0a3e28733eb46c812a887cb052ea4b228d44d18c..ce4ed562d0b3216b811fccee6be4f21db4d5cf58 100644 --- a/theories/logatom_stack/stack.v +++ b/theories/logatom_stack/stack.v @@ -1,17 +1,14 @@ -From iris.heap_lang Require Export lifting notation. From iris.algebra Require Import excl auth list. From iris.base_logic.lib Require Import invariants. From iris.program_logic Require Import atomic. From iris.proofmode Require Import tactics. -From iris.heap_lang Require Import proofmode notation atomic_heap par. +From iris.heap_lang Require Import proofmode atomic_heap. From iris.bi.lib Require Import fractional. +From iris_examples.logatom_stack Require Import spec. Set Default Proof Using "Type". (** * Implement a concurrent stack with helping on top of an arbitrary atomic heap. *) -Definition stackN : namespace := nroot .@ "logatom_stack". -Definition offerN : namespace := nroot .@ "logatom_stack" .@ "offer". -Definition protoN : namespace := nroot .@ "logatom_stack" .@ "protocol". (** The CMRA & functor we need. *) (* Not bundling heapG, as it may be shared with other users. *) @@ -26,9 +23,12 @@ Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ. Proof. solve_inG. Qed. Section stack. - Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ}. + Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} (N : namespace). Notation iProp := (iProp Σ). + Let offerN := N .@ "offer". + Let stackN := N .@ "stack". + Import atomic_heap.notation. (** Code. A stack is a pair of two pointers-to-option-pointers, one for the @@ -71,7 +71,7 @@ Section stack. (* See if we can change the master head pointer *) if: CAS (Fst "stack") (SOME "head_old") (Snd "head_old_data") then (* That worked! We are done. Return the value. *) - Fst "head_old_data" + SOME (Fst "head_old_data") else (* See if there is an offer on the side-channel *) match: !(Snd "stack") with @@ -82,7 +82,7 @@ Section stack. (* Try to accept the offer. *) if: CAS (Snd "offer") #0 #1 then (* Success! We are done. Return the offered value. *) - Fst "offer" + SOME (Fst "offer") else (* Someone else was faster. Just try again. *) "pop" "stack" @@ -94,6 +94,12 @@ Section stack. (own γs (◯ Excl' l))%I. Global Instance stack_content_timeless γs l : Timeless (stack_content γs l) := _. + Lemma stack_content_exclusive γs l1 l2 : + stack_content γs l1 -∗ stack_content γs l2 -∗ False. + Proof. + iIntros "Hl1 Hl2". iDestruct (own_valid_2 with "Hl1 Hl2") as %[]. + Qed. + Definition stack_elem_to_val (stack_rep : option loc) : val := match stack_rep with | None => NONEV @@ -105,8 +111,8 @@ Section stack. Fixpoint list_inv (l : list val) (rep : option loc) : iProp := match l with | nil => ⌜rep = None⌝ - | v::l => ∃ (ℓ : loc) (rep' : option loc), ⌜rep = Some ℓ⌝ ∗ - ℓ ↦ (v, stack_elem_to_val rep') ∗ list_inv l rep' + | v::l => ∃ (ℓ : loc) q (rep' : option loc), ⌜rep = Some ℓ⌝ ∗ + ℓ ↦{q} (v, stack_elem_to_val rep') ∗ list_inv l rep' end%I. Local Hint Extern 0 (environments.envs_entails _ (list_inv (_::_) _)) => simpl. @@ -139,10 +145,13 @@ Section stack. | Some (v, st_loc) => ∃ P Q γo, inv offerN (offer_inv st_loc γo P Q) ∗ (* The persistent part of the Laterable AU *) - □ (▷ P -∗ ◇ AU << ∀ l, stack_content γs l >> @ ⊤∖↑stackN, ∅ + □ (▷ P -∗ ◇ AU << ∀ l, stack_content γs l >> @ ⊤∖↑N, ∅ << stack_content γs (v::l), COMM Q >>) end%I. + Local Instance is_offer_persistent γs offer_rep : Persistent (is_offer γs offer_rep). + Proof. destruct offer_rep as [[??]|]; apply _. Qed. + Definition offer_to_val (offer_rep : option (val * loc)) : val := match offer_rep with | None => NONEV @@ -157,7 +166,7 @@ Section stack. Local Hint Extern 0 (environments.envs_entails _ (stack_inv _ _ _)) => unfold stack_inv. Definition is_stack (γs : gname) (s : val) : iProp := - (∃ head offer : loc, ⌜s = (#head, #offer)%V⌝ ∗ inv protoN (stack_inv γs head offer))%I. + (∃ head offer : loc, ⌜s = (#head, #offer)%V⌝ ∗ inv stackN (stack_inv γs head offer))%I. Global Instance is_stack_persistent γs s : Persistent (is_stack γs s) := _. (** Proofs. *) @@ -169,24 +178,25 @@ Section stack. wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let. iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]". { apply auth_valid_discrete_2. split; done. } - iMod (inv_alloc protoN _ (stack_inv γs head offer) with "[-HΦ Hs◯]"). + iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]"). { iNext. iExists None, None, _. iFrame. done. } iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto. Qed. - Lemma push_spec γs (s v : val) : + Lemma push_spec γs s e v : + IntoVal e v → is_stack γs s -∗ <<< ∀ l, stack_content γs l >>> - push (s, v) @ ⊤∖↑stackN + push (s, e) @ ⊤∖↑N <<< stack_content γs (v::l), RET #() >>>. Proof. - iIntros "#Hinv" (Q Φ) "HQ AU". + intros <-. iIntros "#Hinv" (Q Φ) "HQ AU". iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s. iLöb as "IH". wp_let. wp_proj. wp_let. wp_proj. wp_let. wp_proj. (* Load the old head. *) wp_apply (load_spec with "[HQ AU]"); first by iAccu. - iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)". + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)". iAaccIntro with "H↦"; first by eauto 10 with iFrame. iIntros "?". iSplitL; first by eauto 10 with iFrame. iIntros "!> [HQ AU]". clear offer_rep l. @@ -195,8 +205,8 @@ Section stack. wp_let. wp_proj. (* CAS to change the head. *) wp_apply (cas_spec with "[HQ]"); [by destruct stack_rep|iAccu|]. - iAuIntro. iInv protoN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)". - iAaccIntro with "H↦"; first eauto 10 with iFrame. + iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)". + iAaccIntro with "H↦"; first by eauto 10 with iFrame. iIntros "H↦". destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as [->%stack_elem_to_val_inj|_]. @@ -205,7 +215,7 @@ Section stack. iDestruct (own_valid_2 with "Hs● Hl'") as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']". - { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl (v::l))). done. } + { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. } iMod ("Hclose" with "Hl'") as "HΦ". iModIntro. change (InjRV #head_new) with (stack_elem_to_val (Some head_new)). iSplitR "HΦ"; first by eauto 12 with iFrame. @@ -218,7 +228,7 @@ Section stack. wp_let. wp_let. wp_proj. (* Make the offer *) wp_apply (store_spec with "[HQ]"); first by iAccu. - iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)". + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)". iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame. iMod (own_alloc (Excl ())) as (γo) "Htok"; first done. iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]". @@ -231,7 +241,7 @@ Section stack. iIntros "!> HQ". wp_let. (* Retract the offer. *) wp_proj. wp_apply (store_spec with "[HQ]"); first by iAccu. - iAuIntro. iInv protoN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)". + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)". iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame. iIntros "?". iSplitR "Htok". { iClear "Hoffer". iExists _, None, _. iFrame. done. } @@ -260,6 +270,112 @@ Section stack. iDestruct (own_valid_2 with "Htok Hst") as %[]. Qed. + Lemma pop_spec γs (s : val) : + is_stack γs s -∗ + <<< ∀ l, stack_content γs l >>> + pop s @ ⊤∖↑N + <<< stack_content γs (tail l), + RET match l with [] => NONEV | v :: _ => SOMEV v end >>>. + Proof. + iIntros "#Hinv" (Q Φ) "HQ AU". + iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s. + iLöb as "IH". + wp_let. wp_proj. + (* Load the old head *) + wp_apply (load_spec with "[HQ]"); first by iAccu. + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)". + iAaccIntro with "H↦"; first by eauto 10 with iFrame. + iIntros "?". destruct l as [|v l]; simpl. + - (* The list is empty! We are already done, but it's quite some work to + prove that. *) + iDestruct "Hlist" as ">%". subst stack_rep. + iMod "AU" as (l') "[Hl' [_ Hclose]]". + iDestruct (own_valid_2 with "Hs● Hl'") as + %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + iMod ("Hclose" with "Hl'") as "HΦ". + iSplitR "HΦ"; first by eauto 10 with iFrame. + iIntros "!> HQ". wp_match. by iApply "HΦ". + - (* Non-empty list, let's try to pop. *) + iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep. + iSplitR "AU Htail"; first by eauto 15 with iFrame. + clear offer_rep l. + iIntros "!> HQ". wp_match. + wp_apply (atomic_wp_seq $! (load_spec _) with "Htail"). + iIntros "Htail". wp_let. wp_proj. wp_proj. + (* CAS to change the head *) + wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)". + iAaccIntro with "H↦"; first by eauto 10 with iFrame. + iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)). + destruct (decide (stack_elem_to_val stack_rep = stack_elem_to_val (Some tail))) as + [->%stack_elem_to_val_inj|_]. + + (* CAS succeeded! It must still be the same head element in the list, + and we are done. *) + iMod "AU" as (l') "[Hl' [_ Hclose]]". + iDestruct (own_valid_2 with "Hs● Hl'") as + %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + destruct l as [|v' l]; simpl. + { (* Contradiction. *) iDestruct "Hlist" as ">%". done. } + iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]". + iDestruct "Heq" as %[= <-]. + iDestruct (mapsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj]. + iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']". + { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. } + iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}". + iSplitR "HΦ"; first by eauto 10 with iFrame. + iIntros "!> HQ". clear q' q offer_rep l. + wp_if. wp_proj. by iApply "HΦ". + + (* CAS failed. Go on looking for an offer. *) + iSplitR "AU"; first by eauto 10 with iFrame. + iIntros "!> HQ". wp_if. clear rep stack_rep offer_rep l q tail v. + wp_proj. + (* Load the offer pointer. *) + (* FIXME: [wp_apply (load_spec with "[HQ AU]"); first by iAccu.] here triggers an anomaly. *) + wp_apply (load_spec with "[HQ]"); first by iAccu. + iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & >Hoff↦ & #Hoff)". + iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame. + iIntros "Hoff↦". iSplitR "AU"; first by eauto 10 with iFrame. + iIntros "!> HQ". destruct offer_rep as [[v offer_st_loc]|]; last first. + { (* No offer, just loop. *) wp_match. iApply ("IH" with "HQ AU"). } + clear l stack_rep. wp_match. wp_proj. + (* CAS to accept the offer. *) + wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. simpl. + iAuIntro. iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]". + iInv offerN as (offer_st) "[>Hoff↦ Hoff]". + iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame. + iIntros "Hoff↦". + destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first. + { (* CAS failed, we don't do a thing. *) + iSplitR "AU"; first by eauto 10 with iFrame. + iIntros "!> HQ". wp_if. iApply ("IH" with "HQ AU"). } + (* CAS succeeded! We accept and complete the offer. *) + destruct offer_st; try done; []. clear Heq. + iMod ("AUoff" with "Hoff") as "{AUoff IH} AUoff". + iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)". + iMod "AUoff" as (l') "[Hl' [_ Hclose]]". + iDestruct (own_valid_2 with "Hs● Hl'") as + %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']". + { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. } + iMod ("Hclose" with "Hl'") as "HQoff". + iMod "AU" as (l') "[Hl' [_ Hclose]]". + iDestruct (own_valid_2 with "Hs● Hl'") as + %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']". + { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. } + iMod ("Hclose" with "Hl'") as "HΦ". + iSplitR "Hoff↦ HQoff HΦ"; first by eauto 10 with iFrame. iSplitR "HΦ". + { iIntros "!> !> !>". iExists OfferAccepted. iFrame. } + iIntros "!> !> HQ". wp_if. wp_proj. by iApply "HΦ". + Qed. + End stack. +Definition elimination_stack `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} : + atomic_stack Σ := + {| spec.new_stack_spec := new_stack_spec; + spec.push_spec := push_spec; + spec.pop_spec := pop_spec; + spec.stack_content_exclusive := stack_content_exclusive |}. + Global Typeclasses Opaque stack_content is_stack.