Commit 7c7bc060 authored by Ralf Jung's avatar Ralf Jung

add abstract HoCAP-style spec and show that it implies the logically atomic one

parent 1835a90a
......@@ -83,3 +83,4 @@ theories/hocap/parfib.v
theories/logatom_stack/stack.v
theories/logatom_stack/spec.v
theories/logatom_stack/hocap_spec.v
From stdpp Require Import namespaces.
From iris.algebra Require Import excl auth list.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris_examples.logatom_stack Require spec.
Set Default Proof Using "Type".
Module logatom := logatom_stack.spec.
(** A general HoCAP-style interface for a stack, modeled after the spec in
[hocap/abstract_bag.v]. There are two differences:
- We split [bag_contents] into an authoritative part and a fragment as this
slightly strnegthens the spec: The logically atomic spec only requires
[stack_content ∗ stack_content] to derive a contradiction, the abstract bag
spec requires to get *three* pieces which is only possible when actually
calling a bag operation.
- We also slightly weaken the spec by adding [make_laterable], which is needed
because logical atomicity can only capture laterable resources, which is
needed when implementing e.g. the elimination stack on top of an abstract
logically atomic heap. *)
Record hocap_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_frag (γs : name) (l : list val) : iProp Σ;
stack_content_auth (γs : name) (l : list val) : iProp Σ;
(* -- predicate properties -- *)
is_stack_persistent N γs v : Persistent (is_stack N γs v);
stack_content_frag_timeless γs l : Timeless (stack_content_frag γs l);
stack_content_auth_timeless γs l : Timeless (stack_content_auth γs l);
stack_content_frag_exclusive γs l1 l2 :
stack_content_frag γs l1 - stack_content_frag γs l2 - False;
stack_content_auth_exclusive γs l1 l2 :
stack_content_auth γs l1 - stack_content_auth γs l2 - False;
stack_content_agree γs l1 l2 :
stack_content_frag γs l1 - stack_content_auth γs l2 - l1 = l2;
stack_content_update γs l l' :
stack_content_frag γs l -
stack_content_auth γs l -
|==> stack_content_frag γs l' stack_content_auth γs l';
(* -- operation specs -- *)
new_stack_spec N :
{{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s stack_content_frag γs [] }}};
push_spec N γs s e v (Φ : val iProp Σ) :
IntoVal e v
is_stack N γs s -
make_laterable ( l, stack_content_auth γs l ={⊤∖↑N}= stack_content_auth γs (v::l) Φ #()) -
WP push (s, e) {{ Φ }};
pop_spec N γs s (Φ : val iProp Σ) :
is_stack N γs s -
make_laterable ( l, stack_content_auth γs l ={⊤∖↑N}=
match l with [] => stack_content_auth γs [] Φ NONEV
| v :: l' => stack_content_auth γs l' Φ (SOMEV v) end) -
WP pop s {{ Φ }};
}.
Arguments hocap_stack _ {_}.
Existing Instance is_stack_persistent.
Existing Instance stack_content_frag_timeless.
Existing Instance stack_content_auth_timeless.
(** Show that our way of writing the [pop_spec] is equivalent to what is done in
[concurrent_stack.spec]. IOW, the conjunction-vs-match doesn't matter. Fixing
the postcondition (the [Q] in [concurrent_stack.spec]) still matters. *)
Section pop_equiv.
Context `{invG Σ} (T : Type).
Lemma pop_equiv E (I : list T iProp Σ) (Φemp : iProp Σ) (Φret : T iProp Σ) :
( l, I l ={E}=
match l with [] => I [] Φemp | v :: l' => I l' Φret v end)
⊣⊢
( v vs, I (v :: vs) ={E}= Φret v I vs)
(I [] ={E}= Φemp I []).
Proof.
iSplit.
- iIntros "HΦ". iSplit.
+ iIntros (??) "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
+ iIntros "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
- iIntros "HΦ" (l) "HI". destruct l; rewrite [(I _ _)%I]bi.sep_comm; by iApply "HΦ".
Qed.
End pop_equiv.
(** From a HoCAP stack we can directly implement the logically atomic
interface. *)
Section hocap_logatom.
Context `{!heapG Σ} (stack: hocap_stack Σ).
Lemma logatom_push N γs s e v :
IntoVal e v
stack.(is_stack) N γs s -
<<< l : list val, stack.(stack_content_frag) γs l >>>
stack.(push) (s, e) @ ⊤∖↑N
<<< stack.(stack_content_frag) γs (v::l), RET #() >>>.
Proof.
iIntros (?) "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
iApply (push_spec with "Hstack").
iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]".
iMod ("Hclose" with "Hfrag") as "HΦ". done.
Qed.
Lemma logatom_pop N γs (s : val) :
stack.(is_stack) N γs s -
<<< l : list val, stack.(stack_content_frag) γs l >>>
stack.(pop) s @ ⊤∖↑N
<<< stack.(stack_content_frag) γs (tail l),
RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
Proof.
iIntros "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
iApply (pop_spec with "Hstack").
iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
destruct l;
iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]";
iMod ("Hclose" with "Hfrag") as "HΦ"; done.
Qed.
Definition hocap_logatom : logatom.atomic_stack Σ :=
{| logatom.new_stack_spec := stack.(new_stack_spec);
logatom.push_spec := logatom_push;
logatom.pop_spec := logatom_pop;
logatom.stack_content_exclusive := stack.(stack_content_frag_exclusive) |}.
End hocap_logatom.
(** From a logically atomic stack, we can implement a HoCAP stack by adding an
auth invariant. *)
(** The CMRA & functor we need. *)
Class hocapG Σ := HocapG {
hocap_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
}.
Definition hocapΣ : gFunctors :=
#[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
Instance subG_hocapΣ {Σ} : subG hocapΣ Σ hocapG Σ.
Proof. solve_inG. Qed.
Section logatom_hocap.
Context `{!heapG Σ} `{!hocapG Σ} (stack: logatom.atomic_stack Σ).
Definition hocap_name : Type := stack.(logatom.name) * gname.
Implicit Types γs : hocap_name.
Definition hocap_stack_content_auth γs l : iProp Σ := own γs.2 ( Excl' l).
Definition hocap_stack_content_frag γs l : iProp Σ := own γs.2 ( Excl' l).
Definition hocap_is_stack N γs v : iProp Σ :=
(stack.(logatom.is_stack) (N .@ "stack") γs.1 v
inv (N .@ "wrapper") ( l, stack.(logatom.stack_content) γs.1 l hocap_stack_content_auth γs l))%I.
Lemma hocap_new_stack N :
{{{ True }}}
stack.(logatom.new_stack) #()
{{{ γs s, RET s; hocap_is_stack N γs s hocap_stack_content_frag γs [] }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
iIntros "!>" (γs s) "[Hstack Hcont]".
iMod (own_alloc ( Excl' [] Excl' [])) as (γw) "[Hs● Hs◯]".
{ apply auth_valid_discrete_2. split; done. }
iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
iApply inv_alloc. eauto with iFrame.
Qed.
Lemma hocap_push N γs s e v (Φ : val iProp Σ) :
IntoVal e v
hocap_is_stack N γs s -
make_laterable ( l, hocap_stack_content_auth γs l ={⊤∖↑N}= hocap_stack_content_auth γs (v::l) Φ #()) -
WP stack.(logatom.push) (s, e) {{ Φ }}.
Proof using Type*.
iIntros (?) "#[Hstack Hwrap] Hupd". iApply (logatom.push_spec with "Hstack"); first iAccu.
iAuIntro. iInv "Hwrap" as (l) "[>Hcont >H●]".
iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
iIntros "Hcont".
iMod fupd_intro_mask' as "Hclose";
last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
iMod "Hclose" as "_". iIntros "!>".
eauto with iFrame.
Qed.
Lemma hocap_pop N γs s (Φ : val iProp Σ) :
hocap_is_stack N γs s -
make_laterable ( l, hocap_stack_content_auth γs l ={⊤∖↑N}=
match l with [] => hocap_stack_content_auth γs [] Φ NONEV
| v :: l' => hocap_stack_content_auth γs l' Φ (SOMEV v) end) -
WP stack.(logatom.pop) s {{ Φ }}.
Proof using Type*.
iIntros "#[Hstack Hwrap] Hupd". iApply (logatom.pop_spec with "Hstack"); first iAccu.
iAuIntro. iInv "Hwrap" as (l) "[>Hcont >H●]".
iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
iIntros "Hcont". destruct l.
- iMod fupd_intro_mask' as "Hclose";
last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
- iMod fupd_intro_mask' as "Hclose";
last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
Qed.
Program Definition logatom_hocap : hocap_stack Σ :=
{| new_stack_spec := hocap_new_stack;
push_spec := hocap_push;
pop_spec := hocap_pop |}.
Next Obligation.
iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
Qed.
Next Obligation.
iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
Qed.
Next Obligation.
iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. done.
Qed.
Next Obligation.
iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
by iFrame.
Qed.
End logatom_hocap.
......@@ -25,12 +25,12 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
push_spec N γs s e v :
IntoVal e v
is_stack N γs s -
<<< l, stack_content γs l >>>
<<< l : list val, 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 >>>
<<< l : list val, stack_content γs l >>>
pop s @ ⊤∖↑N
<<< stack_content γs (tail l),
RET match l with [] => NONEV | v :: _ => SOMEV v end >>>;
......
......@@ -186,25 +186,25 @@ Section stack.
Lemma push_spec γs s e v :
IntoVal e v
is_stack γs s -
<<< l, stack_content γs l >>>
<<< l : list val, stack_content γs l >>>
push (s, e) @ ⊤∖↑N
<<< stack_content γs (v::l), RET #() >>>.
Proof.
intros <-. iIntros "#Hinv" (Q Φ) "HQ AU".
iIntros (<-) "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "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.
wp_apply (load_spec with "[AU]"); first by iAccu.
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.
iIntros "!> AU". clear offer_rep l.
(* Go on. *)
wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
wp_let. wp_proj.
(* CAS to change the head. *)
wp_apply (cas_spec with "[HQ]"); [by destruct stack_rep|iAccu|].
wp_apply cas_spec; [by destruct stack_rep|iAccu|].
iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
iAaccIntro with "H↦"; first by eauto 10 with iFrame.
iIntros "H↦".
......@@ -219,15 +219,15 @@ Section stack.
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.
iIntros "Q". wp_if. by iApply "HΦ".
iIntros "_". wp_if. by iApply "HΦ".
- (* The CAS failed, go on making an offer. *)
iModIntro. iSplitR "AU"; first by eauto 8 with iFrame.
clear stack_rep stack_rep' offer_rep l head_new.
iIntros "HQ". wp_if.
iIntros "H". wp_if.
wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
wp_let. wp_let. wp_proj.
(* Make the offer *)
wp_apply (store_spec with "[HQ]"); first by iAccu.
wp_apply store_spec; first by iAccu.
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.
......@@ -238,33 +238,33 @@ Section stack.
{ iClear "Hoffer". iExists _, (Some (v, st_loc)), _. iFrame.
rewrite /is_offer /=. iExists _, _, _. iFrame "AU_back Hoinv". done. }
clear stack_rep offer_rep l.
iIntros "!> HQ". wp_let.
iIntros "!> _". wp_let.
(* Retract the offer. *)
wp_proj. wp_apply (store_spec with "[HQ]"); first by iAccu.
wp_proj. wp_apply store_spec; first by iAccu.
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. }
iIntros "!> HQ". wp_seq.
iIntros "!> _". wp_seq.
clear stack_rep offer_rep l.
(* See if someone took it. *)
wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
wp_apply cas_spec; [done|iAccu|].
iAuIntro. iInv offerN as (offer_st) "[>Hst↦ Hst]".
iAaccIntro with "Hst↦"; first by eauto 10 with iFrame.
iIntros "Hst↦". destruct offer_st; simpl.
+ (* Offer was still pending, and we revoked it. Loop around and try again. *)
iModIntro. iSplitR "Hst".
{ iNext. iExists OfferRevoked. iFrame. }
iIntros "HQ".
iIntros "_".
iDestruct ("AU_back" with "Hst") as ">AU {AU_back Hoinv}". clear AU_later.
wp_if. iApply ("IH" with "HQ AU").
wp_if. iApply ("IH" with "AU").
+ (* Offer revoked by someone else? Impossible! *)
iDestruct "Hst" as ">Hst".
iDestruct (own_valid_2 with "Htok Hst") as %[].
+ (* Offer got accepted by someone, awesome! We are done. *)
iModIntro. iSplitR "Hst".
{ iNext. iExists OfferAcked. iFrame. }
iIntros "HQ". wp_if. by iApply "Hst".
iIntros "_". wp_if. by iApply "Hst".
+ (* Offer got acked by someone else? Impossible! *)
iDestruct "Hst" as ">Hst".
iDestruct (own_valid_2 with "Htok Hst") as %[].
......@@ -277,12 +277,12 @@ Section stack.
<<< stack_content γs (tail l),
RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
Proof.
iIntros "#Hinv" (Q Φ) "HQ AU".
iIntros "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "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.
wp_apply load_spec; 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.
......@@ -294,16 +294,16 @@ Section stack.
%[->%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Φ".
iIntros "!> _". 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.
iIntros "!> _". 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|].
wp_apply cas_spec; [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)).
......@@ -323,23 +323,22 @@ Section stack.
{ 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.
iIntros "!> _". 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.
iIntros "!> _". 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.
wp_apply load_spec; 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"). }
iIntros "!> _". destruct offer_rep as [[v offer_st_loc]|]; last first.
{ (* No offer, just loop. *) wp_match. iApply ("IH" with "AU"). }
clear l stack_rep. wp_match. wp_proj.
(* CAS to accept the offer. *)
wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. simpl.
wp_apply cas_spec; [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.
......@@ -347,7 +346,7 @@ Section stack.
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"). }
iIntros "!> _". wp_if. iApply ("IH" with "AU"). }
(* CAS succeeded! We accept and complete the offer. *)
destruct offer_st; try done; []. clear Heq.
iMod ("AUoff" with "Hoff") as "{AUoff IH} AUoff".
......@@ -366,7 +365,7 @@ Section stack.
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Φ".
iIntros "!> !> _". wp_if. wp_proj. by iApply "HΦ".
Qed.
End stack.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment