...
 
Commits (3)
...@@ -115,6 +115,7 @@ theories/heap_lang/lib/lazy_coin.v ...@@ -115,6 +115,7 @@ theories/heap_lang/lib/lazy_coin.v
theories/heap_lang/lib/counter.v theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v theories/heap_lang/lib/increment.v
theories/heap_lang/lib/compare_and_set.v
theories/proofmode/base.v theories/proofmode/base.v
theories/proofmode/tokens.v theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v theories/proofmode/coq_tactics.v
......
...@@ -8,38 +8,10 @@ Section tests. ...@@ -8,38 +8,10 @@ Section tests.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ. Implicit Types Φ : val iProp Σ.
Definition CAS_resolve e1 e2 e3 p v :=
Resolve (CAS e1 e2 e3) p v.
Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
vals_cas_compare_safe v1 v1
{{{ proph p vs l v1 }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #true ; vs', vs = (#true, v)::vs' proph p vs' l v2 }}}.
Proof.
iIntros (Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
wp_cas_suc. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
{{{ proph p vs l v' }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #false ; vs', vs = (#false, v)::vs' proph p vs' l v' }}}.
Proof.
iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
wp_cas_fail. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) : Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
l #n - l #n -
proph p vs - proph p vs -
WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, v = #true vs, proph p vs l #(n+1) }}%I. WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, v = #n vs, proph p vs l #(n+1) }}%I.
Proof. Proof.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done. iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame. wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
......
...@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0. ...@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := Definition incr : val :=
rec: "incr" "l" := rec: "incr" "l" :=
let: "n" := !"l" in let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l".
Definition read : val := λ: "l", !"l". Definition read : val := λ: "l", !"l".
(** The CMRA we need. *) (** The CMRA we need. *)
...@@ -231,10 +231,11 @@ Section counter_proof. ...@@ -231,10 +231,11 @@ Section counter_proof.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]". rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iSplitL "Hl Hγ". wp_cas_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. rewrite {3}/C; eauto 10. wp_op. rewrite bool_decide_true //. wp_if. rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega). - assert (#c #c') by (intros [=]; abstract omega). wp_cas_fail.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10. wp_op. rewrite bool_decide_false //. wp_if.
iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed. Qed.
Check "read_spec". Check "read_spec".
......
...@@ -9,7 +9,7 @@ Set Default Proof Using "Type". ...@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in ( let: "x" := ref NONE in (
(* tryset *) (λ: "n", (* tryset *) (λ: "n",
CAS "x" NONE (SOME "n")), CAS "x" NONE (SOME "n") = NONE),
(* check *) (λ: <>, (* check *) (λ: <>,
let: "y" := !"x" in λ: <>, let: "y" := !"x" in λ: <>,
match: "y" with match: "y" with
...@@ -49,13 +49,15 @@ Proof. ...@@ -49,13 +49,15 @@ Proof.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN". iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". } { iNext. iLeft. by iSplitL "Hl". }
wp_pures. iModIntro. iApply "Hf"; iSplit. wp_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures. - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CAS _ _ _).
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]". iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ iMod (own_update with "Hγ") as "Hγ". + iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). } { by apply cmra_update_exclusive with (y:=Shot n). }
wp_cas_suc. iSplitL; last eauto. wp_cas_suc. iSplitL; iModIntro; last first.
iModIntro. iNext; iRight; iExists n; by iFrame. { wp_pures. eauto. }
+ wp_cas_fail. iSplitL; last eauto. iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; iModIntro; last first.
{ wp_pures. eauto. }
rewrite /one_shot_inv; eauto 10. rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E. - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ". iInv N as ">Hγ".
......
...@@ -97,8 +97,8 @@ Inductive expr := ...@@ -97,8 +97,8 @@ Inductive expr :=
| AllocN (e1 e2 : expr) (* array length (positive number), initial value *) | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
| Load (e : expr) | Load (e : expr)
| Store (e1 : expr) (e2 : expr) | Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr) | CAS (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-and-swap (NOT compare-and-set!) *)
| FAA (e1 : expr) (e2 : expr) | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
(* Prophecy *) (* Prophecy *)
| NewProph | NewProph
| Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *) | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
...@@ -518,6 +518,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := ...@@ -518,6 +518,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then if decide (op = EqOp) then
(* Crucially, this compares the same way as [CAS]! *)
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2) Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
else else
match v1, v2 with match v1, v2 with
...@@ -633,19 +634,13 @@ Inductive head_step : expr → state → list observation → expr → state → ...@@ -633,19 +634,13 @@ Inductive head_step : expr → state → list observation → expr → state →
[] []
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ) (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[] []
| CasFailS l v1 v2 vl σ : | CasS l v1 v2 vl σ :
vals_cas_compare_safe vl v1 vals_cas_compare_safe vl v1
σ.(heap) !! l = Some vl σ.(heap) !! l = Some vl
val_for_compare vl val_for_compare v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
(Val $ LitV $ LitBool false) σ []
| CasSucS l v1 v2 vl σ :
vals_cas_compare_safe vl v1
σ.(heap) !! l = Some vl
val_for_compare vl = val_for_compare v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[] []
(Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ) (* Crucially, this compares the same way as [EqOp]! *)
(Val vl) (if decide (val_for_compare vl = val_for_compare v1) then state_upd_heap <[l:=v2]> σ else σ)
[] []
| FaaS l i1 i2 σ : | FaaS l i1 i2 σ :
σ.(heap) !! l = Some (LitV (LitInt i1)) σ.(heap) !! l = Some (LitV (LitInt i1))
......
...@@ -36,7 +36,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -36,7 +36,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
val_is_unboxed w1 val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l w1 w2 @ <<< v, mapsto l 1 v >>> cas #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v, <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>; RET v >>>;
}. }.
Arguments atomic_heap _ {_}. Arguments atomic_heap _ {_}.
...@@ -100,7 +100,7 @@ Section proof. ...@@ -100,7 +100,7 @@ Section proof.
<<< (v : val), l v >>> <<< (v : val), l v >>>
primitive_cas #l w1 w2 @ primitive_cas #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then l w2 else l v, <<< if decide (val_for_compare v = val_for_compare w1) then l w2 else l v,
RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>. RET v >>>.
Proof. Proof.
iIntros (? Φ) "AU". wp_lam. wp_let. wp_let. iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]". iMod "AU" as (v) "[H↦ [_ Hclose]]".
......
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(* Defines compare-and-set (CASet) on top of compare-and-swap (CAS). *)
Definition compare_and_set : val :=
λ: "l" "v1" "v2", CAS "l" "v1" "v2" = "v1".
Section proof.
Context `{!heapG Σ}.
(* This is basically a logically atomic spec, but stronger and hence easier to apply. *)
Lemma caset_spec (l : loc) (v1 v2 : val) Φ E :
val_is_unboxed v1
(|={,E}=> v, l v let b := bool_decide (val_for_compare v = val_for_compare v1) in
(l (if b then v2 else v) ={E,}= Φ #b) ) -
WP compare_and_set #l v1 v2 @ {{ Φ }}.
Proof.
iIntros (?) "AU". wp_lam. wp_pures. wp_bind (CAS _ _ _).
iMod "AU" as (v) "[H↦ Hclose]". case_bool_decide.
- wp_cas_suc. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
rewrite bool_decide_true //.
- wp_cas_fail. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
rewrite bool_decide_false //.
Qed.
End proof.
...@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants. ...@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth. From iris.algebra Require Import frac_auth auth.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0. Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" := Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". if: compare_and_set "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l". Definition read : val := λ: "l", !"l".
(** Monotone counter *) (** Monotone counter *)
...@@ -50,22 +50,25 @@ Section mono_proof. ...@@ -50,22 +50,25 @@ Section mono_proof.
iDestruct "Hl" as (γ) "[#? Hγf]". iDestruct "Hl" as (γ) "[#? Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]". wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures. wp_pures. wp_apply caset_spec; first done.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]". iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|]. destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf") - iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_both_valid. as %[?%mnat_included _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. } { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iModIntro. iSplitL "Hl Hγ". iExists _; iFrame "Hl". iIntros "!> Hl".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto. { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. iFrame. }
iModIntro. wp_if.
iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). iApply (own_mono with "Hγf").
(* FIXME: FIXME(Coq #6294): needs new unification *) (* FIXME: FIXME(Coq #6294): needs new unification *)
apply: auth_frag_mono. by apply mnat_included, le_n_S. apply: auth_frag_mono. by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro. - iExists _; iFrame "Hl". iIntros "!> Hl".
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10. rewrite {3}/mcounter; eauto 10.
Qed. Qed.
...@@ -129,17 +132,19 @@ Section contrib_spec. ...@@ -129,17 +132,19 @@ Section contrib_spec.
iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec. iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]". wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures. wp_pures. wp_apply caset_spec; first done.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]". iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|]. destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. } { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
wp_cas_suc. iModIntro. iSplitL "Hl Hγ". iExists _; iFrame "Hl". iIntros "!> Hl".
rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. by iApply "HΦ". iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). - iExists _; iFrame "Hl". iIntros "!> Hl".
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto. iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed. Qed.
Lemma read_contrib_spec γ l q n : Lemma read_contrib_spec γ l q n :
......
...@@ -16,7 +16,7 @@ Section increment_physical. ...@@ -16,7 +16,7 @@ Section increment_physical.
Definition incr_phy : val := Definition incr_phy : val :=
rec: "incr" "l" := rec: "incr" "l" :=
let: "oldv" := !"l" in let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1) if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
then "oldv" (* return old value if success *) then "oldv" (* return old value if success *)
else "incr" "l". else "incr" "l".
...@@ -29,9 +29,9 @@ Section increment_physical. ...@@ -29,9 +29,9 @@ Section increment_physical.
wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]". wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
destruct (decide (#v = #w)) as [[= ->]|Hx]. destruct (decide (#v = #w)) as [[= ->]|Hx].
- wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iModIntro. wp_if. done. iModIntro. wp_op. rewrite bool_decide_true //. wp_if. done.
- wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iModIntro. wp_if. iApply "IH". done. iModIntro. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
Qed. Qed.
End increment_physical. End increment_physical.
...@@ -45,7 +45,7 @@ Section increment. ...@@ -45,7 +45,7 @@ Section increment.
Definition incr : val := Definition incr : val :=
rec: "incr" "l" := rec: "incr" "l" :=
let: "oldv" := !"l" in let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1) if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
then "oldv" (* return old value if success *) then "oldv" (* return old value if success *)
else "incr" "l". else "incr" "l".
...@@ -70,9 +70,9 @@ Section increment. ...@@ -70,9 +70,9 @@ Section increment.
{ (* abort case *) iDestruct "Hclose" as "[? _]". done. } { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx]. iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iIntros "!>". wp_if. by iApply "HΦ". iIntros "!>". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
- iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iIntros "!>". wp_if. iApply "IH". done. iIntros "!>". wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
Qed. Qed.
(** A proof of the incr specification that uses lemmas to avoid reasining (** A proof of the incr specification that uses lemmas to avoid reasining
...@@ -94,9 +94,9 @@ Section increment. ...@@ -94,9 +94,9 @@ Section increment.
iIntros "H↦ !>". iIntros "H↦ !>".
simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx]. simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !>". - iRight. iFrame. iIntros "HΦ !>".
wp_if. by iApply "HΦ". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !>". - iLeft. iFrame. iIntros "AU !>".
wp_if. iApply "IH". done. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
Qed. Qed.
(** A "weak increment": assumes that there is no race *) (** A "weak increment": assumes that there is no race *)
......
...@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock. ...@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false. Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true. Definition try_acquire : val := λ: "l", CAS "l" #false #true = #false.
Definition acquire : val := Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l". rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false. Definition release : val := λ: "l", "l" <- #false.
...@@ -61,12 +61,12 @@ Section proof. ...@@ -61,12 +61,12 @@ Section proof.
{{{ b, RET #b; if b is true then locked γ R else True }}}. {{{ b, RET #b; if b is true then locked γ R else True }}}.
Proof. Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv". iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]". wp_rec. wp_bind (CAS _ _ _). iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto). - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
iApply ("HΦ" $! false). done. wp_pures. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]". - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto). iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]"). rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed. Qed.
Lemma acquire_spec γ lk R : Lemma acquire_spec γ lk R :
......
...@@ -20,7 +20,7 @@ Definition newlock : val := ...@@ -20,7 +20,7 @@ Definition newlock : val :=
Definition acquire : val := Definition acquire : val :=
rec: "acquire" "lk" := rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1) if: CAS (Snd "lk") "n" ("n" + #1) = "n"
then wait_loop "n" "lk" then wait_loop "n" "lk"
else "acquire" "lk". else "acquire" "lk".
...@@ -122,14 +122,14 @@ Section proof. ...@@ -122,14 +122,14 @@ Section proof.
wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth". wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
{ iNext. iExists o', (S n). { iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. } rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
wp_if. wp_op. rewrite bool_decide_true //. wp_if.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]"). iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /is_lock; eauto 10. + iFrame. rewrite /is_lock; eauto 10.
+ by iNext. + by iNext.
- wp_cas_fail. iModIntro. - wp_cas_fail. iModIntro.
iSplitL "Hlo' Hln' Hauth Haown". iSplitL "Hlo' Hln' Hauth Haown".
{ iNext. iExists o', n'. by iFrame. } { iNext. iExists o', n'. by iFrame. }
wp_if. by iApply "IH"; auto. wp_op. rewrite bool_decide_false //. wp_if. by iApply "IH"; auto.
Qed. Qed.
Lemma release_spec γ lk R : Lemma release_spec γ lk R :
......
...@@ -56,8 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core ...@@ -56,8 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
(* [simpl apply] is too stupid, so we need extern hints here. *) (* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core. Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core. Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core. Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core. Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core. Local Hint Resolve to_of_val : core.
...@@ -355,7 +354,7 @@ Qed. ...@@ -355,7 +354,7 @@ Qed.
Lemma wp_cas_fail s E l q v' v1 v2 : Lemma wp_cas_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1 val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET LitV (LitBool false); l {q} v' }}}. {{{ RET v'; l {q} v' }}}.
Proof. Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
...@@ -365,7 +364,7 @@ Qed. ...@@ -365,7 +364,7 @@ Qed.
Lemma twp_cas_fail s E l q v' v1 v2 : Lemma twp_cas_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1 val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]]. [[{ RET v'; l {q} v' }]].
Proof. Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
...@@ -376,7 +375,7 @@ Qed. ...@@ -376,7 +375,7 @@ Qed.
Lemma wp_cas_suc s E l v1 v2 v' : Lemma wp_cas_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cas_compare_safe v' v1 val_for_compare v' = val_for_compare v1 vals_cas_compare_safe v' v1
{{{ l v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ l v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET LitV (LitBool true); l v2 }}}. {{{ RET v'; l v2 }}}.
Proof. Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
...@@ -387,7 +386,7 @@ Qed. ...@@ -387,7 +386,7 @@ Qed.
Lemma twp_cas_suc s E l v1 v2 v' : Lemma twp_cas_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cas_compare_safe v' v1 val_for_compare v' = val_for_compare v1 vals_cas_compare_safe v' v1
[[{ l v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET LitV (LitBool true); l v2 }]]. [[{ RET v'; l v2 }]].
Proof. Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
...@@ -496,6 +495,7 @@ Proof. ...@@ -496,6 +495,7 @@ Proof.
iMod "HΦ". iModIntro. by iApply "HΦ". iMod "HΦ". iModIntro. by iApply "HΦ".
Qed. Qed.
(** Lemmas for some particular expression inside the [Resolve]. *)
Lemma wp_resolve_proph s E p vs v : Lemma wp_resolve_proph s E p vs v :
{{{ proph p vs }}} {{{ proph p vs }}}
ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
...@@ -506,4 +506,29 @@ Proof. ...@@ -506,4 +506,29 @@ Proof.
iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame. iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
Qed. Qed.
Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
vals_cas_compare_safe v1 v1
{{{ proph p vs l v1 }}}
Resolve (CAS #l v1 v2) #p v @ s; E
{{{ RET v1 ; vs', vs = (v1, v)::vs' proph p vs' l v2 }}}.
Proof.
iIntros (Hcmp Φ) "[Hp Hl] HΦ".
iApply (wp_resolve with "Hp"); first done.
assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
iApply (wp_cas_suc with "Hl"); [done..|]. iIntros "!> Hl".
iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) q (v' v1 v2 v : val) :
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
{{{ proph p vs l {q} v' }}}
Resolve (CAS #l v1 v2) #p v @ s; E
{{{ RET v' ; vs', vs = (v', v)::vs' proph p vs' l {q} v' }}}.
Proof.
iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
iApply (wp_resolve with "Hp"); first done.
iApply (wp_cas_fail with "Hl"); [done..|]. iIntros "!> Hl".
iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
End lifting. End lifting.
...@@ -135,6 +135,7 @@ Proof. ...@@ -135,6 +135,7 @@ Proof.
- unfold un_op_eval in *. repeat case_match; naive_solver. - unfold un_op_eval in *. repeat case_match; naive_solver.
- eapply bin_op_eval_closed; eauto; naive_solver. - eapply bin_op_eval_closed; eauto; naive_solver.
- by apply heap_closed_alloc. - by apply heap_closed_alloc.
- case_match; try apply map_Forall_insert_2; by naive_solver.
Qed. Qed.
(* Parallel substitution with maps of values indexed by strings *) (* Parallel substitution with maps of values indexed by strings *)
......
...@@ -284,9 +284,9 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ : ...@@ -284,9 +284,9 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cas_compare_safe v v1 vals_cas_compare_safe v v1
(val_for_compare v = val_for_compare v1 (val_for_compare v = val_for_compare v1
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }}))
(val_for_compare v val_for_compare v1 (val_for_compare v val_for_compare v1
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail. rewrite envs_entails_eq=> ???? Hsuc Hfail.
...@@ -305,9 +305,9 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ : ...@@ -305,9 +305,9 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cas_compare_safe v v1 vals_cas_compare_safe v v1
(val_for_compare v = val_for_compare v1 (val_for_compare v = val_for_compare v1
envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }]))
(val_for_compare v val_for_compare v1 (val_for_compare v val_for_compare v1
envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof. Proof.
rewrite envs_entails_eq=> ??? Hsuc Hfail. rewrite envs_entails_eq=> ??? Hsuc Hfail.
...@@ -326,7 +326,7 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ : ...@@ -326,7 +326,7 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I envs_lookup i Δ' = Some (false, l {q} v)%I
val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1 val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ?????. rewrite envs_entails_eq=> ?????.
...@@ -337,7 +337,7 @@ Qed. ...@@ -337,7 +337,7 @@ Qed.
Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ : Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
envs_lookup i Δ = Some (false, l {q} v)%I envs_lookup i Δ = Some (false, l {q} v)%I
val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1 val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof. Proof.
rewrite envs_entails_eq. intros. rewrite -twp_bind. rewrite envs_entails_eq. intros. rewrite -twp_bind.
...@@ -350,7 +350,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ : ...@@ -350,7 +350,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1 val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ??????; subst. rewrite envs_entails_eq=> ??????; subst.
...@@ -363,7 +363,7 @@ Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ : ...@@ -363,7 +363,7 @@ Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1 val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof. Proof.
rewrite envs_entails_eq=>?????; subst. rewrite envs_entails_eq=>?????; subst.
...@@ -621,7 +621,7 @@ Tactic Notation "wp_faa" := ...@@ -621,7 +621,7 @@ Tactic Notation "wp_faa" :=
| |- envs_entails _ (wp ?s ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K)) [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
|fail 1 "wp_faa: cannot find 'CAS' in" e]; |fail 1 "wp_faa: cannot find 'FAA' in" e];
[iSolveTC [iSolveTC
|solve_mapsto () |solve_mapsto ()
|pm_reflexivity |pm_reflexivity
...@@ -629,7 +629,7 @@ Tactic Notation "wp_faa" := ...@@ -629,7 +629,7 @@ Tactic Notation "wp_faa" :=
| |- envs_entails _ (twp ?s ?E ?e ?Q) => | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K)) [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
|fail 1 "wp_faa: cannot find 'CAS' in" e]; |fail 1 "wp_faa: cannot find 'FAA' in" e];
[solve_mapsto () [solve_mapsto ()
|pm_reflexivity |pm_reflexivity
|wp_finish] |wp_finish]
......