Commit 5ef58527 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/cas' into 'master'

Turn CAS from compare-and-set to compare-and-swap

See merge request iris/iris!274
parents 4a85888c f02197aa
...@@ -54,6 +54,12 @@ Changes in heap_lang: ...@@ -54,6 +54,12 @@ Changes in heap_lang:
"normalized" to the same. This makes all closures indistinguishable from each "normalized" to the same. This makes all closures indistinguishable from each
other while remaining unqueal to anything else. We also use the same other while remaining unqueal to anything else. We also use the same
"normalization" to make sure all prophecy variables seem equal to `()`. "normalization" to make sure all prophecy variables seem equal to `()`.
* CAS (compare-and-set) got replaced by CmpXchg (compare-exchange). The
difference is that CmpXchg returns a pair consisting of the old value and a
boolean indicating whether the comparison was successful and hence the
exchange happened. CAS can be obtained by simply projecting to the second
component, but also providing the old value more closely models the primitive
typically provided in systems languages (C, C++, Rust).
Changes in Coq: Changes in Coq:
......
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
============================ ============================
_ : ▷ l ↦ #0 _ : ▷ l ↦ #0
--------------------------------------∗ --------------------------------------∗
WP CAS #l #0 #1 {{ _, l ↦ #1 }} WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
1 subgoal 1 subgoal
...@@ -144,8 +144,9 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or ...@@ -144,8 +144,9 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3" let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}} {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
"not_cas" "not_cmpxchg"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed. Ltac call to "wp_cmpxchg_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()). Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in
(#() #()).
...@@ -79,14 +79,14 @@ Section tests. ...@@ -79,14 +79,14 @@ Section tests.
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I. Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed. Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CAS "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 }]. 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". Check "heap_e7_spec".
Lemma heap_e7_spec l : ^2 l #0 - WP heap_e7 #l {{_, l #1 }}. 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 := Definition FindPred : val :=
rec: "pred" "x" "y" := rec: "pred" "x" "y" :=
...@@ -124,11 +124,11 @@ Section tests. ...@@ -124,11 +124,11 @@ Section tests.
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}. P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed. Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_cas l v : Lemma wp_cmpxchg l v :
val_is_unboxed v val_is_unboxed v
l v - WP CAS #l v v {{ _, True }}. l v - WP CmpXchg #l v v {{ _, True }}.
Proof. Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done. iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
Qed. Qed.
Lemma wp_alloc_split : Lemma wp_alloc_split :
...@@ -210,11 +210,11 @@ End printing_tests. ...@@ -210,11 +210,11 @@ End printing_tests.
Section error_tests. Section error_tests.
Context `{!heapG Σ}. Context `{!heapG Σ}.
Check "not_cas". Check "not_cmpxchg".
Lemma not_cas : Lemma not_cmpxchg :
(WP #() #() {{ _, True }})%I. (WP #() #() {{ _, True }})%I.
Proof. Proof.
Fail wp_cas_suc. Fail wp_cmpxchg_suc.
Abort. Abort.
End error_tests. End error_tests.
......
...@@ -8,46 +8,22 @@ Section tests. ...@@ -8,46 +8,22 @@ 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 (CmpXchg #l #n (#n + #1)) #p v @ E
{{ v, v = (#n, #true)%V vs, proph p vs l #(n+1) }}.
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_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. Qed.
Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) : Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
proph p vs - proph p vs -
WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0 vs, proph p vs }}%I. WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0 vs, proph p vs }}.
Proof. Proof.
iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done. iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame. wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
......
...@@ -222,19 +222,19 @@ Section counter_proof. ...@@ -222,19 +222,19 @@ Section counter_proof.
iDestruct 1 as (c) "[Hl Hγ]". iDestruct 1 as (c) "[Hl Hγ]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op. wp_let. wp_op.
wp_bind (CAS _ _ _). 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γ]". iDestruct 1 as (c') ">[Hl Hγ]".
destruct (decide (c' = c)) as [->|]. destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ". - iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //. iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
iMod (own_update with "Hγ") as "Hγ"; first apply M_update. 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]". 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. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. rewrite {3}/C; eauto 10. 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|]. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
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. Qed.
Check "read_spec". Check "read_spec".
......
...@@ -49,13 +49,13 @@ Proof. ...@@ -49,13 +49,13 @@ 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 (CmpXchg _ _ _).
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_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iModIntro. iNext; iRight; iExists n; by iFrame. iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; last eauto. + wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by 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γ".
......
...@@ -28,11 +28,11 @@ the [Resolve] is stuck), and this value is also attached to the resolution. ...@@ -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 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 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, was attached by the [Resolve] (called [v] above). This allows, for example,
to distinguish a resolution originating from a successful [CAS] from one to distinguish a resolution originating from a successful [CmpXchg] from one
originating from a failing [CAS]. For example: originating from a failing [CmpXchg]. For example:
- [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)], - [Resolve (CmpXchg #l #n #(n+1)) #p v] will behave as [CmpXchg #l #n #(n+1)],
which means step to a boolean [b] while updating the heap, but in the which means step to a value-boole pair [(n', b)] while updating the heap, but
meantime the prophecy variable [p] will be resolved to [(#b, v)]. 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 - [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), [w] pointed to by [l] on the heap (assuming it was allocated properly),
but it will additionally resolve [p] to the pair [(w,v)]. 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]) ...@@ -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] 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 is restricted so that the head-step to which the resolution is attached
cannot be taken by the context. For example: cannot be taken by the context. For example:
- [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a - [Resolve (CmpXchg #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 context-step) to [Resolve (CmpXchg #l #n #(n+1) #p v], and then behave as
described above. 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), Indeed, it can only be evaluated using a head-step (it is a β-redex),
but the process does not yield a value. but the process does not yield a value.
...@@ -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) | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
| 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 *)
...@@ -115,7 +115,7 @@ Bind Scope val_scope with val. ...@@ -115,7 +115,7 @@ Bind Scope val_scope with val.
(** An observation associates a prophecy variable (identifier) to a pair of (** 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 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 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. *) variable was actually resolved to. *)
Definition observation : Set := proph_id * (val * val). Definition observation : Set := proph_id * (val * val).
...@@ -159,13 +159,13 @@ Definition val_is_unboxed (v : val) : Prop := ...@@ -159,13 +159,13 @@ Definition val_is_unboxed (v : val) : Prop :=
| _ => False | _ => False
end. 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 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 values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *) 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. 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 (** We don't compare the logical program values, but we first normalize them
to make sure that prophecies are treated like unit. to make sure that prophecies are treated like unit.
...@@ -235,7 +235,7 @@ Proof. ...@@ -235,7 +235,7 @@ Proof.
| Load e, Load e' => cast_if (decide (e = e')) | Load e, Load e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' => | Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2')) cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| CAS e0 e1 e2, CAS e0' e1' e2' => | CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2')) cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| FAA e1 e2, FAA e1' e2' => | FAA e1 e2, FAA e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2')) cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
...@@ -311,7 +311,7 @@ Proof. ...@@ -311,7 +311,7 @@ Proof.
| AllocN e1 e2 => GenNode 13 [go e1; go e2] | AllocN e1 e2 => GenNode 13 [go e1; go e2]
| Load e => GenNode 14 [go e] | Load e => GenNode 14 [go e]
| Store e1 e2 => GenNode 15 [go e1; go e2] | Store e1 e2 => GenNode 15 [go e1; go e2]
| CAS 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] | FAA e1 e2 => GenNode 17 [go e1; go e2]
| NewProph => GenNode 18 [] | NewProph => GenNode 18 []
| Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2] | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
...@@ -346,7 +346,7 @@ Proof. ...@@ -346,7 +346,7 @@ Proof.
| GenNode 13 [e1; e2] => AllocN (go e1) (go e2) | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
| GenNode 14 [e] => Load (go e) | GenNode 14 [e] => Load (go e)
| GenNode 15 [e1; e2] => Store (go e1) (go e2) | 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] => CmpXchg (go e0) (go e1) (go e2)
| GenNode 17 [e1; e2] => FAA (go e1) (go e2) | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
| GenNode 18 [] => NewProph | GenNode 18 [] => NewProph
| GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2) | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
...@@ -401,9 +401,9 @@ Inductive ectx_item := ...@@ -401,9 +401,9 @@ Inductive ectx_item :=
| LoadCtx | LoadCtx
| StoreLCtx (v2 : val) | StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr) | StoreRCtx (e1 : expr)
| CasLCtx (v1 : val) (v2 : val) | CmpXchgLCtx (v1 : val) (v2 : val)
| CasMCtx (e0 : expr) (v2 : val) | CmpXchgMCtx (e0 : expr) (v2 : val)
| CasRCtx (e0 : expr) (e1 : expr) | CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val) | FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr) | FaaRCtx (e1 : expr)
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val) | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
...@@ -414,8 +414,8 @@ Inductive ectx_item := ...@@ -414,8 +414,8 @@ Inductive ectx_item :=
the local context of [e] is non-empty. As a consequence, the first argument of 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: [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 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 closure will reduce [Resolve (CmpXchg #l #n (#n + #1)) #p #v] into [Resolve
#l #n #(n+1)) #p #v], but it cannot context-step any further. *) (CmpXchg #l #n #(n+1)) #p #v], but it cannot context-step any further. *)
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr := Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with match Ki with
...@@ -437,9 +437,9 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr := ...@@ -437,9 +437,9 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
| LoadCtx => Load e | LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2) | StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e | StoreRCtx e1 => Store e1 e
| CasLCtx v1 v2 => CAS e (Val v1) (Val v2) | CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CasMCtx e0 v2 => CAS e0 e (Val v2) | CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CasRCtx e0 e1 => CAS e0 e1 e | CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
| FaaLCtx v2 => FAA e (Val v2) | FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e | FaaRCtx e1 => FAA e1 e
| ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2) | 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 := ...@@ -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) | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Load e => Load (subst x v e) | Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2) | 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) | 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) | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph | NewProph => NewProph
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2) | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
...@@ -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 [CmpXchg]! *)
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,14 @@ Inductive head_step : expr → state → list observation → expr → state → ...@@ -633,19 +634,14 @@ 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 σ : | CmpXchgS l v1 v2 vl σ b :
vals_cas_compare_safe vl v1 vals_cmpxchg_compare_safe vl v1
σ.(heap) !! l = Some vl σ.(heap) !! l = Some vl
val_for_compare vl val_for_compare v1 (* Crucially, this compares the same way as [EqOp]! *)
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ [] b = bool_decide (val_for_compare vl = val_for_compare v1)
(Val $ LitV $ LitBool false) σ [] head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
| 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)) σ
[] []
(Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ) (Val $ PairV vl (LitV $ LitBool b)) (if b 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))
......
...@@ -11,7 +11,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -11,7 +11,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
alloc : val; alloc : val;
load : val; load : val;
store : val; store : val;
cas : val; cmpxchg : val;
(* -- predicates -- *) (* -- predicates -- *)
mapsto (l : loc) (q: Qp) (v : val) : iProp Σ; mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
(* -- mapsto properties -- *) (* -- mapsto properties -- *)
...@@ -31,12 +31,14 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -31,12 +31,14 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
(* This spec is slightly weaker than it could be: It is sufficient for [w1] (* 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] *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 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.
cas_spec (l : loc) (w1 w2 : val) : The postcondition deliberately does not use [bool_decide] so that users can
[destruct (decide (a = b))] and it will simplify in both places. *)
cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 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, <<< 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 _ {_}. Arguments atomic_heap _ {_}.
...@@ -54,10 +56,28 @@ Notation "'ref' e" := (alloc e) : expr_scope. ...@@ -54,10 +56,28 @@ Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope. Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store e1 e2) : 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. 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. *) (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val := Definition primitive_alloc : val :=
λ: "v", ref "v". λ: "v", ref "v".
...@@ -65,8 +85,8 @@ Definition primitive_load : val := ...@@ -65,8 +85,8 @@ Definition primitive_load : val :=
λ: "l", !"l".