Commit 49d490fe authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

improved

parent 318ce809
......@@ -82,18 +82,20 @@ Section MSQueue.
Context (P : Z iProp Σ).
Definition queue_inv (q: loc): iProp Σ :=
( (γ : gname) (l: loc), q (#l, #l) l (#0, #0) own γ ( (Excl' l)))%I.
(*(∃ h t : loc, q ↦ (#h, #t) ∗ ⌜ #h ≠ #0 ∧ #t ≠ #0 ⌝ ∗
(∃ l1 d1 : Z, h ↦ (#l1, #d1) ∗
⌜match l1 with
| 0 => True
| _ => P(d1) ∗ (∃ (l2 : loc) (d2 : Z), h ↦ (#l2, #d2) ∗ (queue_inv l2))
end⌝))%I.*)
Fixpoint queue_inv (q: loc) (L: list (prod loc Z)): iProp Σ :=
(match L with
| [] => q (#0, #0)
| (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.
Definition queueN : namespace := nroot .@ "queue".
Definition Queue (l : loc): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv q))%I.
( q: loc, l = q inv queueN (queue_inv_s q))%I.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
......@@ -110,11 +112,11 @@ Section MSQueue.
Proof.
intros. iIntros "_ Post". iApply wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (ghost_var_alloc l) as (γ) "[Hγ● Hγ◯]".
(*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 q) with "[Hq Hl Hγ●]") as "#Hinv".
{ iNext. iExists γ, l. iFrame. }
iMod (inv_alloc queueN _ (queue_inv_s q) with "[Hq Hl]") as "#Hinv".
{ iNext. iExists l, l. iFrame. iExists nil. iFrame. }
iModIntro. iApply "Post".
iExists q. eauto.
Qed.
......@@ -127,19 +129,20 @@ Section MSQueue.
intros. iIntros "#Hq Post".
iDestruct "Hq" as (l ->) "#Hinv".
wp_lam. wp_bind (!#l)%E.
iInv queueN as (γ n) "(Hq & Hl & Tok)" "Hclose".
iInv queueN as (h t) "(Hq & HL)" "Hclose".
wp_load.
iMod ("Hclose" with "[Hq Hl Tok]") as "_".
{ iNext. iExists γ, n. iFrame. }
iModIntro. wp_proj. wp_let.
wp_bind (!#n)%E.
iInv queueN as (γ' m) "(Hq & Hl & Tok)" "Hclose".
Admitted.
(*wp_load.
iMod ("Hclose" with "[Hq Hl Tok]") as "_".
{ iNext. iExists γ, n. iFrame. }
iModIntro. wp_op. wp_if.
iApply "Post". done.
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. }
iModIntro. wp_proj. wp_let.
wp_bind (!#t)%E.
iInv queueN as (h' t') "(Hq & HL)" "Hclose".
wp_load.
iMod ("Hclose" with "[Hq Hl Tok]") as "_".
{ iNext. iExists γ, n. iFrame. }
iModIntro. wp_op. wp_if.
iApply "Post". done.
Qed.*)
Lemma tryEnq_spec q x:
......
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