diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index c0246453727e3d9baa9a73febe08a74cdbabce44..942c1aa93ebedde7266e52785607866515f6f2b5 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -68,11 +68,6 @@
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_compare_safe"
- : string
-The command has indeed failed with message:
-Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
"not_cas"
: string
The command has indeed failed with message:
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 54d46b46ef9bc01636f03c15603096acb829056e..61d0e81a54c0c4a08971ce95362fbfe68a682b4e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -166,13 +166,6 @@ End printing_tests.
Section error_tests.
Context `{heapG Σ}.
- Check "not_cas_compare_safe".
- Lemma not_cas_compare_safe (l : loc) (v : val) :
- l ↦ v -∗ WP CAS #l v v {{ _, True }}.
- Proof.
- iIntros "H↦". Fail wp_cas_suc.
- Abort.
-
Check "not_cas".
Lemma not_cas :
(WP #() {{ _, True }})%I.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 30eb83c697b0b4b27ef576356895d4b2c908c073..322bd54490fe69f05a26db3ee7e94a300992c254 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -68,9 +68,6 @@ Inductive expr :=
Bind Scope expr_scope with expr.
-Notation NONE := (InjL (Lit LitUnit)) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x ∈ X)
@@ -99,9 +96,6 @@ Inductive val :=
Bind Scope val_scope with val.
-Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
-Notation SOMEV x := (InjRV x) (only parsing).
-
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e => Rec f x e
@@ -122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=
| _ => None
end.
+(** We assume the following encoding of values to 64-bit words: The least 3
+significant bits of every word are a "tag", and we have 61 bits of payload,
+which is enough if all pointers are 8-byte-aligned (common on 64bit
+architectures). The tags have the following meaning:
+
+0: Payload is the data for a LitV (LitInt _).
+1: Payload is the data for a InjLV (LitV (LitInt _)).
+2: Payload is the data for a InjRV (LitV (LitInt _)).
+3: Payload is the data for a LitV (LitLoc _).
+4: Payload is the data for a InjLV (LitV (LitLoc _)).
+4: Payload is the data for a InjRV (LitV (LitLoc _)).
+6: Payload is one of the following finitely many values, which 61 bits are more
+ than enough to encode:
+ LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
+ LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
+7: Value is boxed, i.e., payload is a pointer to some read-only memory area on
+ the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
+ relevant data for those cases. However, the boxed representation is never
+ used if any of the above representations could be used.
+
+Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
+bits, this means every value is machine-word-sized and can hence be atomically
+read and written. Also notice that the sets of boxed and unboxed values are
+disjoint. *)
+Definition val_is_unboxed (v : val) : Prop :=
+ match v with
+ | LitV _ => True
+ | InjLV (LitV _) => True
+ | InjRV (LitV _) => True
+ | _ => False
+ end.
+
(** The state: heaps of vals. *)
Definition state := gmap loc val.
@@ -367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
| _, _ => None
end.
-(** Return whether it is possible to use CAS to compare vl (current value) with
-v1 (netest value).
-
-We assume the following encoding of values to 64-bit words: The least 3
-significant bits of every word are a "tag", and we have 61 bits of payload,
-which is enough if all pointers are 8-byte-aligned (commong on 64bit
-architectures). The tags have the following meaning:
-
-0: Payload is one of the following finitely many values, which 61 bits are more
- than enough to encode: LitV LitUnit, LitV (LitBool _), NONEV, SOMEV (LitV
- LitUnit), SOMEV (LitV (LitBool _)).
-1: Payload is the data for a LitV (LitInt _).
-2: Payload is the data for a SOMEV (LitV (LitInt _)).
-3: Payload is the data for a LitV (LitLoc _).
-4: Payload is the data for a SOMEV (LitV (LitLoc _)).
-5: Value is boxed, i.e., payload is a pointer to some read-only memory area on
- the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
- relevant data for those cases. However, the boxed representation is never
- used if any of the above representations could be used.
-6: Unused.
-7: Unused.
-
-Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
-bits, this means every value is machine-word-sized and can hence be atomically
-read and written. It also justifies the comparisons allowed for CAS: Whenever
-[vals_cas_compare_safe vl v1] holds, equality of the one-word representation of
-[vl] and [v1] is equivalent to equality of the abstract value represented. This
-is clear for [LitV _ == LitV _] and [SOMEV (LitV _) == SOMEV (LitV _)] because
-none of these are boxed. For [NONEV == v], we can't actually atomically load and
-compare the data for boxed values, but that's okay because we only have to know
-if they are equal to [NONEV] which is distinct from all boxed values.
- *)
+(** CAS just compares the word-sized representation of the 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 :=
- match vl, v1 with
- (* We allow comparing literals with each other, also when wrapped in a SOMEV. *)
- | LitV _, LitV _ => True
- | SOMEV (LitV _), SOMEV (LitV _) => True
- (* We allow comparing NONEV to anything. *)
- | NONEV, _ => True
- | _, NONEV => True
- (* We don't allow comparing anything else. *)
- | _, _ => False
- end.
-(** Just a sanity check. *)
-Lemma vals_cas_compare_safe_sym vl v1 :
- vals_cas_compare_safe vl v1 → vals_cas_compare_safe v1 vl.
-Proof. rewrite /vals_cas_compare_safe. repeat case_match; done. Qed.
+ val_is_unboxed vl ∨ val_is_unboxed v1.
+Arguments vals_cas_compare_safe !_ !_ /.
Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
| BetaS f x e1 e2 v2 e' σ :
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index d2db12190118428c6ce2cdb6dde671a1b563086f..b92acccd5269ddea4cb1e28a09d584c050e81c19 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -39,7 +39,8 @@ Section increment.
(* Prove the atomic shift for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦".
- iApply (aacc_intro with "[H↦]"); [solve_ndisj|simpl;by auto with iFrame|iSplit].
+ iApply (aacc_intro with "[H↦]"); [solve_ndisj| |iSplit].
+ { iFrame. simpl. auto. }
{ iIntros "[_ $] !> $ !> //". }
iIntros ([]) "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index d991e108db625e970de4409058fc7f4ea3f67786..f8ef7a58517e001c25d35b3bcbeccdcbc9714547 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -144,6 +144,12 @@ Notation "e1 || e2" :=
(If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
(** Notations for option *)
+Notation NONE := (InjL (Lit LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
+
+Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
+
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 17236f403ce7ba382d87045b2efb29ba50c42e59..a718a6633e79c147d1d472872cf1e220dd950eaf 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
[iSolveTC
|solve_mapsto ()
|try congruence
- |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+ |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
|simpl; try wp_value_head]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
@@ -415,7 +415,7 @@ Tactic Notation "wp_cas_fail" :=
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
[solve_mapsto ()
|try congruence
- |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+ |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
|wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
@@ -434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
[iSolveTC
|solve_mapsto ()
|try congruence
- |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
+ |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
|pm_reflexivity
|simpl; try wp_value_head]
| |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[solve_mapsto ()
|try congruence
- |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
+ |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
|pm_reflexivity
|wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'"