Commit 6e79f000 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/eq' into 'master'

heap_lang: Make binary "=" operator partial, to sync with CmpXchg

Closes #248

See merge request iris/iris!283
parents 1ee1d9f9 cb27aa7f
Pipeline #18143 failed with stage
in 0 seconds
...@@ -76,8 +76,9 @@ Section tests. ...@@ -76,8 +76,9 @@ Section tests.
Definition heap_e6 : val := λ: "v", "v" = "v". Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I. Lemma heap_e6_spec (v : val) :
Proof. wp_lam. wp_op. by case_bool_decide. Qed. val_is_unboxed v (WP heap_e6 v {{ w, w = #true }})%I.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1. Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
......
...@@ -61,7 +61,7 @@ Open Scope Z_scope. ...@@ -61,7 +61,7 @@ Open Scope Z_scope.
Definition proph_id := positive. Definition proph_id := positive.
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitErased
| LitLoc (l : loc) | LitProphecy (p: proph_id). | LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set := Inductive un_op : Set :=
| NegOp | MinusUnOp. | NegOp | MinusUnOp.
...@@ -151,38 +151,33 @@ Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61 ...@@ -151,38 +151,33 @@ 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 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 read and written. Also notice that the sets of boxed and unboxed values are
disjoint. *) disjoint. *)
Definition lit_is_unboxed (l: base_lit) : Prop :=
match l with
(** Disallow comparing (erased) prophecies with (erased) prophecies, by
considering them boxed. *)
| LitProphecy _ | LitErased => False
| _ => True
end.
Definition val_is_unboxed (v : val) : Prop := Definition val_is_unboxed (v : val) : Prop :=
match v with match v with
| LitV _ => True | LitV l => lit_is_unboxed l
| InjLV (LitV _) => True | InjLV (LitV l) => lit_is_unboxed l
| InjRV (LitV _) => True | InjRV (LitV l) => lit_is_unboxed l
| _ => False | _ => False
end. end.
(** CmpXchg just compares the word-sized representation of two values, it cannot Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
look into boxed data. This works out fine if at least one of the to-be-compared Proof. destruct l; simpl; exact (decide _). Defined.
Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
(** We just compare the word-sized representation of two values, without looking
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_cmpxchg_compare_safe (vl v1 : val) : Prop := Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1. val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cmpxchg_compare_safe !_ !_ /. Arguments vals_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. *) (** The state: heaps of vals. *)
Record state : Type := { Record state : Type := {
...@@ -263,12 +258,18 @@ Proof. solve_decision. Defined. ...@@ -263,12 +258,18 @@ Proof. solve_decision. Defined.
Instance base_lit_countable : Countable base_lit. Instance base_lit_countable : Countable base_lit.
Proof. Proof.
refine (inj_countable' (λ l, match l with refine (inj_countable' (λ l, match l with
| LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None) | LitInt n => (inl (inl n), None)
| LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None) | LitBool b => (inl (inr b), None)
| LitProphecy p => (inr (inl ()), Some p) | LitUnit => (inr (inl false), None)
| LitErased => (inr (inl true), None)
| LitLoc l => (inr (inr l), None)
| LitProphecy p => (inr (inl false), Some p)
end) (λ l, match l with end) (λ l, match l with
| (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b | (inl (inl n), None) => LitInt n
| (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l | (inl (inr b), None) => LitBool b
| (inr (inl false), None) => LitUnit
| (inr (inl true), None) => LitErased
| (inr (inr l), None) => LitLoc l
| (_, Some p) => LitProphecy p | (_, Some p) => LitProphecy p
end) _); by intros []. end) _); by intros [].
Qed. Qed.
...@@ -519,7 +520,10 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := ...@@ -519,7 +520,10 @@ 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]! *) (* Crucially, this compares the same way as [CmpXchg]! *)
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2) if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
else else
match v1, v2 with match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2 | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
...@@ -635,10 +639,10 @@ Inductive head_step : expr → state → list observation → expr → state → ...@@ -635,10 +639,10 @@ 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]> σ)
[] []
| CmpXchgS l v1 v2 vl σ b : | CmpXchgS l v1 v2 vl σ b :
vals_cmpxchg_compare_safe vl v1
σ.(heap) !! l = Some vl σ.(heap) !! l = Some vl
(* Crucially, this compares the same way as [EqOp]! *) (* Crucially, this compares the same way as [EqOp]! *)
b = bool_decide (val_for_compare vl = val_for_compare v1) vals_compare_safe vl v1
b = bool_decide (vl = v1)
head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[] []
(Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ) (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
......
...@@ -37,8 +37,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -37,8 +37,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
cmpxchg_spec (l : loc) (w1 w2 : val) : cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 val_is_unboxed w1
<<< v, mapsto l 1 v >>> cmpxchg #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 (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>; RET (v, #if decide (v = w1) then true else false) >>>;
}. }.
Arguments atomic_heap _ {_}. Arguments atomic_heap _ {_}.
...@@ -68,8 +68,8 @@ Section derived. ...@@ -68,8 +68,8 @@ Section derived.
Lemma cas_spec (l : loc) (w1 w2 : val) : Lemma cas_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 >>> CAS #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 (v = 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 #if decide (v = w1) then true else false >>>.
Proof. Proof.
iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done. iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
iApply (aacc_aupd_commit with "AU"); first done. iApply (aacc_aupd_commit with "AU"); first done.
...@@ -119,12 +119,12 @@ Section proof. ...@@ -119,12 +119,12 @@ Section proof.
val_is_unboxed w1 val_is_unboxed w1
<<< (v : val), l v >>> <<< (v : val), l v >>>
primitive_cmpxchg #l w1 w2 @ primitive_cmpxchg #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then l w2 else l v, <<< if decide (v = w1) then l w2 else l v,
RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>. RET (v, #if decide (v = w1) then true else false) >>>.
Proof. Proof.
iIntros (? Φ) "AU". wp_lam. wp_pures. iIntros (? Φ) "AU". wp_lam. wp_pures.
iMod "AU" as (v) "[H↦ [_ Hclose]]". iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne]; destruct (decide (v = w1)) as [Heq|Hne];
[wp_cmpxchg_suc|wp_cmpxchg_fail]; [wp_cmpxchg_suc|wp_cmpxchg_fail];
iMod ("Hclose" with "H↦") as "HΦ"; done. iMod ("Hclose" with "H↦") as "HΦ"; done.
Qed. Qed.
......
...@@ -161,8 +161,19 @@ Instance pure_unop op v v' : ...@@ -161,8 +161,19 @@ Instance pure_unop op v v' :
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_binop op v1 v2 v' : Instance pure_binop op v1 v2 v' :
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v'). PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
(* Higher-priority instance for EqOp. *)
Instance pure_eqop v1 v2 :
PureExec (vals_compare_safe v1 v2) 1
(BinOp EqOp (Val v1) (Val v2))
(Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
rewrite /bin_op_eval /= decide_True //.
Qed.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1. Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
...@@ -375,7 +386,7 @@ Proof. ...@@ -375,7 +386,7 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_fail s E l q v' v1 v2 : Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1 v' v1 vals_compare_safe v' v1
{{{ l {q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ l {q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool false); l {q} v' }}}. {{{ RET PairV v' (LitV $ LitBool false); l {q} v' }}}.
Proof. Proof.
...@@ -386,7 +397,7 @@ Proof. ...@@ -386,7 +397,7 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ". iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed. Qed.
Lemma twp_cmpxchg_fail s E l q v' v1 v2 : Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1 v' v1 vals_compare_safe v' v1
[[{ l {q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l {q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool false); l {q} v' }]]. [[{ RET PairV v' (LitV $ LitBool false); l {q} v' }]].
Proof. Proof.
...@@ -398,7 +409,7 @@ Proof. ...@@ -398,7 +409,7 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_suc s E l v1 v2 v' : Lemma wp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cmpxchg_compare_safe v' v1 v' = v1 vals_compare_safe v' v1
{{{ l v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ l v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool true); l v2 }}}. {{{ RET PairV v' (LitV $ LitBool true); l v2 }}}.
Proof. Proof.
...@@ -410,7 +421,7 @@ Proof. ...@@ -410,7 +421,7 @@ Proof.
iModIntro. iSplit=>//. iFrame. by iApply "HΦ". iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed. Qed.
Lemma twp_cmpxchg_suc s E l v1 v2 v' : Lemma twp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cmpxchg_compare_safe v' v1 v' = v1 vals_compare_safe v' v1
[[{ l v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool true); l v2 }]]. [[{ RET PairV v' (LitV $ LitBool true); l v2 }]].
Proof. Proof.
...@@ -534,7 +545,7 @@ Proof. ...@@ -534,7 +545,7 @@ Proof.
Qed. Qed.
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v : Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
vals_cmpxchg_compare_safe v1 v1 vals_compare_safe v1 v1
{{{ proph p pvs l v1 }}} {{{ proph p pvs l v1 }}}
Resolve (CmpXchg #l v1 v2) #p v @ s; E Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v1, #true) ; pvs', pvs = ((v1, #true)%V, v)::pvs' proph p pvs' l v2 }}}. {{{ RET (v1, #true) ; pvs', pvs = ((v1, #true)%V, v)::pvs' proph p pvs' l v2 }}}.
...@@ -547,7 +558,7 @@ Proof. ...@@ -547,7 +558,7 @@ Proof.
Qed. Qed.
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v : Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1 v' v1 vals_compare_safe v' v1
{{{ proph p pvs l {q} v' }}} {{{ proph p pvs l {q} v' }}}
Resolve (CmpXchg #l v1 v2) #p v @ s; E Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v', #false) ; pvs', pvs = ((v', #false)%V, v)::pvs' proph p pvs' l {q} v' }}}. {{{ RET (v', #false) ; pvs', pvs = ((v', #false)%V, v)::pvs' proph p pvs' l {q} v' }}}.
...@@ -582,7 +593,7 @@ Proof. ...@@ -582,7 +593,7 @@ Proof.
Qed. Qed.
Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) : Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
{{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}. {{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed. Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_store_offset s E l off vs v : Lemma wp_store_offset s E l off vs v :
...@@ -604,8 +615,8 @@ Qed. ...@@ -604,8 +615,8 @@ Qed.
Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 : Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
vs !! off = Some v' vs !! off = Some v'
val_for_compare v' = val_for_compare v1 v' = v1
vals_cmpxchg_compare_safe v' v1 vals_compare_safe v' v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}. {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
...@@ -617,8 +628,8 @@ Proof. ...@@ -617,8 +628,8 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
val_for_compare (vs !!! off) = val_for_compare v1 vs !!! off = v1
vals_cmpxchg_compare_safe (vs !!! off) v1 vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}. {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
...@@ -629,8 +640,8 @@ Qed. ...@@ -629,8 +640,8 @@ Qed.
Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 : Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
vs !! off = Some v0 vs !! off = Some v0
val_for_compare v0 val_for_compare v1 v0 v1
vals_cmpxchg_compare_safe v0 v1 vals_compare_safe v0 v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v0, #false); l ↦∗ vs }}}. {{{ RET (v0, #false); l ↦∗ vs }}}.
...@@ -644,8 +655,8 @@ Proof. ...@@ -644,8 +655,8 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
val_for_compare (vs !!! off) val_for_compare v1 vs !!! off v1
vals_cmpxchg_compare_safe (vs !!! off) v1 vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #false); l ↦∗ vs }}}. {{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
......
...@@ -65,6 +65,12 @@ Ltac wp_finish := ...@@ -65,6 +65,12 @@ Ltac wp_finish :=
pm_prettify. (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and pm_prettify. (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
λs caused by wp_value *) λs caused by wp_value *)
Ltac solve_vals_compare_safe :=
(* The first branch is for when we have [vals_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).
(** The argument [efoc] can be used to specify the construct that should be (** The argument [efoc] can be used to specify the construct that should be
reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search
for an [EIf _ _ _] in the expression, and reduce it. for an [EIf _ _ _] in the expression, and reduce it.
...@@ -81,7 +87,7 @@ Tactic Notation "wp_pure" open_constr(efoc) := ...@@ -81,7 +87,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
unify e' efoc; unify e' efoc;
eapply (tac_wp_pure _ _ _ _ (fill K e')); eapply (tac_wp_pure _ _ _ _ (fill K e'));
[iSolveTC (* PureExec *) [iSolveTC (* PureExec *)
|try fast_done (* The pure condition for PureExec *) |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
|iSolveTC (* IntoLaters *) |iSolveTC (* IntoLaters *)
|wp_finish (* new goal *) |wp_finish (* new goal *)
]) ])
...@@ -282,15 +288,15 @@ Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ : ...@@ -282,15 +288,15 @@ Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cmpxchg_compare_safe v v1 vals_compare_safe v v1
(val_for_compare v = val_for_compare v1 (v = v1
envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})) envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}))
(val_for_compare v val_for_compare v1 (v v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail. rewrite envs_entails_eq=> ???? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne]. destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -wp_bind. eapply wand_apply. - rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cmpxchg_suc; eauto. } { eapply wp_cmpxchg_suc; eauto. }
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl. rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
...@@ -303,15 +309,15 @@ Qed. ...@@ -303,15 +309,15 @@ Qed.
Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ : Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cmpxchg_compare_safe v v1 vals_compare_safe v v1
(val_for_compare v = val_for_compare v1 (v = v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])) envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]))
(val_for_compare v val_for_compare v1 (v v1
envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof. Proof.
rewrite envs_entails_eq=> ??? Hsuc Hfail. rewrite envs_entails_eq=> ??? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne]. destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -twp_bind. eapply wand_apply. - rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cmpxchg_suc; eauto. } { eapply twp_cmpxchg_suc; eauto. }
rewrite /= {1}envs_simple_replace_sound //; simpl. rewrite /= {1}envs_simple_replace_sound //; simpl.
...@@ -325,7 +331,7 @@ Qed. ...@@ -325,7 +331,7 @@ Qed.
Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ : Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I envs_lookup i Δ' = 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_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof. Proof.
...@@ -336,7 +342,7 @@ Proof. ...@@ -336,7 +342,7 @@ Proof.
Qed. Qed.
Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ : Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
envs_lookup i Δ = Some (false, l {q} v)%I envs_lookup i Δ = 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_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof. Proof.
...@@ -349,7 +355,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ : ...@@ -349,7 +355,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
val_for_compare v = val_for_compare v1 vals_cmpxchg_compare_safe v v1 v = v1 vals_compare_safe v v1
envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}) envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof. Proof.
...@@ -362,7 +368,7 @@ Qed. ...@@ -362,7 +368,7 @@ Qed.
Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ : Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
val_for_compare v = val_for_compare v1 vals_cmpxchg_compare_safe v v1 v = v1 vals_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]) envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]). envs_entails Δ (