Commit a8d7b804 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Deq spec done

parent 3a6db102
......@@ -90,8 +90,8 @@ 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)) (γ: gname),
q {1/2} #h own γc ( (Excl' (Lout, γ))) own γm ( (ListSome (Lout ++ Lin))) iTok γ)%I.
( (h: loc) (Lout: list (loc * Z * gname)) (γ: gname),
q {1/2} #h own γc ( (Excl' (Lout, γ))) iTok γ)%I.
Definition Producer (q: loc): iProp Σ := ( (t: loc), (q + 1) {1/2} #t)%I.
Lemma newQueue_spec:
......@@ -116,7 +116,7 @@ Section MSQueue.
iExists γc, γm.
iSplitL "Hinv". iExists q. eauto.
iSplitL "Htp". iExists l. iFrame.
iExists l, nil, nil, γ. iFrame.
iExists l, nil, γ. iFrame.
Qed.
(*Lemma findTail_spec q γc:
......@@ -162,13 +162,6 @@ Section MSQueue.
wp_alloc n as "Hn". wp_let.
wp_load; wp_proj; wp_store.
wp_op. wp_load. 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.
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.
......@@ -189,26 +182,24 @@ Section MSQueue.
intros. iIntros "(#Hq & Hc) Post".
wp_lam. wp_op. rewrite loc_add_0.
iDestruct "Hq" as (l ->) "#Hinv".
iDestruct "Hc" as (h Lout Lin s) "(Hhc & Hγc◯ & Hγm◯ & Hγ)".
iDestruct "Hc" as (h Lout s) "(Hhc & Hγc◯ & Hγ)".
wp_bind (!#l)%E.
wp_load.
wp_let. wp_bind (!#h)%E.
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.
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● 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.
wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, Lout, s. iFrame. by iLeft.
- iDestruct "Hr" as (d l'') "(>Hh & HTrade & Hr)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H.
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◯]".
(* iMod (ghost_var_update _ (Lout, γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)". *)
wp_load.
iCombine "Hγ" "HTrade" as "HTrade". rewrite bi.sep_or_l.
rewrite unit_tok_exclusive. iDestruct "HTrade" as "[HF|[Hγ Hl']]"; try done.
......@@ -220,22 +211,30 @@ Section MSQueue.
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".
iDestruct "HL" as (Lin'') "(>Hγm● & Hr)".
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_store.
iDestruct "Hh" as "(Hhc & Hhq)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %H.
inversion H. rewrite <- H2. clear H. clear H1. clear H2.
iMod (ghost_var_update _ (Lout ++ [(l', v, γ')], γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iRename "Hγm◯" into "H".
iMod (own_lat_auth_update _ _ _ (Lout ++ [(l', v, γ')] ++ Lin'') _ with "Hγm●") as "[Hγm● Hγm◯]".
iDestruct (own_lat_auth_max _ _ with "[Hγm● H]") as %Hpre. iFrame.
iMod ("Hclose" with "[Hhq Htq Hr Hγc● Hγm●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists Lin''. rewrite app_assoc. iFrame. }
iDestruct (own_lat_auth_max _ _ with "[Hγm● Hγm◯]") as %Hpre. iFrame.
apply prefix_app_inv in Hpre.
assert (L'', Lin' = (l', v, γ') :: L'' L' `prefix_of` L'') as [L'' [H1 H2]].
{ inversion Hpre. replace ((l', v, γ') :: L') with ([(l', v, γ')] ++ L') in H by done.
rewrite <- app_assoc in H. exists (L' ++ x).
replace ([(l', v, γ')] ++ L' ++ x) with ((l', v, γ') :: L' ++ x) in H by done.
split. assumption. exists x. done. } subst Lin'.
simpl. iMod ("Hclose" with "[Hhq Htq Hr Hγc● Hγm●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists L''.
replace ((l', v, γ') :: L'') with ([(l', v, γ')] ++ L'') by done. rewrite app_assoc.
iDestruct "Hr" as (d' l''') "(Hh & HTrade & Hqinv)". iFrame. }
iModIntro. wp_seq. wp_load. wp_proj.
iApply "Post".
iSplitR "Pv".
+ iExists l', (Lout ++ [(l', v, γ')]), L', γ'. iFrame. admit.
+ iExists l', (Lout ++ [(l', v, γ')]), γ'. iFrame.
+ by iRight.
Admitted.
Qed.
End proof.
End MSQueue.
......
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