Commit 7952bca4 authored by Robbert Krebbers's avatar Robbert Krebbers

Make atomic a boolean predicate.

parent ebb20a1a
......@@ -342,15 +342,16 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr []) : Prop :=
Definition atomic (e: expr []) : bool :=
match e with
| Alloc e => is_Some (to_val e)
| Load e => is_Some (to_val e)
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| CAS e0 e1 e2 => is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2)
| Alloc e => bool_decide (is_Some (to_val e))
| Load e => bool_decide (is_Some (to_val e))
| Store e1 e2 => bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => True
| _ => False
| App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false
end.
(** Substitution *)
......@@ -449,7 +450,7 @@ Lemma val_stuck e1 σ1 e2 σ2 ef :
Proof. destruct 1; naive_solver. Qed.
Lemma atomic_not_val e : atomic e to_val e = None.
Proof. destruct e; naive_solver. Qed.
Proof. by destruct e. Qed.
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) is_Some (to_val e).
Proof.
......
......@@ -34,8 +34,8 @@ Proof.
rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[l [-> [Hl [-> ?]]]].
rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
rewrite -(of_to_val (Loc l) (LocV l)) // in Hl. apply of_val_inj in Hl.
by subst.
rewrite -(of_to_val (Loc l) (LocV l)) // in Hl.
by apply of_val_inj in Hl as ->.
Qed.
Lemma wp_load_pst E σ l v Φ :
......@@ -62,7 +62,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
?right_id //; last (by intros; inv_head_step; eauto);
simpl; split_and?; by eauto.
simpl; by eauto 10.
Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
......@@ -72,7 +72,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
(<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
simpl; split_and?; by eauto.
simpl; by eauto 10.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
......
......@@ -113,6 +113,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false.
......
......@@ -9,7 +9,7 @@ Class EctxLanguage (expr val ectx state : Type) := {
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
atomic : expr Prop;
atomic : expr bool;
head_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
......
......@@ -6,7 +6,7 @@ Structure language := Language {
state : Type;
of_val : val expr;
to_val : expr option val;
atomic : expr Prop;
atomic : expr bool;
prim_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
......
......@@ -57,12 +57,11 @@ Proof.
rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
rewrite (always_sep_dup (_ _)); apply sep_mono.
- apply forall_intro=>n. apply: always_intro. wp_let.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
rewrite (True_intro (inv _ _)) right_id.
apply wand_intro_r; rewrite sep_or_l; apply or_elim.
+ rewrite -wp_pvs.
wp eapply wp_cas_suc; rewrite /= ?to_of_val; eauto with I ndisj.
wp eapply wp_cas_suc; eauto with I ndisj.
rewrite (True_intro (heap_ctx _)) left_id.
ecancel [l _]%I; apply wand_intro_l.
rewrite (own_update); (* FIXME: canonical structures are not working *)
......@@ -72,14 +71,13 @@ Proof.
solve_sep_entails.
+ rewrite sep_exist_l; apply exist_elim=>m.
eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
eauto with I ndisj; strip_later.
ecancel [l _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
rewrite /one_shot_inv -or_intro_r -(exist_intro m).
solve_sep_entails.
- apply: always_intro. wp_seq.
wp_focus (Load (%l))%I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
apply wand_intro_r.
trans (heap_ctx heapN inv N (one_shot_inv γ l) v, l v
((v = InjLV #0 own γ OneShotPending)
......@@ -115,8 +113,7 @@ Proof.
rewrite [(w=_ _)%I]comm !assoc; apply const_elim_sep_r=>->.
(* FIXME: why do we need to fold? *)
wp_case; fold of_val. wp_let. wp_focus (Load (%l))%I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
rewrite (True_intro (inv _ _)) right_id.
apply wand_intro_r; rewrite sep_or_l; apply or_elim.
+ rewrite (True_intro (heap_ctx _)) (True_intro (l _)) !left_id.
......
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