Commit 2c5a6373 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Is this gonna work?

parent 4c162731
......@@ -78,18 +78,18 @@ Section MSQueue.
else #0.
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR locO)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}.
Context (P : Z iProp Σ).
Fixpoint queue_inv (q: loc) (L: list (prod loc Z)): iProp Σ :=
Fixpoint queue_inv (s t: loc) (L: list (prod loc Z)): iProp Σ :=
(match L with
| [] => dummy, q (#0, #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => q (#l, #v) P(v) (queue_inv l L')
| [] => dummy, s = t s (#0, #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => dummy next_link, s (#l, #dummy) l (#next_link, #v) P(v) (queue_inv l t L')
end)%I.
Definition queue_inv_s (q: loc): iProp Σ :=
( h t: loc, q (#h, #t) L: list (prod loc Z), queue_inv h L)%I.
( s t: loc, q (#s, #t) L: list (prod loc Z), queue_inv s t L)%I.
Definition queueN : namespace := nroot .@ "queue".
Definition Queue (l : loc): iProp Σ :=
......@@ -105,7 +105,7 @@ Section MSQueue.
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, 0. iFrame. }
{ iNext. iExists l, l. iFrame. iExists nil, 0. iFrame. done. }
iModIntro. iApply "Post".
iExists q. eauto.
Qed.
......@@ -118,15 +118,16 @@ Section MSQueue.
intros. iIntros "#Hq Post".
iDestruct "Hq" as (l ->) "#Hinv".
wp_lam. wp_bind (!#l)%E.
iInv queueN as (h t) "(Hq & HL)" "Hclose".
iInv queueN as (s t) "(Hq & HL)" "Hclose".
wp_load.
iDestruct "HL" as (L) "HL".
destruct L.
- unfold queue_inv in *. iMod ("Hclose" with "[Hq HL]") as "_".
{ iNext. iExists h, t. iFrame. iExists nil. iFrame. }
- iDestruct "HL" as (d Ht) "Hs". rewrite <- Ht in *.
iMod ("Hclose" with "[Hq Hs]") as "_".
{ iNext. iExists s, s. iFrame. iExists nil, d. iFrame. done. }
iModIntro. wp_proj. wp_let.
wp_bind (!#t)%E.
iInv queueN as (h' t') "(Hq & HL)" "Hclose".
wp_bind (!#s)%E.
iInv queueN as (s' t') "(Hq & HL)" "Hclose".
wp_load.
iMod ("Hclose" with "[Hq Hl Tok]") as "_".
{ iNext. iExists γ, n. iFrame. }
......
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