Commit a78f1c3b authored by Robbert Krebbers's avatar Robbert Krebbers

Make atomic a type class.

parent 79bddd1a
...@@ -175,7 +175,7 @@ Proof. ...@@ -175,7 +175,7 @@ Proof.
f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym. f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
Qed. Qed.
Definition atomic (e : expr) := Definition is_atomic (e : expr) :=
match e with match e with
| Alloc e => bool_decide (is_Some (to_val e)) | Alloc e => bool_decide (is_Some (to_val e))
| Load e => bool_decide (is_Some (to_val e)) | Load e => bool_decide (is_Some (to_val e))
...@@ -187,7 +187,7 @@ Definition atomic (e : expr) := ...@@ -187,7 +187,7 @@ Definition atomic (e : expr) :=
| App (Rec _ _ (Lit _)) (Lit _) => true | App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false | _ => false
end. end.
Lemma atomic_correct e : atomic e language.atomic (to_expr e). Lemma is_atomic_correct e : is_atomic e Atomic (to_expr e).
Proof. Proof.
intros He. apply ectx_language_atomic. intros He. apply ectx_language_atomic.
- intros σ e' σ' ef Hstep; simpl in *. - intros σ e' σ' ef Hstep; simpl in *.
...@@ -228,13 +228,11 @@ Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances. ...@@ -228,13 +228,11 @@ Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
Ltac solve_atomic := Ltac solve_atomic :=
match goal with match goal with
| |- language.atomic ?e => | |- Atomic ?e =>
let e' := W.of_expr e in change (language.atomic (W.to_expr e')); let e' := W.of_expr e in change (Atomic (W.to_expr e'));
apply W.atomic_correct; vm_compute; exact I apply W.is_atomic_correct; vm_compute; exact I
end. end.
Hint Extern 10 (language.atomic _) => solve_atomic. Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
(* For the side-condition of elim_upd_fupd_wp_atomic *)
Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
(** Substitution *) (** Substitution *)
Ltac simpl_subst := Ltac simpl_subst :=
......
...@@ -118,7 +118,7 @@ Section ectx_language. ...@@ -118,7 +118,7 @@ Section ectx_language.
Lemma ectx_language_atomic e : Lemma ectx_language_atomic e :
( σ e' σ' efs, head_step e σ e' σ' efs irreducible e' σ') ( σ e' σ' efs, head_step e σ e' σ' efs irreducible e' σ')
sub_values e sub_values e
atomic e. Atomic e.
Proof. Proof.
intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep]. intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
assert (K = empty_ectx) as -> by eauto 10 using val_stuck. assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
......
...@@ -58,7 +58,7 @@ Proof. ...@@ -58,7 +58,7 @@ Proof.
Qed. Qed.
Lemma ht_atomic E1 E2 P P' Φ Φ' e : Lemma ht_atomic E1 E2 P P' Φ Φ' e :
atomic e Atomic e
(P ={E1,E2}=> P') {{ P' }} e @ E2 {{ Φ' }} ( v, Φ' v ={E2,E1}=> Φ v) (P ={E1,E2}=> P') {{ P' }} e @ E2 {{ Φ' }} ( v, Φ' v ={E2,E1}=> Φ v)
{{ P }} e @ E1 {{ Φ }}. {{ P }} e @ E1 {{ Φ }}.
Proof. Proof.
......
...@@ -58,15 +58,15 @@ Section language. ...@@ -58,15 +58,15 @@ Section language.
stronger sense defined below, and we have to be able to open invariants stronger sense defined below, and we have to be able to open invariants
around that expression. See `CasStuckS` in around that expression. See `CasStuckS` in
[lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *) [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
Definition atomic (e : expr Λ) : Prop := Class Atomic (e : expr Λ) : Prop :=
σ e' σ' efs, prim_step e σ e' σ' efs irreducible e' σ'. atomic σ e' σ' efs : prim_step e σ e' σ' efs irreducible e' σ'.
(* To open invariants with a WP that does not ensure safety, we need a (* To open invariants with a WP that does not ensure safety, we need a
stronger form of atomicity. With the above definition, in case `e` reduces stronger form of atomicity. With the above definition, in case `e` reduces
to a stuck non-value, there is no proof that the invariants have been to a stuck non-value, there is no proof that the invariants have been
established again. *) established again. *)
Definition strongly_atomic (e : expr Λ) : Prop := Class StronglyAtomic (e : expr Λ) : Prop :=
σ e' σ' efs, prim_step e σ e' σ' efs is_Some (to_val e'). strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs is_Some (to_val e').
Inductive step (ρ1 ρ2 : cfg Λ) : Prop := Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 efs t1 t2 : | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
...@@ -87,9 +87,8 @@ Section language. ...@@ -87,9 +87,8 @@ Section language.
Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Lemma strongly_atomic_atomic e : Lemma strongly_atomic_atomic e : StronglyAtomic e Atomic e.
strongly_atomic e atomic e. Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
Proof. unfold strongly_atomic, atomic. eauto using val_irreducible. Qed.
Lemma reducible_fill `{LanguageCtx Λ K} e σ : Lemma reducible_fill `{LanguageCtx Λ K} e σ :
to_val e = None reducible (K e) σ reducible e σ. to_val e = None reducible (K e) σ reducible e σ.
......
...@@ -147,7 +147,7 @@ Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}. ...@@ -147,7 +147,7 @@ Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed. Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
Lemma wp_atomic E1 E2 e Φ : Lemma wp_atomic E1 E2 e Φ :
atomic e Atomic e
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) WP e @ E1 {{ Φ }}. (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) WP e @ E1 {{ Φ }}.
Proof. Proof.
iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre. iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
...@@ -285,10 +285,8 @@ Section proofmode_classes. ...@@ -285,10 +285,8 @@ Section proofmode_classes.
(* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *) (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ : Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e Atomic e
ElimModal (|={E1,E2}=> P) P ElimModal (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100. (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed. Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes. End proofmode_classes.
Hint Extern 0 (atomic _) => assumption : typeclass_instances.
...@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these ...@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
mask changing update modalities directly in our proofs, but in this file we use mask changing update modalities directly in our proofs, but in this file we use
the first prove the rule as a lemma, and then use that. *) the first prove the rule as a lemma, and then use that. *)
Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ : Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
nclose N E atomic e nclose N E Atomic e
inv N P ( P - WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}. inv N P ( P - WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}.
Proof. Proof.
iIntros (??) "[#Hinv Hwp]". iIntros (??) "[#Hinv Hwp]".
......
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