Commit 917d7705 authored by Ralf Jung's avatar Ralf Jung

bump Iris for CmpXchg change, and port everyting

parent 4223390a
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-06-20.3.4f0c1046") | (= "dev") }
"coq-iris" { (= "dev.2019-06-24.3.5ef58527") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -111,23 +111,23 @@ Section stacks.
wp_load.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro. wp_let. wp_alloc ' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iModIntro. wp_let. wp_alloc ' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ('' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
destruct (decide (v' = v'')) as [->|Hne].
- wp_cas_suc. { destruct v''; left; done. }
- wp_cmpxchg_suc. { destruct v''; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (Some '); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
wp_if.
wp_pures.
by iApply "HΦ".
- wp_cas_fail.
- wp_cmpxchg_fail.
{ destruct v', v''; simpl; congruence. }
{ destruct v''; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HP HΦ").
Qed.
......@@ -153,25 +153,25 @@ Section stacks.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
wp_pures. wp_bind (CAS _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ('' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
destruct (decide (v'' = (Some l))) as [-> |].
* rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
simpl.
wp_cas_suc.
wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
* wp_cas_fail. { destruct v''; simpl; congruence. }
* wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HΦ").
Qed.
End stacks.
......
......@@ -97,22 +97,22 @@ Section side_channel.
{{{ v', RET v'; ( v'' : val, v' = InjRV v'' P v'') v' = InjLV #() }}}.
Proof.
iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
wp_lam. wp_bind (CAS _ _ _). wp_pures.
wp_lam. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iRight; iRight; iFrame. }
iModIntro.
wp_pures.
by iApply "HΦ"; iLeft; iExists _; iSplit.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[H]") as "_".
{ iRight; iLeft; auto. }
iModIntro.
wp_pures.
by iApply "HΦ"; iRight.
- wp_cas_fail.
- wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
Qed.
......@@ -123,22 +123,22 @@ Section side_channel.
{{{ v', RET v'; ( v'' : val, v' = InjRV v'' P v'') v' = InjLV #() }}}.
Proof.
iIntros (Φ) "H HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
wp_lam. wp_proj. wp_bind (CAS _ _ _).
wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
iInv N as "Hstages" "Hclose".
iDestruct "Hstages" as "[[H HP] | [H | [Hl Hγ]]]".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hclose" with "[H]") as "_".
{ by iRight; iLeft. }
iModIntro.
wp_pures.
iApply "HΦ"; iLeft; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[H]") as "_".
{ by iRight; iLeft. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
......@@ -326,23 +326,23 @@ Section stack_works.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (list) "(Hl & Hlist)" "Hclose".
destruct (decide (v'' = list)) as [ -> |].
* wp_cas_suc. { destruct list; left; done. }
* wp_cmpxchg_suc. { destruct list; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists (Some _); iFrame.
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
wp_if.
wp_pures.
by iApply "HΦ".
* wp_cas_fail.
* wp_cmpxchg_fail.
{ destruct list, v''; simpl; congruence. }
{ destruct list; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HP HΦ").
- wp_match.
by iApply "HΦ".
......@@ -373,24 +373,24 @@ Section stack_works.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as (v'') "[Hl Hlist]" "Hclose".
destruct (decide (v'' = Some list)) as [-> |].
+ rewrite is_list_unfold.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
wp_cas_suc.
wp_cmpxchg_suc.
iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+ wp_cas_fail. { destruct v''; simpl; congruence. }
+ wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HΦ").
- iDestruct "HSome" as (v) "[-> HP]".
wp_pures.
......
......@@ -118,23 +118,23 @@ Section stack_works.
{ iNext; iExists _, _; iFrame. }
clear xs.
iModIntro.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
- wp_cas_suc. { destruct list'; left; done. }
- wp_cmpxchg_suc. { destruct list'; left; done. }
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_if.
wp_pures.
by iApply ("HΦ" with "HΨ").
- wp_cas_fail.
- wp_cmpxchg_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "Hupd HΦ").
Qed.
......@@ -172,10 +172,10 @@ Section stack_works.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
* wp_cas_suc.
* wp_cmpxchg_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
iDestruct "Hupd" as "[Hupdcons _]".
......@@ -188,11 +188,11 @@ Section stack_works.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
* wp_cas_fail. { destruct v'; simpl; congruence. }
* wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "Hupd HΦ").
Qed.
End stack_works.
......
......@@ -119,24 +119,24 @@ Section proofs.
{{{ v', RET v'; ( v'' : val, v' = InjRV v'' can_push P Q v'') (v' = InjLV #() (Q #())) }}}.
Proof.
iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
wp_lam. wp_pures. wp_bind (CAS _ _ _).
wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nside_channel as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext; iRight; iRight; iFrame. }
iModIntro.
wp_pures.
by iApply "HΦ"; iLeft; iExists _; iFrame.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext; iRight; iRight; iLeft; iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HQ]"); iRight; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
- wp_cas_fail.
- wp_cmpxchg_fail.
iDestruct (own_valid_2 with "H Hγ") as %[].
Qed.
......@@ -149,11 +149,11 @@ Section proofs.
( v'' : val, v' = InjRV v'' Ψ v') (v' = InjLV #() (do_pop Q')) }}}.
Proof.
simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
wp_lam. wp_proj. wp_bind (CAS _ _ _).
wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
iInv Nside_channel as "Hstages" "Hclose".
iDestruct "Hstages" as "[[Hl Hpush] | [[Hl HQ] | [[Hl Hγ] | [Hl Hγ]]]]".
- iMod "Hopener" as (xs) "[HP Hcloser]".
wp_cas_suc.
wp_cmpxchg_suc.
iMod ("Hpush" with "HP") as "[HP HQ]".
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hcloser" with "HP") as "_".
......@@ -162,19 +162,19 @@ Section proofs.
iApply fupd_intro_mask; first done.
wp_pures.
iApply "HΦ"; iLeft; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl HQ]") as "_".
{ iRight; iLeft; iFrame. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
wp_pures.
iApply "HΦ"; auto.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hl Hγ]").
{ iRight; iRight; iFrame. }
iModIntro.
......@@ -350,25 +350,25 @@ Section proofs.
{ iNext; iExists _, _; iFrame. }
clear xs.
iModIntro.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
destruct (decide (list = list')) as [ -> |].
* wp_cas_suc. { destruct list'; left; done. }
* wp_cmpxchg_suc. { destruct list'; left; done. }
iMod (fupd_intro_mask' ( Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_if.
wp_pures.
by iApply ("HΦ" with "HΨ").
* wp_cas_fail.
* wp_cmpxchg_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HΦ Hupd").
- wp_match. iApply ("HΦ" with "HΨ").
Qed.
......@@ -426,10 +426,10 @@ Section proofs.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
wp_pures. wp_bind (CAS _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (Some l'))) as [ -> |].
+ wp_cas_suc.
+ wp_cmpxchg_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
iMod (fupd_intro_mask' ( Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
......@@ -444,7 +444,7 @@ Section proofs.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
+ wp_cas_fail. { destruct v'; simpl; congruence. }
+ wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
......
......@@ -162,21 +162,21 @@ Section proof.
{ iNext. iExists _,_. iFrame. } clear ls.
iModIntro.
wp_alloc n as "Hn".
wp_pures. wp_bind (CAS _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
destruct (decide (o = o')) as [->|?].
- wp_cas_suc. { destruct o'; left; done. }
- wp_cmpxchg_suc. { destruct o'; left; done. }
iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
{ iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
simpl. iExists _. iFrame. by iExists 1%Qp. }
iModIntro. wp_if_true. by iApply "HΦ".
- wp_cas_fail.
iModIntro. wp_pures. by iApply "HΦ".
- wp_cmpxchg_fail.
{ destruct o, o'; simpl; congruence. }
{ destruct o'; left; done. }
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,ls. by iFrame "Ho Hb". }
iModIntro. wp_if_false.
iModIntro. wp_proj. wp_if.
by iApply ("IH" with "HP [HΦ]").
Qed.
......@@ -214,11 +214,11 @@ Section proof.
iExists _; eauto. by iFrame. }
iModIntro. repeat wp_pure _.
iDestruct "Hhd'" as (q) "Hhd".
wp_load. repeat wp_pure _.
wp_bind (CAS _ _ _).
wp_load. wp_pures.
wp_bind (CmpXchg _ _ _).
iInv N as (o' ls') "[Ho [Hls >Hb]]" "Hcl".
destruct (decide (o' = (Some hd))) as [->|?].
+ wp_cas_suc.
+ wp_cmpxchg_suc.
(* The list is still the same *)
rewrite (is_list_duplicate tl). iDestruct "Hls'" as "[Hls' Htl]".
iAssert (is_list (Some hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
......@@ -230,10 +230,10 @@ Section proof.
iMod ("Hcl" with "[Ho Htl Hb]") as "_".
{ iNext. iExists _,ls. by iFrame "Ho Hb". }
iModIntro. wp_pures. by iApply "HΦ".
+ wp_cas_fail. { destruct o'; simpl; congruence. }
+ wp_cmpxchg_fail. { destruct o'; simpl; congruence. }
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,ls'. by iFrame "Ho Hb". }
iModIntro. wp_if_false.
iModIntro. wp_proj. wp_if.
by iApply ("IH" with "HP [HΦ]").
Qed.
End proof.
......
......@@ -316,10 +316,10 @@ Section monotone_counter.
{ iNext; iExists m; iFrame. }
iModIntro.
wp_let; wp_op; wp_let.
wp_bind (CAS _ _ _)%E.
wp_bind (CmpXchg _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
+ wp_cas_suc.
+ wp_cmpxchg_suc.
(* If the CAS succeeds we need to update our ghost state. This is achieved using the own_update rule/lemma.
The arguments are the ghost name and the ghost resources x from which and to which we are updating.
Finally we need to give up own γ x to get ownership of the new resources.
......@@ -332,12 +332,12 @@ Section monotone_counter.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
iModIntro; wp_pures; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
+ wp_cas_fail; first intros ?; simplify_eq.
+ wp_cmpxchg_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
- iExists k; iFrame.
- iModIntro; wp_if.
- iModIntro. wp_proj. wp_if.
iApply ("IH" with "HOwnFrag HCont"); iFrame.
Qed.
End monotone_counter.
......@@ -501,22 +501,22 @@ Section monotone_counter'.
{ iNext; iExists m; iFrame. }
iModIntro.
wp_let; wp_op; wp_let.
wp_bind (CAS _ _ _)%E.
wp_bind (CmpXchg _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
+ wp_cas_suc.
+ wp_cmpxchg_suc.
iMod (own_update γ (( m n)) ( (S m : mnatUR) ( (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
{ apply mcounterRA_update'. }
{ rewrite own_op; iFrame. }
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
iModIntro; wp_pures; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
+ wp_cas_fail; first intros ?; simplify_eq.
+ wp_cmpxchg_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
- iExists k; iFrame.
- iModIntro; wp_if.
- iModIntro. wp_proj. wp_if.
iApply ("IH" with "HOwnFrag HCont"); iFrame.
Qed.
End monotone_counter'.
......@@ -621,16 +621,16 @@ Section ccounter.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hpt]" "Hclose".
wp_load. iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op. wp_let.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hpt]" "Hclose".
wp_bind (CmpXchg _ _ _). iInv N as (c') ">[Hγ Hpt]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hown") as "[Hγ Hown]".
{ apply ccounterRA_update. } (* We use the update lemma for our RA. *)
wp_cas_suc. iMod ("Hclose" with "[Hpt Hγ]") as "_".
wp_cmpxchg_suc. iMod ("Hclose" with "[Hpt Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. iApply "HΦ". by iFrame "Hinv".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iModIntro. wp_pures. iApply "HΦ". by iFrame "Hinv".
- wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hown] [HΦ]"); auto.
iModIntro. wp_pures. by iApply ("IH" with "[Hown] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ q n :
......
......@@ -94,17 +94,19 @@ Section lock_spec.
iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
iLöb as "IH".
wp_rec.
wp_bind (CAS _ _ _).
wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iApply "Hcont".
iFrame.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iApply ("IH" with "[$Hcont]").
Qed.
......@@ -129,4 +131,4 @@ End lock_spec.
Typeclasses Opaque locked.
Global Opaque locked.
Typeclasses Opaque is_lock.
Global Opaque is_lock.
\ No newline at end of file
Global Opaque is_lock.
......@@ -109,17 +109,19 @@ Section lock_spec.
iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
iLöb as "IH".
wp_rec.
wp_bind (CAS _ _ _).
wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iApply "Hcont".
iFrame.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iApply ("IH" with "[$Hcont]").
Qed.
......@@ -167,16 +169,18 @@ Section lock_spec.
iIntros (HE) "#Hi"; rewrite /acquire.
iLöb as "IH".
wp_rec.
wp_bind (CAS _ _ _).
wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iFrame.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
wp_if.
iApply "IH".
Qed.
......
......@@ -169,21 +169,21 @@ Section cnt_spec.
iModIntro.
wp_let.
wp_op.
wp_bind (CAS _ _ _)%E.
wp_bind (CmpXchg _ _ _)%E.
iInv (N .@ "internal") as (m') "[>Hpt >Hown]" "HClose".
destruct (decide (m = m')); simplify_eq.
- wp_cas_suc.
- wp_cmpxchg_suc.
iMod ("HVS" $! m' with "[Hown HP]") as "[Hown HQ]"; first iFrame.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply "HCont"; by iFrame.
- wp_cas_fail.
- wp_cmpxchg_fail.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
wp_if.
wp_pures.
iApply ("IH" with "HP HCont").
Qed.
......
......@@ -23,7 +23,7 @@ Definition new_counter : val :=
(*
complete(c, f, x, n, p) :=
Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
Resolve CmpXchg(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
*)
Definition complete : val :=
λ: "c" "f" "x" "n" "p",
......@@ -31,7 +31,7 @@ Definition complete : val :=
(* Compare with #true to make this a total operation that never
gets stuck, no matter the value stored in [f]. *)
let: "new_n" := if: !"f" = #true then "n" + #1 else "n" in
Resolve (CAS "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
Resolve (CmpXchg "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
(*
get c :=
......@@ -131,7 +131,7 @@ Section conditional_counter.
Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
match vs with
| (#true , LitV (LitLoc l)) :: _ => Some l
| ((_, #true)%V, LitV (LitLoc l)) :: _ => Some l
| _ :: vs => val_to_some_loc vs
| _ => None
end.
......@@ -161,12 +161,12 @@ Section conditional_counter.
Definition accepted_state Q (proph_winner : option loc) (l_ghost_winner : loc) :=
(l_ghost_winner {1/2} - match proph_winner with None => True | Some l => l = l_ghost_winner Q end)%I.
(* The same thread then wins the CAS and moves from [accepted] to [done].
(* The same thread then wins the CmpXchg and moves from [accepted] to [done].
Then, the [γ_t] token guards the transition to take out [Q].
Remember that the thread winning the CAS might be just helping. The token
Remember that the thread winning the CmpXchg might be just helping. The token
is owned by the thread whose request this is.
In this state, [l_ghost_winner] serves as a token to make sure that
only the CAS winner can transition to here, and owning half of[l] serves as a
only the CmpXchg winner can transition to here, and owning half of[l] serves as a
"location" token to ensure there is no ABA going on. Notice how [counter_inv]
owns *more than* half of its [l], which means we know that the [l] there
and here cannot be the same. *)
......@@ -264,7 +264,7 @@ Section conditional_counter.
((own_token γ_t ={}= Q) - Φ #()) -
own γ_n ( Excl' n) -
l_new InjLV #n -
WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
WP Resolve (CmpXchg #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros "#InvC #InvS Hl_ghost HQ Hn● [Hl_new Hl_new']". wp_bind (Resolve _ _ _)%E.
iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
......@@ -286,9 +286,9 @@ Section conditional_counter.
while a [state] protocol is not [done], it owns enough of
the [counter] protocol to ensure that does not move anywhere else. *)
iDestruct (mapsto_agree with "Hc Hc'") as %[= ->].
(* We perform the CAS. *)
(* We perform the CmpXchg. *)
iCombine "Hc Hc'" as "Hc".