Commit bcd51c6c authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

alloc added. newQueue proved. deq near to the end

parent 4ced3d79
From iris.proofmode Require Import tactics.
From iris.algebra Require Import cmra auth list.
From iris.base_logic.lib Require Import own.
From iris.base_logic.lib Require Import own invariants.
Lemma eq_app_nil {A: Type} (x y : list A) :
x = x ++ y y = [].
......@@ -127,6 +128,14 @@ Section lp_auth.
Context (A: Type) `{EqDecision A} {EquivA : Equiv A} `{@Equivalence A EquivA} `{@LeibnizEquiv A EquivA}
`{inG Σ (authR (@lpUR A _ _ _ _))}.
Lemma ghost_var_lp_alloc (V: list A):
(|==> γ, own γ ( (ListSome V)))%I.
Proof.
iMod (own_alloc ( (ListSome V) (ListSome V))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma own_lat_auth_update γ (V V': list A) (Ext: V `prefix_of` V'):
own γ ( (ListSome V)) == own γ ( (ListSome V')) own γ ( (ListSome V')).
Proof.
......
......@@ -61,7 +61,7 @@ Section MSQueue.
else #0.
Section proof.
Definition my_master_camera := (authR (@lpUR (loc * Z) _ _ _)).
Definition my_master_camera := (authR (@lpUR (loc * Z) _ _ _ _)).
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO locO ZO)) gnameO)))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_master_camera, !inG Σ my_camera}.
......@@ -85,18 +85,20 @@ Section MSQueue.
end)%I.
(*Typeclasses eauto := debug.*)
Definition queue_inv_s (q: loc) (γc: gname): iProp Σ :=
Definition queue_inv_s (q: loc) (γc γm: gname): iProp Σ :=
( (h t: loc) (Lout: list (loc * Z)) (γ: gname),
q {1/2} #h (q + 1) {1/2} #t own γc ( (Excl' (Lout, γ)))
( (Lin: list (loc * Z)),
own γc ( (ListSome (Lout ++ Lin))) queue_inv h t γ Lin)
own γm ( (ListSome (Lout ++ Lin))) queue_inv h t γ Lin)
)%I.
Definition queueN : namespace := nroot .@ "queue".
Definition Queue (l : loc) (γc: gname): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q γc))%I.
Definition Queue (l : loc) (γc γm: gname): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q γc γm))%I.
Definition Consumer (q: loc) (γc: gname): iProp Σ := ( (h: loc) (Lout: list (loc * Z)) (γ: gname), q {1/2} #h own γc ( (Excl' (Lout, γ))) iTok γ)%I.
Definition Consumer (q: loc) (γc γm: gname): iProp Σ :=
( (h: loc) (Lout Lin: list (loc * Z)) (γ: gname),
q {1/2} #h own γc ( (Excl' (Lout, γ))) own γm ( (ListSome (Lout ++ Lin))) iTok γ)%I.
Definition Producer (q: loc): iProp Σ := ( (t: loc), (q + 1) {1/2} #t)%I.
Lemma ghost_var_alloc n :
......@@ -128,25 +130,26 @@ Section MSQueue.
Lemma newQueue_spec:
{{{ True }}}
(newQueue #())
{{{ q, RET #q; γc, Queue q γc Producer q Consumer q γc}}}.
{{{ q, RET #q; γc γm, Queue q γc γm Producer q Consumer q γc γm}}}.
Proof.
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 (nil, γ)) as (γc) "[Hγc● Hγc◯]".
iMod (ghost_var_alloc (nil ++ nil)) as (γc) "[Hγc● Hγc◯]".
iMod (ghost_var_lp_alloc _ (nil ++ nil)) as (γm) "Hγm●".
iMod (own_lat_auth_update_fork _ _ _ with "Hγm●") as "[Hγm● Hγm◯]".
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.
iDestruct "Hh" as "[Hhq Hhc]".
iDestruct "Ht" as "(Htq & Htp)".
iMod (inv_alloc queueN _ (queue_inv_s q γc) with "[Hhq Htq Hl Hγc●]") as "#Hinv".
{ iNext. iExists l, l, nil, γ. iFrame. iExists nil. iFrame. done. }
iMod (inv_alloc queueN _ (queue_inv_s q γc γm) with "[Hhq Htq Hl Hγc● Hγm●]") as "#Hinv".
{ iNext. iExists l, l, nil, γ. iFrame. iExists nil. iFrame. iExists 0. iFrame. done. }
iModIntro. iApply "Post".
iExists γc.
iExists γc, γm.
iSplitL "Hinv". iExists q. eauto.
iSplitL "Htp". iExists l. iFrame.
iExists l, γ. iFrame.
iExists l, nil, nil, γ. iFrame.
Qed.
(*Lemma findTail_spec q γc:
......@@ -178,8 +181,8 @@ Section MSQueue.
iApply "Post". done.
Qed.*)*)
Lemma tryEnq_spec q x γc:
{{{ Queue q γc Producer q P x }}}
Lemma tryEnq_spec q x γc γm:
{{{ Queue q γc γm Producer q P x }}}
tryEnq #q #x
{{{ (z: Z), RET #z; Producer q ( z 0 P x) }}}.
Proof.
......@@ -188,59 +191,73 @@ Section MSQueue.
wp_lam. wp_let.
wp_alloc n as "Hn". wp_let.
wp_load; wp_proj; wp_store.
(*wp_rec.*)
wp_op. wp_let.
(*wp_rec.
wp_bind ((rec: "getTail" "q" := _) #q)%V.
wp_rec.
wp_bind (findTail #q).
(*iApply (findTail_spec q with "[Hq Hp]"). iFrame. done.
iApply (findTail_spec q with "[Hq Hp]"). iFrame. done.
iNext. iIntros (t) "_".
wp_let.*)
Admitted.
Lemma prefix_app_inv : (A : Type) (l l1 l2 : list A),
l ++ l1 `prefix_of` l ++ l2 l1 `prefix_of` l2.
Proof.
intros. inversion H. Admitted.
Instance inhabited_base_lit : Inhabited base_lit := populate (LitUnit).
Lemma tryDeq_spec q γc:
{{{ Queue q γc Consumer q γc }}}
Lemma tryDeq_spec q γc γm:
{{{ Queue q γc γm Consumer q γc γm }}}
tryDeq #q
{{{ x, RET #x; Consumer q γc ( x = 0 P x) }}}.
{{{ x, RET #x; Consumer q γc γm ( 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◯ & Hγ)".
iDestruct "Hc" as (h Lout Lin s) "(Hhc & Hγc◯ & Hγm◯ & Hγ)".
wp_bind (!#l)%E.
wp_load.
wp_let. wp_bind (!#h)%E.
iInv queueN as (h' t γ) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iInv queueN as (h' t Lout' γ) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (L) "Hr".
destruct L as [|(l',v) L'] eqn:HL.
iDestruct "HL" as (Lin') "(>Hγm● & Hr)".
destruct Lin' as [|(l',v) L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% Hh]". subst t.
wp_load.
iMod ("Hclose" with "[Hhq Htq Hh Hγc●]") as "_".
{ iNext. iExists h, h, γ. iFrame. iExists nil, d. iFrame. done. }
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm●]") as "_".
{ iNext. iExists h, h, Lout', γ. iFrame. iExists nil. iFrame. iExists d. iFrame. done. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, s. iFrame. by iLeft.
wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, Lout, Lin, s. iFrame. by iLeft.
- iDestruct "Hr" as (d l'' γ') "(>Hh & HTrade & Hr)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %<-.
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H.
inversion H. rewrite <- H2.
iClear "Hγm◯".
iMod (own_lat_auth_update_fork _ _ _ with "Hγm●") as "[Hγm● Hγm◯]".
wp_load.
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γ')".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ Hr]") as "_".
{ iNext. iExists h, t, γ. iFrame. iExists ((l', v) :: L'), d, l', γ'. iFrame. }
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm● Hγ Hr]") as "_".
{ iNext. iExists h, t, Lout, γ. iFrame. iExists ((l', v) :: L'). iFrame. iExists 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 & Hγ'c● & HL)" "Hclose".
iInv queueN as (h' t' Lout'' γ'') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct "HL" as (Lin'') "(>Hγm● & Hr)".
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 _ γ' with "Hγ'c● Hγc◯") as "(Hγc● & Hγc◯)".
iMod ("Hclose" with "[Hhq Htq HL Hγc●]") as "_".
{ iNext. iExists l', t', γ'. iFrame. iExists L', γ'. iFrame. }
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H.
inversion H. rewrite <- H2.
iDestruct (own_lat_auth_max _ _ with "[Hγm● Hγm◯]") as %Hpre. iFrame.
iMod (ghost_var_update _ (Lout ++ [(l', v)], γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iMod (own_lat_auth_update _ _ _ (Lout ++ (l', v) :: L') Hpre with "Hγm●") as "[Hγm● Hγm◯]".
iMod ("Hclose" with "[Hhq Htq Hr Hγc● Hγm●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v)]), γ'. iFrame. iExists L'. iFrame.
iExists }
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