Skip to content

I
Iris
Commit 12bec4d5 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

rename CompareExchange to CmpXchg 

This is the name used by x86 (CMPXCHG) and LLVM.  Also reorder the result (value
first, boolean second) for consistency with LLVM, because why not.
parent fc9bb073
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 221 additions and 202 deletions
tests/heap_lang.ref
View file @ 12bec4d5
......@@ -40,7 +40,7 @@
============================
_ : ▷ l ↦ #0
--------------------------------------∗
WP CompareExchange #l #0 #1 {{ _, l ↦ #1 }}
WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
1 subgoal
......@@ -144,9 +144,9 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
"not_cas"
"not_cmpxchg"
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CompareExchange' in
Ltac call to "wp_cmpxchg_suc" failed.
Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in
(#() #()).
tests/heap_lang.v
View file @ 12bec4d5
......@@ -79,14 +79,14 @@ 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", CompareExchange "v" #0 #1.
Definition heap_e7 : val := λ: "v", CmpXchg "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.
Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
Check "heap_e7_spec".
Lemma heap_e7_spec l : ▷^2 l ↦ #0 -∗ WP heap_e7 #l {{_, l ↦ #1 }}.
Proof. iIntros. wp_lam. Show. wp_cas_suc. Show. auto. Qed.
Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
......@@ -124,11 +124,11 @@ Section tests.
P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_cas l v :
Lemma wp_cmpxchg l v :
val_is_unboxed v →
l ↦ v -∗ WP CompareExchange #l v v {{ _, True }}.
l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
Qed.
Lemma wp_alloc_split :
......@@ -210,11 +210,11 @@ End printing_tests.
Section error_tests.
Context `{!heapG Σ}.
Check "not_cas".
Lemma not_cas :
Check "not_cmpxchg".
Lemma not_cmpxchg :
(WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Fail wp_cmpxchg_suc.
Abort.
End error_tests.
......
tests/heap_lang_proph.v
View file @ 12bec4d5
......@@ -11,11 +11,14 @@ 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 (CompareExchange #l #n (#n + #1)) #p v @ E
{{ v, ⌜v = (#true, #n)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
{{ v, ⌜v = (#n, #true)%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.
wp_cmpxchg_suc. iIntros (ws ->) "Hp". eauto with iFrame.
Restart.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
Qed.
Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
......
tests/ipm_paper.v
View file @ 12bec4d5
......@@ -222,17 +222,17 @@ 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 (CompareExchange _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
wp_bind (CmpXchg _ _ _). 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γ".
iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iSplitL "Hl Hγ".
wp_cmpxchg_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
- wp_cmpxchg_fail; first (intros [=]; abstract omega).
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed.
......
tests/one_shot.v
View file @ 12bec4d5
......@@ -49,13 +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 (CompareExchange _ _ _).
- iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
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. iModIntro. iSplitL; last (wp_pures; by eauto).
wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
+ wp_cmpxchg_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 @ 12bec4d5
......@@ -28,11 +28,11 @@ the [Resolve] is stuck), and this value is also attached to the resolution.
A prophecy variable is thus resolved to a pair containing (1) the result
value of the wrapped expression (called [e] above), and (2) the value that
was attached by the [Resolve] (called [v] above). This allows, for example,
to distinguish a resolution originating from a successful [CAS] from one
originating from a failing [CAS]. For example:
- [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)],
which means step to a boolean [b] while updating the heap, but in the
meantime the prophecy variable [p] will be resolved to [(#b, v)].
to distinguish a resolution originating from a successful [CmpXchg] from one
originating from a failing [CmpXchg]. For example:
- [Resolve (CmpXchg #l #n #(n+1)) #p v] will behave as [CmpXchg #l #n #(n+1)],
which means step to a value-boole pair [(n', b)] while updating the heap, but
in the meantime the prophecy variable [p] will be resolved to [(n', b), v)].
- [Resolve (! #l) #p v] will behave as [! #l], that is return the value
[w] pointed to by [l] on the heap (assuming it was allocated properly),
but it will additionally resolve [p] to the pair [(w,v)].
......@@ -41,10 +41,10 @@ Note that the sub-expressions of [Resolve e p v] (i.e., [e], [p] and [v])
are reduced as usual, from right to left. However, the evaluation of [e]
is restricted so that the head-step to which the resolution is attached
cannot be taken by the context. For example:
- [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a
context-step) to [Resolve (CAS #l #n #(n+1) #p v], and then behave as
- [Resolve (CmpXchg #l #n (#n + #1)) #p v] will first be reduced (with by a
context-step) to [Resolve (CmpXchg #l #n #(n+1) #p v], and then behave as
described above.
- However, [Resolve ((λ: "n", CAS #l "n" ("n" + #1)) #n) #p v] is stuck.
- However, [Resolve ((λ: "n", CmpXchg #l "n" ("n" + #1)) #n) #p v] is stuck.
Indeed, it can only be evaluated using a head-step (it is a β-redex),
but the process does not yield a value.
......@@ -97,7 +97,7 @@ Inductive expr :=
| AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CompareExchange (e0 : expr) (e1 : expr) (e2 : expr)
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
(* Prophecy *)
| NewProph
......@@ -115,7 +115,7 @@ Bind Scope val_scope with val.
(** An observation associates a prophecy variable (identifier) to a pair of
values. The first value is the one that was returned by the (atomic) operation
during which the prophecy resolution happened (typically, a boolean when the
wrapped operation is a CAS). The second value is the one that the prophecy
wrapped operation is a CmpXchg). The second value is the one that the prophecy
variable was actually resolved to. *)
Definition observation : Set := proph_id * (val * val).
......@@ -159,13 +159,13 @@ Definition val_is_unboxed (v : val) : Prop :=
| _ => False
end.
(** CAS just compares the word-sized representation of two values, it cannot
(** CmpXchg just compares the word-sized representation of two values, it cannot
look into boxed data. This works out fine if at least one of the to-be-compared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
Definition vals_cmpxchg_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl ∨ val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Arguments vals_cmpxchg_compare_safe !_ !_ /.
(** We don't compare the logical program values, but we first normalize them
to make sure that prophecies are treated like unit.
......@@ -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'))
| CompareExchange e0 e1 e2, CompareExchange e0' e1' e2' =>
| CmpXchg e0 e1 e2, CmpXchg 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]
| CompareExchange e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
| CmpXchg 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] => CompareExchange (go e0) (go e1) (go e2)
| GenNode 16 [e0; e1; e2] => CmpXchg (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)
| CompareExchangeLCtx (v1 : val) (v2 : val)
| CompareExchangeMCtx (e0 : expr) (v2 : val)
| CompareExchangeRCtx (e0 : expr) (e1 : expr)
| CmpXchgLCtx (v1 : val) (v2 : val)
| CmpXchgMCtx (e0 : expr) (v2 : val)
| CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
......@@ -414,8 +414,8 @@ Inductive ectx_item :=
the local context of [e] is non-empty. As a consequence, the first argument of
[Resolve] is not completely evaluated (down to a value) by contextual closure:
no head steps (i.e., surface reductions) are taken. This means that contextual
closure will reduce [Resolve (CAS #l #n (#n + #1)) #p #v] into [Resolve (CAS
#l #n #(n+1)) #p #v], but it cannot context-step any further. *)
closure will reduce [Resolve (CmpXchg #l #n (#n + #1)) #p #v] into [Resolve
(CmpXchg #l #n #(n+1)) #p #v], but it cannot context-step any further. *)
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
......@@ -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
| CompareExchangeLCtx v1 v2 => CompareExchange e (Val v1) (Val v2)
| CompareExchangeMCtx e0 v2 => CompareExchange e0 e (Val v2)
| CompareExchangeRCtx e0 e1 => CompareExchange e0 e1 e
| CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CmpXchgRCtx e0 e1 => CmpXchg 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)
| CompareExchange e0 e1 e2 => CompareExchange (subst x v e0) (subst x v e1) (subst x v e2)
| CmpXchg e0 e1 e2 => CmpXchg (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)
......@@ -518,7 +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 :=
if decide (op = EqOp) then
(* Crucially, this compares the same way as [CAS]! *)
(* Crucially, this compares the same way as [CmpXchg]! *)
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
else
match v1, v2 with
......@@ -634,14 +634,14 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CompareExchangeS l v1 v2 vl σ b :
vals_cas_compare_safe vl v1 →
| CmpXchgS l v1 v2 vl σ b :
vals_cmpxchg_compare_safe vl v1 →
σ.(heap) !! l = Some vl →
(* Crucially, this compares the same way as [EqOp]! *)
b = bool_decide (val_for_compare vl = val_for_compare v1) →
head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
(Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
(Val $ PairV vl (LitV $ LitBool b)) (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 @ 12bec4d5
......@@ -11,7 +11,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
alloc : val;
load : val;
store : val;
cas : val;
cmpxchg : val;
(* -- predicates -- *)
mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
(* -- mapsto properties -- *)
......@@ -34,11 +34,11 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
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) :
cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
<<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
<<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
<<< 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, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
}.
Arguments atomic_heap _ {_}.
......@@ -56,10 +56,28 @@ Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
Notation CAS e1 e2 e3 := (cas e1 e2 e3).
Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
End notation.
Section derived.
Context `{!heapG Σ, !atomic_heap Σ}.
Import notation.
Lemma 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 #if decide (val_for_compare v = val_for_compare w1) then true else false >>>.
Proof.
iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
iApply (aacc_aupd_commit with "AU"); first done.
iIntros (v) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> HΦ !>". wp_pures. done.
Qed.
End derived.
(** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val :=
λ: "v", ref "v".
......@@ -67,8 +85,8 @@ Definition primitive_load : val :=
λ: "l", !"l".
Definition primitive_store : val :=
λ: "l" "x", "l" <- "x".
Definition primitive_cas : val :=
λ: "l" "e1" "e2", CAS "l" "e1" "e2".
Definition primitive_cmpxchg : val :=
λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
Section proof.
Context `{!heapG Σ}.
......@@ -97,18 +115,18 @@ Section proof.
wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
Qed.
Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
<<< ∀ (v : val), l ↦ v >>>
primitive_cas #l w1 w2 @ ⊤
primitive_cmpxchg #l w1 w2 @ ⊤
<<< 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, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
Proof.
iIntros (? Φ) "AU". wp_lam. wp_pures. wp_bind (CompareExchange _ _ _).
iIntros (? Φ) "AU". wp_lam. wp_pures.
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Φ"; iModIntro; by wp_pures.
[wp_cmpxchg_suc|wp_cmpxchg_fail];
iMod ("Hclose" with "H↦") as "HΦ"; done.
Qed.
End proof.
......@@ -118,5 +136,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec;
store_spec := primitive_store_spec;
cas_spec := primitive_cas_spec;
cmpxchg_spec := primitive_cmpxchg_spec;
mapsto_agree := gen_heap.mapsto_agree |}.
theories/heap_lang/lib/counter.v
View file @ 12bec4d5
......@@ -50,20 +50,20 @@ 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_bind (CompareExchange _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
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. }
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
wp_cmpxchg_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.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
- wp_cmpxchg_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.
......@@ -129,15 +129,15 @@ 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_bind (CompareExchange _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
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. }
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
- wp_cmpxchg_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.
......
theories/heap_lang/lib/increment.v
View file @ 12bec4d5
......@@ -26,11 +26,11 @@ 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 (CompareExchange _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
wp_pures. wp_bind (CmpXchg _ _ _)%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Φ".
- wp_cmpxchg_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iModIntro. wp_pures. done.
- wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
- wp_cmpxchg_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
iModIntro. wp_pures. iApply "IH". done.
Qed.
End increment_physical.
......
theories/heap_lang/lib/spin_lock.v
View file @ 12bec4d5
......@@ -61,10 +61,10 @@ 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 (CompareExchange _ _ _). iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
wp_rec. wp_bind (CmpXchg _ _ _). iInv N as ([]) "[Hl HR]".
- wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
wp_pures. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
- wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
......
theories/heap_lang/lib/ticket_lock.v
View file @ 12bec4d5
......@@ -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 (CompareExchange _ _ _).
wp_pures. wp_bind (CmpXchg _ _ _).
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]".
......@@ -119,14 +119,14 @@ Section proof.
eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
apply (set_seq_S_end_disjoint 0). }
rewrite -(set_seq_S_end_union_L 0).
wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
wp_pures.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /is_lock; eauto 10.
+ by iNext.
- wp_cas_fail. iModIntro.
- wp_cmpxchg_fail. iModIntro.
iSplitL "Hlo' Hln' Hauth Haown".
{ iNext. iExists o', n'. by iFrame. }
wp_pures. by iApply "IH"; auto.
......
theories/heap_lang/lifting.v
View file @ 12bec4d5
......@@ -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 (CompareExchange _ _ _) _ _ _ _ _) => eapply CompareExchangeS : core.
Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : 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 (CompareExchange (Val v0) (Val v1) (Val v2)).
Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (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.
......@@ -374,10 +374,10 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
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' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (#false, v'); l ↦{q} v' }}}.
Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
{{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (v', #false); 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 %?.
......@@ -385,10 +385,10 @@ Proof.
rewrite 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' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (#false, v'); l ↦{q} v' }]].
Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
[[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (v', #false); 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 %?.
......@@ -397,10 +397,10 @@ Proof.
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' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (#true, v'); l ↦ v2 }}}.
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
{{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET (v', #true); 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 %?.
......@@ -409,10 +409,10 @@ Proof.
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' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (#true, v'); l ↦ v2 }]].
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
[[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET (v', #true); l ↦ v2 }]].
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 %?.
......@@ -533,28 +533,28 @@ Proof.
iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
Qed.
Lemma wp_resolve_cas_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
vals_cas_compare_safe v1 v1 →
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
vals_cmpxchg_compare_safe v1 v1 →
{{{ proph p pvs ∗ ▷ l ↦ v1 }}}
Resolve (CompareExchange #l v1 v2) #p v @ s; E
{{{ RET (#true, v1) ; ∃ pvs', ⌜pvs = ((#true, v1)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ 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".
iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
Lemma wp_resolve_cas_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
{{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
Resolve (CompareExchange #l v1 v2) #p v @ s; E
{{{ RET (#false, v') ; ∃ pvs', ⌜pvs = ((#false, v')%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ 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".
iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
......@@ -602,54 +602,54 @@ Proof.