Commit bafeb112 authored by Ralf Jung's avatar Ralf Jung
Browse files

adjust to partial comparison operator

parent 90884c23
......@@ -257,8 +257,8 @@ Lemma tac_tp_cmpxchg_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l
IntoVal e1 v1
IntoVal e2 v2
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I
val_for_compare v' val_for_compare v1
vals_cmpxchg_compare_safe v' v1
v' v1
vals_compare_safe v' v1
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j fill K' (v', #false)%V)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3
envs_entails Δ3 (|={E1,E2}=> Q)
......@@ -301,7 +301,7 @@ Tactic Notation "tp_cmpxchg_fail" constr(j) :=
|iSolveTC
|iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '? ↦ ?'"
|try (simpl; congruence) (* v' ≠ v1 *)
|try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
|try heap_lang.proofmode.solve_vals_compare_safe
|pm_reflexivity || fail "tp_cmpxchg_fail: this should not happen"
|(* new goal *)]).
......@@ -313,8 +313,8 @@ Lemma tac_tp_cmpxchg_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l
IntoVal e1 v1
IntoVal e2 v2
envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I
val_for_compare v' = val_for_compare v1
vals_cmpxchg_compare_safe v' v1
v' = v1
vals_compare_safe v' v1
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j fill K' (v', #true)%V)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3
envs_entails Δ3 (|={E1,E2}=> Q)
......@@ -357,7 +357,7 @@ Tactic Notation "tp_cmpxchg_suc" constr(j) :=
|iSolveTC
|iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? ↦ ?'"
|try (simpl; congruence) (* v' = v1 *)
|try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
|try heap_lang.proofmode.solve_vals_compare_safe
|pm_reflexivity || fail "tp_cmpxchg_suc: this should not happen"
|(* new goal *)]).
......
......@@ -102,7 +102,7 @@ Tactic Notation "rel_apply_l" open_constr(lem) :=
end));
try lazymatch goal with
| |- val_is_unboxed _ => fast_done
| |- vals_cmpxchg_compare_safe _ _ =>
| |- vals_compare_safe _ _ =>
fast_done || (left; fast_done) || (right; fast_done)
end;
try rel_finish.
......@@ -174,7 +174,7 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
eapply (tac_rel_pure_l K e');
[reflexivity (** e = fill K e1 *)
|iSolveTC (** PureClosed ϕ e1 e2 *)
|try fast_done (** φ *)
|try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
|first [left; split; reflexivity (** Here we decide if the mask E is ⊤ *)
| right; reflexivity] (** (m = n ∧ E = ⊤) ∨ (m = 0) *)
|iSolveTC (** IntoLaters *)
......@@ -191,7 +191,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
eapply (tac_rel_pure_r K e');
[reflexivity (** e = fill K e1 *)
|iSolveTC (** PureClosed ϕ e1 e2 *)
|try fast_done (** φ *)
|try heap_lang.proofmode.solve_vals_compare_safe (** φ *)
|solve_ndisj || fail 1 "rel_pure_r: cannot solve ↑specN ⊆ ?"
|simpl; reflexivity (** eres = fill K e2 *)
|rel_finish (** new goal *)])
......@@ -438,8 +438,8 @@ Lemma tac_rel_cmpxchg_fail_r `{relocG Σ} K ℶ1 i1 E (l : loc) e1 e2 v1 v2 v e
IntoVal e2 v2
nclose specN E
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
val_for_compare v val_for_compare v1
vals_cmpxchg_compare_safe v v1
v v1
vals_compare_safe v v1
eres = fill K (v, #false)%V
envs_entails 1 (refines E t eres A)
envs_entails 1 (refines E t e A).
......@@ -457,8 +457,8 @@ Lemma tac_rel_cmpxchg_suc_r `{relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) e1 e2 v1 v2
IntoVal e2 v2
nclose specN E
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
val_for_compare v = val_for_compare v1
vals_cmpxchg_compare_safe v v1
v = v1
vals_compare_safe v v1
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v2)) 1 = Some 2
eres = fill K (v, #true)%V
envs_entails 2 (refines E t eres A)
......@@ -489,7 +489,7 @@ Tactic Notation "rel_cmpxchg_fail_r" :=
[solve_ndisj || fail "rel_cmpxchg_fail_r: cannot prove 'nclose specN ⊆ ?'"
|solve_mapsto ()
|try (simpl; congruence) (** v ≠ v1 *)
|try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
|try heap_lang.proofmode.solve_vals_compare_safe
|reflexivity
|rel_finish (** new goal *)].
......@@ -510,7 +510,7 @@ Tactic Notation "rel_cmpxchg_suc_r" :=
[solve_ndisj || fail "rel_cmpxchg_suc_r: cannot prove 'nclose specN ⊆ ?'"
|solve_mapsto ()
|try (simpl; congruence) (** v = v1 *)
|try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
|try heap_lang.proofmode.solve_vals_compare_safe
|pm_reflexivity (** new env *)
|reflexivity
|rel_finish (** new goal *)].
......
......@@ -198,8 +198,8 @@ Section rules.
nclose specN E
IntoVal e1 v1
IntoVal e2 v2
vals_cmpxchg_compare_safe v v1
val_for_compare v val_for_compare v1
vals_compare_safe v v1
v v1
l ↦ₛ v -
(l ↦ₛ v - REL t << fill K (of_val (v, #false)) @ E : A)
- REL t << fill K (CmpXchg #l e1 e2) @ E : A.
......@@ -220,8 +220,8 @@ Section rules.
nclose specN E
IntoVal e1 v1
IntoVal e2 v2
vals_cmpxchg_compare_safe v v1
val_for_compare v = val_for_compare v1
vals_compare_safe v v1
v = v1
l ↦ₛ v -
(l ↦ₛ v2 - REL t << fill K (of_val (v, #true)) @ E : A)
- REL t << fill K (CmpXchg #l e1 e2) @ E : A.
......@@ -390,14 +390,14 @@ Section rules.
IntoVal e2 v2
val_is_unboxed v1
(|={,E}=> v', l v'
(val_for_compare v' val_for_compare v1 - (l v' - REL fill K (of_val (v', #false)) << t @ E : A))
(val_for_compare v' = val_for_compare v1 - (l v2 - REL fill K (of_val (v', #true)) << t @ E : A)))
(v' v1 - (l v' - REL fill K (of_val (v', #false)) << t @ E : A))
(v' = v1 - (l v2 - REL fill K (of_val (v', #true)) << t @ E : A)))
- REL fill K (CmpXchg #l e1 e2) << t : A.
Proof.
iIntros (<-<-?) "Hlog".
iApply refines_atomic_l; auto.
iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
destruct (decide (val_for_compare v' = val_for_compare v1)).
destruct (decide (v' = v1)).
- (* CmpXchg successful *) subst.
iApply (wp_cmpxchg_suc with "Hl"); eauto.
{ by right. }
......
......@@ -217,8 +217,8 @@ Section rules.
IntoVal e1 v1
IntoVal e2 v2
nclose specN E
vals_cmpxchg_compare_safe v' v1
val_for_compare v' val_for_compare v1
vals_compare_safe v' v1
v' v1
spec_ctx ρ j fill K (CmpXchg #l e1 e2) l ↦ₛ{q} v'
={E}= j fill K (v', #false)%V l ↦ₛ{q} v'.
Proof.
......@@ -243,8 +243,8 @@ Section rules.
IntoVal e1 v1
IntoVal e2 v2
nclose specN E
vals_cmpxchg_compare_safe v1' v1
val_for_compare v1' = val_for_compare v1
vals_compare_safe v1' v1
v1' = v1
spec_ctx ρ j fill K (CmpXchg #l e1 e2) l ↦ₛ v1'
={E}= j fill K (v1', #true)%V l ↦ₛ v2.
Proof.
......
......@@ -295,7 +295,7 @@ Section fundamental.
simplify_eq. rel_cmpxchg_l_atomic.
iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #Hv]]" "Hclose".
iModIntro. iExists _; iFrame. simpl.
destruct (decide (val_for_compare v1 = val_for_compare v2')) as [|Hneq]; subst.
destruct (decide (v1 = v2')) as [|Hneq]; subst.
- iSplitR; first by (iIntros (?); contradiction).
iIntros (?). iNext. iIntros "Hv1".
iDestruct (eq_type_sound with "Hv") as "%"; first fast_done.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment