Commit fb37b170 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

changes in inv

parent 5bceb320
......@@ -79,7 +79,7 @@ Section MSQueue.
(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' γ))
(iTok γ (l (#next_link, #v) P(v) own γc ( (Excl' γ')))) (queue_inv l t γc γ' L')
(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 Σ :=
......@@ -214,13 +214,13 @@ Section MSQueue.
{ iNext. iExists h, h. iFrame. iExists nil, γ, d. iFrame. done. }
iModIntro. wp_proj.
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 "Hr" as (d l'' γ') "(>Hh & >Hγc● & HTrade)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %<-.
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γ'c●)".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ HL']") as "_".
iDestruct "Hl'" as "(Hl' & Pv & Hγ'c● & HL')".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ]") as "_".
{ iNext. iExists h, t. iFrame. iExists ((l', v) :: L'), γ, d, l'', γ'. iFrame. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if.
......@@ -231,9 +231,9 @@ Section MSQueue.
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. }
iMod ("Hclose" with "[Hhq Htq HL HL']") as "_".
{ iNext. iExists l', t'. iFrame. iExists L', γ'. iFrame.
destruct L as [|(l',v) L'] eqn:HL. }
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