hocap_spec.v 9.59 KB
Newer Older
1 2 3 4 5 6
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.
7
From iris_examples.logatom.elimination_stack Require spec.
8 9
Set Default Proof Using "Type".

10
Module logatom := elimination_stack.spec.
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50

(** 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 [] }}};
51
  push_spec N γs s (v : val) (Φ : val  iProp Σ) :
52 53
    is_stack N γs s -
    make_laterable ( l, stack_content_auth γs l ={∖↑N}= stack_content_auth γs (v::l)  Φ #()) -
54
    WP push s v {{ Φ }};
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
  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 Σ).

94
  Lemma logatom_push N γs s (v : val) :
95 96
    stack.(is_stack) N γs s -
    <<<  l : list val, stack.(stack_content_frag) γs l >>>
97
      stack.(push) s v @ ∖↑N
98 99
    <<< stack.(stack_content_frag) γs (v::l), RET #() >>>.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
100
    iIntros "Hstack". iIntros (Φ) "HΦ".
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
    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.
Ralf Jung's avatar
Ralf Jung committed
116
    iIntros "Hstack". iIntros (Φ) "HΦ".
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
    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◯]".
Hai Dang's avatar
Hai Dang committed
168
    { apply auth_both_valid. split; done. }
169 170 171 172
    iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
    iApply inv_alloc. eauto with iFrame.
  Qed.

173
  Lemma hocap_push N γs s (v : val) (Φ : val  iProp Σ) :
174 175
    hocap_is_stack N γs s -
    make_laterable ( l, hocap_stack_content_auth γs l ={∖↑N}= hocap_stack_content_auth γs (v::l)  Φ #()) -
176
    WP stack.(logatom.push) s v {{ Φ }}.
177
  Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
178 179
    iIntros "#[Hstack Hwrap] Hupd". awp_apply (logatom.push_spec with "Hstack").
    iInv "Hwrap" as (l) "[>Hcont >H●]".
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
    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*.
Ralf Jung's avatar
Ralf Jung committed
195 196
    iIntros "#[Hstack Hwrap] Hupd". awp_apply (logatom.pop_spec with "Hstack").
    iInv "Hwrap" as (l) "[>Hcont >H●]".
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
    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.
Hai Dang's avatar
Hai Dang committed
215
    iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
216 217 218
  Qed.
  Next Obligation.
    iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
Hai Dang's avatar
Hai Dang committed
219
      %[->%Excl_included%leibniz_equiv _]%auth_both_valid. done.
220 221 222 223 224 225 226 227
  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.