Commit f1d05839 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

changes in enq

parent d3a14f04
......@@ -64,20 +64,10 @@ Section MSQueue.
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) (L: list (loc * Z)): iProp Σ :=
(match L with
| [] => dummy, h = t (h #0 (h + 1) #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => dummy nl, h #l (h + 1) #dummy
(l #nl (l + 1) #v P(v)) (queue_inv l t L')
| [] => h = t h #0
| (l, v) :: L' => dummy, h #l (h + 1) #dummy (l + 1) #v P(v) queue_inv l t L'
end)%I.
Definition queue_inv_s (q: loc) (γc γp: gname): iProp Σ :=
......@@ -113,7 +103,7 @@ Section MSQueue.
iDestruct "Hh" as "[Hhq Hhc]".
iDestruct "Ht" as "(Htq & Htp)".
iMod (inv_alloc queueN _ (queue_inv_s q γc γp) with "[Hhq Htq Hl Hd Hγc● Hγp●1]") as "#Hinv".
{ iNext. iExists l, l, nil. iFrame. iExists nil. iFrame. iExists 0. rewrite loc_add_0. iFrame. done. }
{ iNext. iExists l, l, nil. iFrame. iExists nil. iFrame. rewrite loc_add_0. by iFrame. }
iModIntro. iApply "Post".
iExists γc, γp.
iSplitL "Hinv". iExists q. eauto.
......@@ -168,18 +158,26 @@ Section MSQueue.
iDestruct (mapsto_agree with "Htp Htq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (Lin) "(>Hγp●1 & Hr)".
destruct Lin as [|[l' v] L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% [Htl Htd]]". subst h.
- iDestruct "Hr" as ">[% Htl]". subst t.
rewrite loc_add_0. wp_store.
assert (Agr: Lout ++ [] = L). admit. subst.
(* rewrite app_nil_r.
assert (Agr: Lout ++ [] = L). admit. subst L.
(* iAssert (Lout ++ [] ≡ L)%I with "[Hγp●1 Hγp●2]" as "Agr".
{ iApply (own_lat_auth_frac_agree _ γp (Lout ++ []) L (1/2) (1/2) with "[Hγp●1 Hγp●2]"). subst.
rewrite app_nil_r.
assert (own γp (●{1 / 2} ListSome Lout ⋅ ●{1 / 2} ListSome L) → ListSome Lout ≡ ListSome L).
*)
iCombine "Hγp●1" "Hγp●2" as "Hγp●".
iMod (@own_lat_auth_update (leibnizO (loc * Z)) _ _ _ _ _ _ (Lout ++ [(n, x)]) _ with "Hγp●") as "[[Hγp●1 Hγp●2] _]".
iMod ("Hclose" with "[Hhq Htq Htl Htd Hnl Hnd Hγc● Hγp●1 Px]") as "_".
{ iNext. iExists _, _, _. iFrame. iExists _. iFrame. iExists _, _.
iMod ("Hclose" with "[Hhq Htq Htl Hnl Hnd Hγc● Hγp●1 Px]") as "_".
{ iNext. iExists _, _, _. iFrame. iExists _. iFrame. iExists _.
rewrite loc_add_0. iFrame. admit. } (* problematique invariant in one elem case *)
iModIntro. wp_seq. wp_op. wp_bind (_ <- _)%E.
iModIntro. wp_seq. wp_op. wp_bind (_ <- _)%E.
iInv queueN as (h' t Lout') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct "HL" as (Lin') "(>Hγp●1 & Hr)".
iDestruct (mapsto_agree with "Htp Htq") as %?.
assert (Agr: Lout ++ [(n, x)] = Lout' ++ Lin'). admit. rewrite <- Agr.
iCombine "Hγp●1" "Hγp●2" as "Hγp●".
(*iDestruct "Hr" as ">[% Htl]".*)
Admitted.
Lemma tryDeq_spec q γc γp:
......@@ -198,18 +196,18 @@ Section MSQueue.
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (Lin) "(>Hγp● & Hr)".
destruct Lin as [|[l' v] L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% [Hh Hd]]". subst t.
- iDestruct "Hr" as ">[% Hh]". subst t.
wp_load.
iMod ("Hclose" with "[Hhq Htq Hh Hd Hγc● Hγp●]") as "_".
{ iNext. iExists h, h, Lout'. iFrame. iExists nil. iFrame. iExists d. iFrame. done. }
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγp●]") as "_".
{ iNext. iExists h, h, Lout'. iFrame. iExists nil. by iFrame. }
iModIntro. wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, Lout. iFrame. by iLeft.
- iDestruct "Hr" as (d l'') "(>Hh & >Hd & HTrade & Hr)".
- iDestruct "Hr" as (d) "(>Hh & >Hd & HTrade & Hr)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H. subst.
iMod (own_lat_auth_update_fork _ _ _ with "Hγp●") as "[Hγp● Hγp◯]".
wp_load.
iMod ("Hclose" with "[HTrade Hhq Htq Hh Hd Hγc● Hγp● Hr]") as "_".
{ iNext. iExists h, t, Lout. iFrame.
iExists ((l', v) :: L'). iFrame. iExists d, l''. iFrame. }
iExists ((l', v) :: L'). iFrame. iExists d. iFrame. }
iModIntro. wp_let. wp_op. wp_if.
wp_op. rewrite loc_add_0. wp_bind (_ <- _)%E.
iInv queueN as (h' t' Lout'') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
......@@ -221,7 +219,7 @@ Section MSQueue.
iMod (ghost_var_update _ (Lout ++ [(l', v)]) with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iDestruct (own_lat_auth_max _ _ with "[Hγp● Hγp◯]") as %Hpre. iFrame.
apply prefix_app_inv in Hpre. apply non_nil_prefix in Hpre as [L'' [H1 H2]]. subst Lin'.
iDestruct "Hr" as (dn ln) "(Hh & Hd & (Hl' & Hd' & Pv) & HInv)".
iDestruct "Hr" as (dn) "(Hh & Hd & Hd' & Pv & HInv)".
iMod ("Hclose" with "[Hh HInv Hhq Htq Hγc● Hγp●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v)]). iFrame. iExists L''.
replace ((l', v) :: L'') with ([(l', v)] ++ L'') by done. rewrite app_assoc.
......
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