Commit 5bceb320 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

new done. deq almost done.

parent 95c666b0
......@@ -61,15 +61,25 @@ Section MSQueue.
else #0.
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR gnameO)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR gnameO)))}.
Context (P : Z iProp Σ).
Local Notation iTok γ := (own γ (Excl ())).
Lemma unit_tok_exclusive γ: iTok γ iTok γ False.
Proof.
iIntros "excl". rewrite -own_op.
iDestruct (own_valid with "excl") as %Valid.
by apply (excl_exclusive (Excl ())) in Valid.
Qed.
Fixpoint queue_inv (h t: loc) (γc γ: gname) (L: list (prod loc Z)): iProp Σ :=
(match L with
| [] => dummy, h = t h (#0, #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => dummy next_link γ', h (#l, #dummy)
(own γc ( (Excl' γ)) (l (#next_link, #v) P(v) own γc ( (Excl' γ')))) (queue_inv l t γc γ' L')
| (l, v) :: L' => dummy next_link γ', h (#l, #dummy) own γc ( (Excl' γ))
(iTok γ (l (#next_link, #v) P(v) own γc ( (Excl' γ')))) (queue_inv l t γc γ' L')
end)%I.
Definition queue_inv_s (q: loc) (γc: gname): iProp Σ :=
......@@ -79,7 +89,7 @@ Section MSQueue.
Definition Queue (l : loc) (γc: gname): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q γc))%I.
Definition Consumer (q: loc) (γc: gname): iProp Σ := ( (h: loc) (γ: gname), q {1/2} #h own γc ( (Excl' γ)))%I.
Definition Consumer (q: loc) (γc: gname): iProp Σ := ( (h: loc) (γ: gname), q {1/2} #h own γc ( (Excl' γ)) iTok γ)%I.
Definition Producer (q: loc): iProp Σ := ( (t: loc), (q + 1) {1/2} #t)%I.
Lemma ghost_var_alloc n :
......@@ -116,7 +126,7 @@ Section MSQueue.
intros. iIntros "_ Post". iApply wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (ghost_var_alloc γ) as (γc) "[Hγc● Hγc◯]". iClear "Hγ".
iMod (ghost_var_alloc γ) as (γc) "[Hγc● Hγc◯]".
wp_let. wp_alloc q as "(Hh & Ht)". lia. rewrite big_sepL_singleton.
wp_let. do 2 (wp_op; wp_store).
rewrite loc_add_0.
......@@ -134,7 +144,7 @@ Section MSQueue.
Lemma findTail_spec q γc:
{{{ Queue q γc Producer q }}}
findTail #q
{{{ (n: loc), RET #n; True }}}.
{{{ (n: loc), RET #n; Producer q }}}.
Proof.
intros. iIntros "[#Hq Hp] Post".
iDestruct "Hq" as (l ->) "#Hinv".
......@@ -164,7 +174,7 @@ Section MSQueue.
Lemma tryEnq_spec q x γc:
{{{ Queue q γc Producer q P x }}}
tryEnq #q #x
{{{ (z: Z), RET #z; z 0 P x }}}.
{{{ (z: Z), RET #z; Producer q ( z 0 P x) }}}.
Proof.
intros. iIntros "(#Hq & Hp & P) Post".
(* iDestruct "Hq" as (γ l) "(Hq & Hl & Tok)". *)
......@@ -183,33 +193,47 @@ Section MSQueue.
Instance inhabited_base_lit : Inhabited base_lit := populate (LitUnit).
Lemma tryDeq_spec q γc:
{{{ Queue q γc Consumer q γc}}}
{{{ Queue q γc Consumer q γc }}}
tryDeq #q
{{{ x, RET #x; x = 0 P x }}}.
{{{ x, RET #x; Consumer q γc ( x = 0 P x) }}}.
Proof.
intros. iIntros "(#Hq & Hc) Post".
wp_lam. wp_op. rewrite loc_add_0.
iDestruct "Hq" as (l ->) "#Hinv".
iDestruct "Hc" as (h s) "(Hhc & Hγc◯)".
iDestruct "Hc" as (h s) "(Hhc & Hγc◯ & Hγ)".
wp_bind (!#l)%E.
wp_load.
wp_let. wp_bind (!#h)%E.
iInv queueN as (h' t) "(>Hhq & >Htq & HL)" "Hclose".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (L γ) "Hr".
iInduction L as [|(l',v) L'] "IHL'" forall (s h t γ).
destruct L as [|(l',v) L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% Hh]". subst t.
wp_load.
iMod ("Hclose" with "[Hhq Htq Hh]") as "_".
{ iNext. iExists h, h. iFrame. iExists nil, γ, d. iFrame. done. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if. iApply "Post". by iLeft.
- iDestruct "Hr" as (d l'' γ') "(>Hh & HTrade & HL')".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, s. iFrame. by iLeft.
- iDestruct "Hr" as (d l'' γ') "(>Hh & >Hγc● & HTrade & HL')".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %<-.
wp_load.
iDestruct "HTrade" as "[Hγc● | Hl]".
+ iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %<-.
iCombine "Hγ" "HTrade" as "HTrade". rewrite bi.sep_or_l.
rewrite unit_tok_exclusive. iDestruct "HTrade" as "[HF|[Hγ Hl']]"; try done.
iDestruct "Hl'" as "(Hl' & Pv & Hγ'c●)".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ HL']") as "_".
{ iNext. iExists h, t. iFrame. iExists ((l', v) :: L'), γ, d, l'', γ'. iFrame. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if.
wp_op. rewrite loc_add_0.
wp_bind (CmpXchg _ _ _).
iInv queueN as (h' t') "(>Hhq & >Htq & HL)" "Hclose".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iCombine "Hhc" "Hhq" as "Hh". wp_cmpxchg_suc.
iDestruct "Hh" as "(Hhc & Hhq)".
iDestruct (ghost_var_agree with "Hγ'c● Hγc◯") as %<-.
iMod (ghost_var_update γc γ' with "Hγ'c● Hγc◯") as "[Hγ'c● Hγ'c◯]".
iMod ("Hclose" with "[Hhq Htq HL]") as "_".
{ iNext. iExists l', t'. iFrame. }
Admitted.
End proof.
......
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