Skip to content

GitLab

Commit 242cee02 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

make primitive compare-exchange return both boolean and old value for ease of use

parent 5fae061a
Hide whitespace changes
Inline Side-by-side
Showing with 126 additions and 150 deletions
_CoqProject
View file @ 242cee02
......@@ -116,7 +116,6 @@ theories/heap_lang/lib/clairvoyant_coin.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/compare_and_set.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
tests/heap_lang.ref
View file @ 242cee02
......@@ -40,7 +40,7 @@
============================
_ : ▷ l ↦ #0
--------------------------------------∗
WP CAS #l #0 #1 {{ _, l ↦ #1 }}
WP CompareExchange #l #0 #1 {{ _, l ↦ #1 }}
1 subgoal
......@@ -148,4 +148,5 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
Tactic failure: wp_cas_suc: cannot find 'CompareExchange' in
(#() #()).
tests/heap_lang.v
View file @ 242cee02
......@@ -79,7 +79,7 @@ Section tests.
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
Definition heap_e7 : val := λ: "v", CompareExchange "v" #0 #1.
Lemma heap_e7_spec_total l : l ↦ #0 -∗ WP heap_e7 #l [{_, l ↦ #1 }].
Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
......@@ -126,7 +126,7 @@ Section tests.
Lemma wp_cas l v :
val_is_unboxed v →
l ↦ v -∗ WP CAS #l v v {{ _, True }}.
l ↦ v -∗ WP CompareExchange #l v v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
......
tests/heap_lang_proph.v
View file @ 242cee02
......@@ -11,7 +11,8 @@ Section tests.
Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
l ↦ #n -∗
proph p vs -∗
WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #n⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
WP Resolve (CompareExchange #l #n (#n + #1)) #p v @ E
{{ v, ⌜v = (#true, #n)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
Proof.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
......
tests/ipm_paper.v
View file @ 242cee02
......@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
Definition incr : val :=
rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l".
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** The CMRA we need. *)
......@@ -222,7 +222,7 @@ Section counter_proof.
iDestruct 1 as (c) "[Hl Hγ]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_bind (CAS _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
wp_bind (CompareExchange _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c') ">[Hl Hγ]".
destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ".
......@@ -231,11 +231,10 @@ Section counter_proof.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_op. rewrite bool_decide_true //. wp_if. rewrite {3}/C; eauto 10.
- assert (#c ≠ #c') by (intros [=]; abstract omega). wp_cas_fail.
wp_pures. rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_op. rewrite bool_decide_false //. wp_if.
iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed.
Check "read_spec".
......
tests/one_shot.v
View file @ 242cee02
......@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
CAS "x" NONE (SOME "n") = NONE),
CAS "x" NONE (SOME "n")),
(* check *) (λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
......@@ -49,15 +49,13 @@ Proof.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
wp_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CAS _ _ _).
- iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CompareExchange _ _ _).
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
wp_cas_suc. iSplitL; iModIntro; last first.
{ wp_pures. eauto. }
wp_cas_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; iModIntro; last first.
{ wp_pures. eauto. }
+ wp_cas_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
......
theories/heap_lang/lang.v
View file @ 242cee02
......@@ -97,7 +97,7 @@ Inductive expr :=
| AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-and-swap (NOT compare-and-set!) *)
| CompareExchange (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
(* Prophecy *)
| NewProph
......@@ -235,7 +235,7 @@ Proof.
| Load e, Load e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| CAS e0 e1 e2, CAS e0' e1' e2' =>
| CompareExchange e0 e1 e2, CompareExchange e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| FAA e1 e2, FAA e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
......@@ -311,7 +311,7 @@ Proof.
| AllocN e1 e2 => GenNode 13 [go e1; go e2]
| Load e => GenNode 14 [go e]
| Store e1 e2 => GenNode 15 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
| CompareExchange e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
| FAA e1 e2 => GenNode 17 [go e1; go e2]
| NewProph => GenNode 18 []
| Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
......@@ -346,7 +346,7 @@ Proof.
| GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
| GenNode 14 [e] => Load (go e)
| GenNode 15 [e1; e2] => Store (go e1) (go e2)
| GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 16 [e0; e1; e2] => CompareExchange (go e0) (go e1) (go e2)
| GenNode 17 [e1; e2] => FAA (go e1) (go e2)
| GenNode 18 [] => NewProph
| GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
......@@ -401,9 +401,9 @@ Inductive ectx_item :=
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| CasLCtx (v1 : val) (v2 : val)
| CasMCtx (e0 : expr) (v2 : val)
| CasRCtx (e0 : expr) (e1 : expr)
| CompareExchangeLCtx (v1 : val) (v2 : val)
| CompareExchangeMCtx (e0 : expr) (v2 : val)
| CompareExchangeRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
......@@ -437,9 +437,9 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
| CasMCtx e0 v2 => CAS e0 e (Val v2)
| CasRCtx e0 e1 => CAS e0 e1 e
| CompareExchangeLCtx v1 v2 => CompareExchange e (Val v1) (Val v2)
| CompareExchangeMCtx e0 v2 => CompareExchange e0 e (Val v2)
| CompareExchangeRCtx e0 e1 => CompareExchange e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
| ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
......@@ -468,7 +468,7 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
| CompareExchange e0 e1 e2 => CompareExchange (subst x v e0) (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
......@@ -634,13 +634,14 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CasS l v1 v2 vl σ :
| CompareExchangeS l v1 v2 vl σ :
vals_cas_compare_safe vl v1 →
σ.(heap) !! l = Some vl →
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
(* Crucially, this compares the same way as [EqOp]! *)
let b := bool_decide (val_for_compare vl = val_for_compare v1) in
head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val 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 σ)
(Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
[]
| FaaS l i1 i2 σ :
σ.(heap) !! l = Some (LitV (LitInt i1)) →
......
theories/heap_lang/lib/atomic_heap.v
View file @ 242cee02
......@@ -31,12 +31,14 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
spec is still good enough for all our applications.
The postcondition deliberately does not use [bool_decide] so that users can
[destruct (decide (a = b))] and it will simplify in both places. *)
cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
<<< ∀ 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,
RET v >>>;
RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
}.
Arguments atomic_heap _ {_}.
......@@ -100,13 +102,13 @@ Section proof.
<<< ∀ (v : val), l ↦ v >>>
primitive_cas #l w1 w2 @ ⊤
<<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
RET v >>>.
RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
Proof.
iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
iIntros (? Φ) "AU". wp_lam. wp_pures. wp_bind (CompareExchange _ _ _).
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
[wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; done.
iMod ("Hclose" with "H↦") as "HΦ"; iModIntro; by wp_pures.
Qed.
End proof.
......
theories/heap_lang/lib/compare_and_set.v deleted 100644 → 0
View file @ 5fae061a
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.
theories/heap_lang/lib/counter.v
View file @ 242cee02
......@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: compare_and_set "l" "n" (#1 + "n") then #() else "incr" "l".
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
......@@ -50,25 +50,22 @@ Section mono_proof.
iDestruct "Hl" as (γ) "[#? Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures. wp_apply caset_spec; first done.
iInv N as (c') ">[Hγ Hl]" "Hclose".
wp_pures. wp_bind (CompareExchange _ _ _).
iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_both_valid.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
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. iFrame. }
iModIntro. wp_if.
iApply "HΦ"; iExists γ; repeat iSplit; eauto.
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf").
(* FIXME: FIXME(Coq #6294): needs new unification *)
apply: auth_frag_mono. by apply mnat_included, le_n_S.
- iExists _; iFrame "Hl". iIntros "!> Hl".
rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10.
Qed.
......@@ -132,19 +129,17 @@ Section contrib_spec.
iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures. wp_apply caset_spec; first done.
iInv N as (c') ">[Hγ Hl]" "Hclose".
wp_pures. wp_bind (CompareExchange _ _ _).
iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
iExists _; iFrame "Hl". iIntros "!> Hl".
rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. by iApply "HΦ".
- iExists _; iFrame "Hl". iIntros "!> Hl".
rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
wp_pures. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ l q n :
......
theories/heap_lang/lib/increment.v
View file @ 242cee02
......@@ -16,7 +16,7 @@ Section increment_physical.
Definition incr_phy : val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
if: CAS "l" "oldv" ("oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
......@@ -26,12 +26,12 @@ Section increment_physical.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
wp_pures. wp_bind (CompareExchange _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
destruct (decide (#v = #w)) as [[= ->]|Hx].
- wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iModIntro. wp_op. rewrite bool_decide_true //. wp_if. done.
iModIntro. wp_pures. done.
- wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iModIntro. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
iModIntro. wp_pures. iApply "IH". done.
Qed.
End increment_physical.
......@@ -45,7 +45,7 @@ Section increment.
Definition incr : val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
if: CAS "l" "oldv" ("oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
......@@ -70,9 +70,9 @@ Section increment.
{ (* abort case *) iDestruct "Hclose" as "[? _]". done. }
iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iIntros "!>". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
iIntros "!>". wp_if. by iApply "HΦ".
- iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iIntros "!>". wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
iIntros "!>". wp_if. iApply "IH". done.
Qed.
(** A proof of the incr specification that uses lemmas to avoid reasining
......@@ -94,9 +94,9 @@ Section increment.
iIntros "H↦ !>".
simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !>".
wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !>".
wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
wp_if. iApply "IH". done.
Qed.
(** A "weak increment": assumes that there is no race *)
......
theories/heap_lang/lib/spin_lock.v
View file @ 242cee02
......@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true = #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
......@@ -61,7 +61,7 @@ Section proof.
{{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. wp_bind (CAS _ _ _). iInv N as ([]) "[Hl HR]".
wp_rec. wp_bind (CompareExchange _ _ _). iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
wp_pures. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
......
theories/heap_lang/lib/ticket_lock.v
View file @ 242cee02
......@@ -20,7 +20,7 @@ Definition newlock : val :=
Definition acquire : val :=
rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1) = "n"
if: CAS (Snd "lk") "n" ("n" + #1)
then wait_loop "n" "lk"
else "acquire" "lk".
......@@ -111,7 +111,7 @@ Section proof.
iInv N as (o n) "[Hlo [Hln Ha]]".
wp_load. iModIntro. iSplitL "Hlo Hln Ha".
{ iNext. iExists o, n. by iFrame. }
wp_pures. wp_bind (CAS _ _ _).
wp_pures. wp_bind (CompareExchange _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
- iMod (own_update with "Hauth") as "[Hauth Hofull]".
......@@ -122,14 +122,14 @@ Section proof.
wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
wp_op. rewrite bool_decide_true //. wp_if.
wp_pures.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /is_lock; eauto 10.
+ by iNext.
- wp_cas_fail. iModIntro.
iSplitL "Hlo' Hln' Hauth Haown".
{ iNext. iExists o', n'. by iFrame. }
wp_op. rewrite bool_decide_false //. wp_if. by iApply "IH"; auto.
wp_pures. by iApply "IH"; auto.
Qed.
Lemma release_spec γ lk R :
......
theories/heap_lang/lifting.v
View file @ 242cee02
......@@ -56,7 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasS : core.
Local Hint Extern 0 (head_step (CompareExchange _ _ _) _ _ _ _ _) => eapply CompareExchangeS : 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 Resolve to_of_val : core.
......@@ -77,7 +77,7 @@ Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Instance cas_atomic s v0 v1 v2 : Atomic s (CompareExchange (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
......@@ -376,44 +376,48 @@ Qed.
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 →
{{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET v'; l ↦{q} v' }}}.
{{{ ▷ l ↦{q} v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (#false, v'); l ↦{q} v' }}}.
Proof.
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 %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
rewrite /b bool_decide_false //.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
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 →
[[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET v'; l ↦{q} v' }]].
[[{ l ↦{q} v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (#false, v'); l ↦{q} v' }]].
Proof.
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 %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
rewrite /b bool_decide_false //.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc s E l v1 v2 v' :
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
{{{ RET v'; l ↦ v2 }}}.
{{{ ▷ l ↦ v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (#true, v'); l ↦ v2 }}}.
Proof.
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 %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
rewrite /b bool_decide_true //.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l v1 v2 v' :
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
[[{ RET v'; l ↦ v2 }]].
[[{ l ↦ v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (#true, v'); l ↦ v2 }]].
Proof.