Commit 4c162731 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

some minor changes to the invariant

parent 49d490fe
......@@ -84,12 +84,10 @@ Section MSQueue.
Fixpoint queue_inv (q: loc) (L: list (prod loc Z)): iProp Σ :=
(match L with
| [] => q (#0, #0)
| [] => dummy, q (#0, #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => q (#l, #v) P(v) (queue_inv l L')
end)%I.
(*∗ own γ (● (Excl' l))*)
Definition queue_inv_s (q: loc): iProp Σ :=
( h t: loc, q (#h, #t) L: list (prod loc Z), queue_inv h L)%I.
......@@ -97,14 +95,6 @@ Section MSQueue.
Definition Queue (l : loc): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q))%I.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma newQueue_spec:
{{{ True }}}
(newQueue #())
......@@ -112,11 +102,10 @@ Section MSQueue.
Proof.
intros. iIntros "_ Post". iApply wp_fupd.
wp_lam. wp_alloc l as "Hl".
(*iMod (ghost_var_alloc l) as (γ) "[Hγ● Hγ◯]".*)
wp_let. wp_alloc q as "Hq". wp_let.
do 2 (wp_load; wp_proj; wp_store).
iMod (inv_alloc queueN _ (queue_inv_s q) with "[Hq Hl]") as "#Hinv".
{ iNext. iExists l, l. iFrame. iExists nil. iFrame. }
{ iNext. iExists l, l. iFrame. iExists nil, 0. iFrame. }
iModIntro. iApply "Post".
iExists q. eauto.
Qed.
......
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