Merge branch 'ralf/cas' into 'gen_proofmode'

Make CAS slightly more realistic

See merge request FP/iris-coq!165

tests/heap_lang.ref

@@ -68,3 +68,13 @@
     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:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.

tests/heap_lang.v

@@ -161,5 +161,23 @@ Section printing_tests.
 
 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.
+  Proof.
+    Fail wp_cas_suc.
+  Abort.
+End error_tests.
+
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.

theories/heap_lang/lang.v

@@ -66,6 +66,9 @@ Inductive expr :=
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
   | FAA (e1 : expr) (e2 : expr).
 
+Notation NONE := (InjL (Lit LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
+
 Bind Scope expr_scope with expr.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
@@ -94,6 +97,9 @@ Inductive val :=
   | InjLV (v : val)
   | InjRV (v : val).
 
+Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
+
 Bind Scope val_scope with val.
 
 Fixpoint of_val (v : val) : expr :=
@@ -361,6 +367,23 @@ 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). *)
+Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
+  match vl, v1 with
+  | LitV _, LitV _ => True
+  (* We want to support CAS'ing [NONEV] to [SOMEV #l].  An implementation of
+  this is possible if literals have an invalid bit pattern that can be used to
+  represent NONE. *)
+  | NONEV, NONEV => True
+  | NONEV, SOMEV (LitV _) => True
+  | SOMEV (LitV _), NONEV => True
+  | _, _ => 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.
+
 Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :
      to_val e2 = Some v2 →
@@ -405,10 +428,12 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
+     vals_cas_compare_safe vl v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
+     vals_cas_compare_safe v1 v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
   | FaaS l i1 e2 i2 σ :
      to_val e2 = Some (LitV (LitInt i2)) →

theories/heap_lang/lib/atomic_heap.v

@@ -37,7 +37,7 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
     IntoVal e1 w1 → IntoVal e2 w2 →
     atomic_wp (cas (#l, e1, e2))%E
               ⊤ ⊤
-              (λ v, mapsto l 1 v)
+              (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ mapsto l 1 v)%I
               (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
               (λ v _, #(if decide (v = w1) then true else false)%V);
 }.
@@ -91,12 +91,12 @@ Section proof.
     IntoVal e1 w1 → IntoVal e2 w2 →
     atomic_wp (primitive_cas (#l, e1, e2))%E
               ⊤ ⊤
-              (λ v, l ↦ v)%I
+              (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ l ↦ v)%I
               (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
               (λ v _, #(if decide (v = w1) then true else false)%V).
   Proof.
     iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj.
-    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    iMod (aupd_acc with "AU") as (v) "[[% H↦] [_ Hclose]]"; first solve_ndisj.
     destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
   Qed.

theories/heap_lang/lib/increment.v

@@ -39,8 +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|done|iSplit].
-    { iIntros "$ !> $ !> //". }
+    iApply (aacc_intro with "[H↦]"); [solve_ndisj|simpl;by auto with iFrame|iSplit].
+    { iIntros "[_ $] !> $ !> //". }
     iIntros ([]) "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
     - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".

theories/heap_lang/lifting.v

@@ -185,22 +185,22 @@ Proof.
 Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
-  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → vals_cas_compare_safe v' v1 →
   {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
-  iIntros (<- [v2 <-] ? Φ) ">Hl HΦ".
+  iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' e1 v1 e2 :
-  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 → vals_cas_compare_safe v' v1 →
   [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
   [[{ RET LitV (LitBool false); l ↦{q} v' }]].
 Proof.
-  iIntros (<- [v2 <-] ? Φ) "Hl HΦ".
+  iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
@@ -208,11 +208,11 @@ Proof.
 Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
   {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
-  iIntros (<- <- Φ) ">Hl HΦ".
+  iIntros (<- <- ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
@@ -220,11 +220,11 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 Lemma twp_cas_suc s E l e1 v1 e2 v2 :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
   [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
   [[{ RET LitV (LitBool true); l ↦ v2 }]].
 Proof.
-  iIntros (<- <- Φ) "Hl HΦ".
+  iIntros (<- <- ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.

theories/heap_lang/notation.v

@@ -144,12 +144,6 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL #()) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
-Notation NONEV := (InjLV #()) (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.

theories/heap_lang/proofmode.v

@@ -224,18 +224,18 @@ Qed.
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ??????.
+  rewrite envs_entails_eq=> ???????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
-  envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 →
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
 Proof.
@@ -247,19 +247,19 @@ Qed.
 Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ???????; subst.
+  rewrite envs_entails_eq=> ????????; subst.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 →
+  envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
@@ -406,6 +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"
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -414,6 +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"
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
@@ -432,6 +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"
     |pm_reflexivity
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -441,6 +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"
     |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"