Commit ebf63295 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/eq' into 'master'

comparison: treat prophecies like unit and make all closures equal

See merge request iris/iris!270
parents 7a983818 0a39a2a6
......@@ -25,7 +25,7 @@ Section tests.
Qed.
Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
v' v1 vals_cas_compare_safe v' v1
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' }}}.
......
......@@ -159,6 +159,31 @@ Definition val_is_unboxed (v : val) : Prop :=
| _ => False
end.
(** CAS 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 :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
(** We don't compare the logical program values, but we first normalize them
to make sure that prophecies are treated like unit.
Also all functions become the same, but still distinct from anything else. *)
Definition lit_for_compare (l : base_lit) : base_lit :=
match l with
| LitProphecy p => LitUnit
| l => l
end.
Fixpoint val_for_compare (v : val) : val :=
match v with
| LitV l => LitV (lit_for_compare l)
| PairV v1 v2 => PairV (val_for_compare v1) (val_for_compare v2)
| InjLV v => InjLV (val_for_compare v)
| InjRV v => InjRV (val_for_compare v)
| RecV f x e => RecV BAnon BAnon (Val $ LitV $ LitUnit)
end.
(** The state: heaps of vals. *)
Record state : Type := {
heap: gmap loc val;
......@@ -492,21 +517,15 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
end.
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
| LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
| LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l + off)
| _, _ => None
end.
(** 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 :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
if decide (op = EqOp) then
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
| LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
| LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l + off)
| _, _ => None
end.
Definition state_upd_heap (f: gmap loc val gmap loc val) (σ: state) : state :=
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
......@@ -615,13 +634,15 @@ Inductive head_step : expr → state → list observation → expr → state →
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CasFailS l v1 v2 vl σ :
σ.(heap) !! l = Some vl vl v1
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 false) σ []
| CasSucS l v1 v2 σ :
σ.(heap) !! l = Some v1
vals_cas_compare_safe v1 v1
| 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]> σ)
......
......@@ -35,8 +35,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l w1 w2 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
<<< 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) >>>;
}.
Arguments atomic_heap _ {_}.
......@@ -99,12 +99,13 @@ Section proof.
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas #l w1 w2 @
<<< if decide (v = w1) then l w2 else l v,
RET #(if decide (v = w1) then true else false) >>>.
<<< 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) >>>.
Proof.
iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
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Φ"; done.
Qed.
End proof.
......
......@@ -68,7 +68,7 @@ Section increment.
rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
iModIntro. iExists _. iFrame "Hl". iSplit.
{ (* abort case *) iDestruct "Hclose" as "[? _]". done. }
iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
iIntros "!>". wp_if. by iApply "HΦ".
- iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
......@@ -92,7 +92,7 @@ Section increment.
iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !>".
wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !>".
......
......@@ -376,7 +376,7 @@ Proof.
Qed.
Lemma wp_cas_fail s E l q v' v1 v2 :
v' v1 vals_cas_compare_safe v' v1
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
......@@ -386,7 +386,7 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' v1 v2 :
v' v1 vals_cas_compare_safe v' v1
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
......@@ -396,23 +396,23 @@ Proof.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc s E l v1 v2 :
vals_cas_compare_safe v1 v1
{{{ l v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
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' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
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 %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
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 :
vals_cas_compare_safe v1 v1
[[{ l v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
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' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
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 %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
......
......@@ -283,12 +283,16 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}))
(v v1 envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}))
(val_for_compare v = val_for_compare v1
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}))
(val_for_compare v val_for_compare v1
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite envs_entails_eq=> ???? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
- rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_suc; eauto. }
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
- rewrite -wp_bind. eapply wand_apply.
......@@ -300,12 +304,16 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]))
(v v1 envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]))
(val_for_compare v = val_for_compare v1
envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]))
(val_for_compare v val_for_compare v1
envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
rewrite envs_entails_eq=> ??? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
- rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cas_suc; eauto. }
rewrite /= {1}envs_simple_replace_sound //; simpl.
apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
- rewrite -twp_bind. eapply wand_apply.
......@@ -317,7 +325,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
v v1 vals_cas_compare_safe v v1
val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
......@@ -328,7 +336,7 @@ Proof.
Qed.
Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
envs_lookup i Δ = Some (false, l {q} v)%I
v v1 vals_cas_compare_safe v v1
val_for_compare v val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
......@@ -341,26 +349,26 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
v = v1 val_is_unboxed v
val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??????; subst.
rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_suc; eauto. by left. }
{ eapply wp_cas_suc; eauto. }
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 v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
v = v1 val_is_unboxed v
val_for_compare v = val_for_compare v1 vals_cas_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=>?????; subst.
rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cas_suc; eauto. by left. }
{ eapply twp_cas_suc; eauto. }
rewrite envs_simple_replace_sound //; simpl.
rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
......@@ -522,6 +530,12 @@ Tactic Notation "wp_store" :=
| _ => fail "wp_store: not a 'wp'"
end.
Local Ltac solve_vals_cas_compare_safe :=
(* The first branch is for when we have [vals_cas_compare_safe] in the context.
The other two branches are for when either one of the branches reduces to
[True] or we have it in the context. *)
fast_done || (left; fast_done) || (right; fast_done).
Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
let solve_mapsto _ :=
let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
......@@ -535,7 +549,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|try solve_vals_cas_compare_safe
|intros H1; wp_finish
|intros H2; wp_finish]
| |- envs_entails _ (twp ?E ?e ?Q) =>
......@@ -544,7 +558,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
|fail 1 "wp_cas: cannot find 'CAS' in" e];
[solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|try solve_vals_cas_compare_safe
|intros H1; wp_finish
|intros H2; wp_finish]
| _ => fail "wp_cas: not a 'wp'"
......@@ -562,16 +576,16 @@ Tactic Notation "wp_cas_fail" :=
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
[iSolveTC
|solve_mapsto ()
|try congruence
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|try (simpl; congruence) (* value inequality *)
|try solve_vals_cas_compare_safe
|wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
[solve_mapsto ()
|try congruence
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|try (simpl; congruence) (* value inequality *)
|try solve_vals_cas_compare_safe
|wp_finish]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
......@@ -589,8 +603,8 @@ Tactic Notation "wp_cas_suc" :=
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
|try (simpl; congruence) (* value equality *)
|try solve_vals_cas_compare_safe
|wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
......@@ -598,8 +612,8 @@ Tactic Notation "wp_cas_suc" :=
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[solve_mapsto ()
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
|try (simpl; congruence) (* value equality *)
|try solve_vals_cas_compare_safe
|wp_finish]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
......
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