Commit c201286c authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

some changes and adding gamma to tuppple

parent bcd51c6c
......@@ -44,9 +44,9 @@ Section MSQueue.
λ: "q" "x",
let: "n" := Alloc (Pair #0 #0) in
"n" <- (link "n", "x") ;;
let: "t" := ("q" + #tail) (*getTail "q"*) in
if: (CAS (link "t") #0 ("n"))
then ("q" + #tail) <- "n" ;; #1
let: "t" := !("q" + #tail) in
if: link "t" = #0
then "t" <- ("n", data "t");; ("q" + #tail) <- "n" ;; #1
else #0.
Definition tryDeq : val :=
......@@ -61,8 +61,9 @@ Section MSQueue.
else #0.
Section proof.
Definition my_master_camera := (authR (@lpUR (loc * Z) _ _ _ _)).
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO locO ZO)) gnameO)))).
(* Typeclasses eauto := debug. *)
Definition my_master_camera := (authR (@lpUR (loc * Z * gname) _ _ _ _)).
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO (prodO locO ZO) gnameO)) gnameO)))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_master_camera, !inG Σ my_camera}.
Context (P : Z iProp Σ).
......@@ -77,18 +78,17 @@ Section MSQueue.
Qed.
Fixpoint queue_inv (h t: loc) (γ: gname) (L: list (loc * Z)): iProp Σ :=
Fixpoint queue_inv (h t: loc) (γ: gname) (L: list (loc * Z * gname)): 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)
| (l, v, γ') :: L' => dummy next_link, h (#l, #dummy)
(iTok γ (l (#next_link, #v) P(v) iTok γ')) (queue_inv l t γ' L')
end)%I.
(*Typeclasses eauto := debug.*)
Definition queue_inv_s (q: loc) (γc γm: gname): iProp Σ :=
( (h t: loc) (Lout: list (loc * Z)) (γ: gname),
( (h t: loc) (Lout: list (loc * Z * gname)) (γ: gname),
q {1/2} #h (q + 1) {1/2} #t own γc ( (Excl' (Lout, γ)))
( (Lin: list (loc * Z)),
( (Lin: list (loc * Z * gname)),
own γm ( (ListSome (Lout ++ Lin))) queue_inv h t γ Lin)
)%I.
......@@ -97,7 +97,7 @@ Section MSQueue.
( q: loc, l = q inv queueN (queue_inv_s q γc γm))%I.
Definition Consumer (q: loc) (γc γm: gname): iProp Σ :=
( (h: loc) (Lout Lin: list (loc * Z)) (γ: gname),
( (h: loc) (Lout Lin: list (loc * Z * gname)) (γ: 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.
......@@ -181,17 +181,20 @@ Section MSQueue.
iApply "Post". done.
Qed.*)*)
Instance inhabited_base_lit : Inhabited base_lit := populate (LitUnit).
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.
intros. iIntros "(#Hq & Hp & P) Post".
(* iDestruct "Hq" as (γ l) "(Hq & Hl & Tok)". *)
iDestruct "Hq" as (l ->) "#Hinv".
iDestruct "Hp" as (t) "Htp".
wp_lam. wp_let.
wp_alloc n as "Hn". wp_let.
wp_load; wp_proj; wp_store.
wp_op. wp_let.
wp_op. wp_load. wp_let.
(*wp_rec.
wp_bind ((rec: "getTail" "q" := _) #q)%V.
wp_rec.
......@@ -199,6 +202,16 @@ Section MSQueue.
iApply (findTail_spec q with "[Hq Hp]"). iFrame. done.
iNext. iIntros (t) "_".
wp_let.*)
wp_bind (!#t)%E.
iInv queueN as (h t' Lout γ) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Htp Htq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (Lin) "(>Hγm● & Hr)".
destruct Lin as [|((l',v), γ') L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% Ht]". subst h.
wp_load.
iMod ("Hclose" with "[Hhq Htq Ht Hγc● Hγm●]") as "_".
{ iNext. iExists _, _, _, _. iFrame. iExists _. iFrame. iExists _. iFrame. done. }
iModIntro. wp_proj. wp_op. wp_if. wp_store.
Admitted.
Lemma prefix_app_inv : (A : Type) (l l1 l2 : list A),
......@@ -206,8 +219,6 @@ Section MSQueue.
Proof.
intros. inversion H. Admitted.
Instance inhabited_base_lit : Inhabited base_lit := populate (LitUnit).
Lemma tryDeq_spec q γc γm:
{{{ Queue q γc γm Consumer q γc γm }}}
tryDeq #q
......@@ -223,16 +234,16 @@ Section MSQueue.
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 (Lin') "(>Hγm● & Hr)".
destruct Lin' as [|(l',v) L'] eqn:HL.
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● 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, Lout, Lin, s. iFrame. by iLeft.
- iDestruct "Hr" as (d l'' γ') "(>Hh & HTrade & Hr)".
- iDestruct "Hr" as (d l'') "(>Hh & HTrade & Hr)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H.
inversion H. rewrite <- H2.
inversion H. rewrite <- H2. clear H. clear H1. clear H2.
iClear "Hγm◯".
iMod (own_lat_auth_update_fork _ _ _ with "Hγm●") as "[Hγm● Hγm◯]".
wp_load.
......@@ -240,7 +251,7 @@ Section MSQueue.
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γm● Hγ Hr]") as "_".
{ iNext. iExists h, t, Lout, γ. iFrame. iExists ((l', v) :: L'). iFrame. iExists d, l', γ'. iFrame. }
{ 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.
......@@ -250,14 +261,10 @@ Section MSQueue.
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 %H.
inversion H. rewrite <- H2.
iMod (ghost_var_update _ (Lout ++ [(l', v, γ')], γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
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 }
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists Lin''. 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