From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Behaviors.v | 150 ++++++++++++++++ common/Events.v | 497 ++++++++++++++++++++++++++++------------------------- common/Smallstep.v | 303 +++++++++++++++++++++++++++++--- common/Values.v | 7 + 4 files changed, 698 insertions(+), 259 deletions(-) (limited to 'common') diff --git a/common/Behaviors.v b/common/Behaviors.v index ccb5749..454ea34 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -530,6 +530,156 @@ Qed. End BACKWARD_SIMULATIONS. +(** * Program behaviors for the "atomic" construction *) + +Section ATOMIC. + +Variable L: semantics. +Hypothesis Lwb: well_behaved_traces L. + +Remark atomic_finish: forall s t, output_trace t -> Star (atomic L) (t, s) t (E0, s). +Proof. + induction t; intros. + apply star_refl. + simpl in H; destruct H. eapply star_left; eauto. + simpl. apply atomic_step_continue; auto. simpl; auto. auto. +Qed. + +Lemma step_atomic_plus: + forall s1 t s2, Step L s1 t s2 -> Plus (atomic L) (E0,s1) t (E0,s2). +Proof. + intros. destruct t. + apply plus_one. simpl; apply atomic_step_silent; auto. + exploit Lwb; eauto. simpl; intros. + eapply plus_left. eapply atomic_step_start; eauto. eapply atomic_finish; eauto. auto. +Qed. + +Lemma star_atomic_star: + forall s1 t s2, Star L s1 t s2 -> Star (atomic L) (E0,s1) t (E0,s2). +Proof. + induction 1. apply star_refl. eapply star_trans with (s2 := (E0,s2)). + apply plus_star. eapply step_atomic_plus; eauto. eauto. auto. +Qed. + +Lemma atomic_forward_simulation: forward_simulation L (atomic L). +Proof. + set (ms := fun (s: state L) (ts: state (atomic L)) => ts = (E0,s)). + apply forward_simulation_plus with ms; intros. + auto. + exists (E0,s1); split. simpl; auto. red; auto. + red in H. subst s2. simpl; auto. + red in H0. subst s2. exists (E0,s1'); split. + apply step_atomic_plus; auto. red; auto. +Qed. + +Lemma atomic_star_star_gen: + forall ts1 t ts2, Star (atomic L) ts1 t ts2 -> + exists t', Star L (snd ts1) t' (snd ts2) /\ fst ts1 ** t' = t ** fst ts2. +Proof. + induction 1. + exists E0; split. apply star_refl. traceEq. + destruct IHstar as [t' [A B]]. + simpl in H; inv H; simpl in *. + exists t'; split. eapply star_left; eauto. auto. + exists (ev :: t0 ** t'); split. eapply star_left; eauto. rewrite B; auto. + exists t'; split. auto. rewrite B; auto. +Qed. + +Lemma atomic_star_star: + forall s1 t s2, Star (atomic L) (E0,s1) t (E0,s2) -> Star L s1 t s2. +Proof. + intros. exploit atomic_star_star_gen; eauto. intros [t' [A B]]. + simpl in *. replace t with t'. auto. subst; traceEq. +Qed. + +Lemma atomic_forever_silent_forever_silent: + forall s, Forever_silent (atomic L) s -> Forever_silent L (snd s). +Proof. + cofix COINDHYP; intros. inv H. inv H0. + apply forever_silent_intro with (snd (E0, s')). auto. apply COINDHYP; auto. +Qed. + +Remark star_atomic_output_trace: + forall s t t' s', + Star (atomic L) (E0, s) t (t', s') -> output_trace t'. +Proof. + assert (forall ts1 t ts2, Star (atomic L) ts1 t ts2 -> + output_trace (fst ts1) -> output_trace (fst ts2)). + induction 1; intros. auto. inv H; simpl in *. + apply IHstar. auto. + apply IHstar. exploit Lwb; eauto. + destruct H2. apply IHstar. auto. + intros. change t' with (fst (t',s')). eapply H; eauto. simpl; auto. +Qed. + +Lemma atomic_forever_reactive_forever_reactive: + forall s T, Forever_reactive (atomic L) (E0,s) T -> Forever_reactive L s T. +Proof. + assert (forall t s T, Forever_reactive (atomic L) (t,s) T -> + exists T', Forever_reactive (atomic L) (E0,s) T' /\ T = t *** T'). + induction t; intros. exists T; auto. + inv H. inv H0. congruence. simpl in H; inv H. + destruct (IHt s (t2***T0)) as [T' [A B]]. eapply star_forever_reactive; eauto. + exists T'; split; auto. simpl. congruence. + + cofix COINDHYP; intros. inv H0. destruct s2 as [t2 s2]. + destruct (H _ _ _ H3) as [T' [A B]]. + assert (Star (atomic L) (E0, s) (t**t2) (E0, s2)). + eapply star_trans. eauto. apply atomic_finish. eapply star_atomic_output_trace; eauto. auto. + replace (t *** T0) with ((t ** t2) *** T'). apply forever_reactive_intro with s2. + apply atomic_star_star; auto. destruct t; simpl in *; unfold E0 in *; congruence. + apply COINDHYP. auto. + subst T0; traceEq. +Qed. + +Theorem atomic_behaviors: + forall beh, program_behaves L beh <-> program_behaves (atomic L) beh. +Proof. + intros; split; intros. + (* L -> atomic L *) + exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto. + intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]]. + congruence. + subst beh. inv H. inv H1. + apply program_runs with (E0,s). simpl; auto. + apply state_goes_wrong with (E0,s'). apply star_atomic_star; auto. + red; intros; red; intros. inv H. eelim H3; eauto. eelim H3; eauto. + intros; red; intros. simpl in H. destruct H. eelim H4; eauto. + apply program_goes_initially_wrong. + intros; red; intros. simpl in H; destruct H. eelim H1; eauto. + (* atomic L -> L *) + inv H. + (* initial state defined *) + destruct s as [t s]. simpl in H0. destruct H0; subst t. + apply program_runs with s; auto. + inv H1. + (* termination *) + destruct s' as [t' s']. simpl in H2; destruct H2; subst t'. + econstructor. eapply atomic_star_star; eauto. auto. + (* silent divergence *) + destruct s' as [t' s']. + assert (t' = E0). inv H2. inv H1; auto. subst t'. + econstructor. eapply atomic_star_star; eauto. + change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto. + (* reactive divergence *) + econstructor. apply atomic_forever_reactive_forever_reactive. auto. + (* going wrong *) + destruct s' as [t' s']. + assert (t' = E0). + destruct t'; auto. eelim H2. simpl. apply atomic_step_continue. + eapply star_atomic_output_trace; eauto. + subst t'. econstructor. apply atomic_star_star; eauto. + red; intros; red; intros. destruct t0. + elim (H2 E0 (E0,s'0)). constructor; auto. + elim (H2 (e::nil) (t0,s'0)). constructor; auto. + intros; red; intros. elim (H3 r). simpl; auto. + (* initial state undefined *) + apply program_goes_initially_wrong. + intros; red; intros. elim (H0 (E0,s)); simpl; auto. +Qed. + +End ATOMIC. + (** * Additional results about infinite reduction sequences *) (** We now show that any infinite sequence of reductions is either of diff --git a/common/Events.v b/common/Events.v index 018314e..3d082a7 100644 --- a/common/Events.v +++ b/common/Events.v @@ -490,6 +490,59 @@ Qed. End MATCH_TRACES_INV. +(** An output trace is a trace composed only of output events, + that is, events that do not take any result from the outside world. *) + +Definition output_event (ev: event) : Prop := + match ev with + | Event_syscall _ _ _ => False + | Event_vload _ _ _ _ => False + | Event_vstore _ _ _ _ => True + | Event_annot _ _ => True + end. + +Fixpoint output_trace (t: trace) : Prop := + match t with + | nil => True + | ev :: t' => output_event ev /\ output_trace t' + end. + +(** * Semantics of volatile memory accesses *) + +Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := + match Genv.find_var_info ge b with + | None => false + | Some gv => gv.(gvar_volatile) + end. + +Inductive volatile_load (F V: Type) (ge: Genv.t F V): + memory_chunk -> mem -> block -> int -> trace -> val -> Prop := + | volatile_load_vol: forall chunk m b ofs id ev v, + block_is_volatile ge b = true -> + Genv.find_symbol ge id = Some b -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_load ge chunk m b ofs + (Event_vload chunk id ofs ev :: nil) + (Val.load_result chunk v) + | volatile_load_nonvol: forall chunk m b ofs v, + block_is_volatile ge b = false -> + Mem.load chunk m b (Int.unsigned ofs) = Some v -> + volatile_load ge chunk m b ofs E0 v. + +Inductive volatile_store (F V: Type) (ge: Genv.t F V): + memory_chunk -> mem -> block -> int -> val -> trace -> mem -> Prop := + | volatile_store_vol: forall chunk m b ofs id ev v, + block_is_volatile ge b = true -> + Genv.find_symbol ge id = Some b -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_store ge chunk m b ofs v + (Event_vstore chunk id ofs ev :: nil) + m + | volatile_store_nonvol: forall chunk m b ofs v m', + block_is_volatile ge b = false -> + Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> + volatile_store ge chunk m b ofs v E0 m'. + (** * Semantics of external functions *) (** For each external function, its behavior is defined by a predicate relating: @@ -530,12 +583,6 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := f b1 = None -> f' b1 = Some(b2, delta) -> ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. -Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := - match Genv.find_var_info ge b with - | None => false - | Some gv => gv.(gvar_volatile) - end. - Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := mk_extcall_properties { @@ -624,20 +671,34 @@ Record extcall_properties (sem: extcall_sem) Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | volatile_load_sem_vol: forall b ofs m id ev v, - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> - eventval_match ge ev (type_of_chunk chunk) v -> - volatile_load_sem chunk ge - (Vptr b ofs :: nil) m - (Event_vload chunk id ofs ev :: nil) - (Val.load_result chunk v) m - | volatile_load_sem_nonvol: forall b ofs m v, - block_is_volatile ge b = false -> - Mem.load chunk m b (Int.unsigned ofs) = Some v -> - volatile_load_sem chunk ge - (Vptr b ofs :: nil) m - E0 - v m. + | volatile_load_sem_intro: forall b ofs m t v, + volatile_load ge chunk m b ofs t v -> + volatile_load_sem chunk ge (Vptr b ofs :: nil) m t v m. + +Lemma volatile_load_preserved: + forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m b ofs t v, + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> + volatile_load ge1 chunk m b ofs t v -> + volatile_load ge2 chunk m b ofs t v. +Proof. + intros. inv H1; constructor; auto. + rewrite H0; auto. + rewrite H; auto. + eapply eventval_match_preserved; eauto. + rewrite H0; auto. +Qed. + +Lemma volatile_load_extends: + forall F V (ge: Genv.t F V) chunk m b ofs t v m', + volatile_load ge chunk m b ofs t v -> + Mem.extends m m' -> + exists v', volatile_load ge chunk m' b ofs t v' /\ Val.lessdef v v'. +Proof. + intros. inv H. + econstructor; split; eauto. econstructor; eauto. + exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. +Qed. Remark meminj_preserves_block_is_volatile: forall F V (ge: Genv.t F V) f b1 b2 delta, @@ -653,6 +714,35 @@ Proof. auto. Qed. +Lemma volatile_load_inject: + forall F V (ge: Genv.t F V) f chunk m b ofs t v b' ofs' m', + meminj_preserves_globals ge f -> + volatile_load ge chunk m b ofs t v -> + val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Mem.inject f m m' -> + exists v', volatile_load ge chunk m' b' ofs' t v' /\ val_inject f v v'. +Proof. + intros. inv H0. + inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H8 in EQ; inv EQ. + rewrite Int.add_zero. exists (Val.load_result chunk v0); split. + constructor; auto. + apply val_load_result_inject. eapply eventval_match_inject_2; eauto. + exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros [v' [A B]]. exists v'; split; auto. + constructor; auto. rewrite <- H3. inv H1. eapply meminj_preserves_block_is_volatile; eauto. +Qed. + +Lemma volatile_load_receptive: + forall F V (ge: Genv.t F V) chunk m b ofs t1 t2 v1, + volatile_load ge chunk m b ofs t1 v1 -> match_traces ge t1 t2 -> + exists v2, volatile_load ge chunk m b ofs t2 v2. +Proof. + intros. inv H; inv H0. + exploit eventval_match_valid; eauto. intros [A B]. + exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. + intros [v' EVM]. exists (Val.load_result chunk v'). constructor; auto. + exists v1; constructor; auto. +Qed. + Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) @@ -660,64 +750,36 @@ Lemma volatile_load_ok: Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. destruct H. + unfold proj_sig_res; simpl. inv H. inv H0. destruct chunk; destruct v; simpl; constructor. eapply Mem.load_type; eauto. (* arity *) - destruct H; simpl; auto. + inv H; inv H0; auto. (* symbols *) - destruct H1. - econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. - econstructor; eauto. + inv H1. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) - destruct H; auto. + inv H; auto. (* bounds *) - destruct H; auto. + inv H; auto. (* mem extends *) - destruct H. - inv H1. inv H8. inv H6. - exists (Val.load_result chunk v); exists m1'; intuition. - constructor; auto. - red; auto. - inv H1. inv H7. inv H5. - exploit Mem.load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. - econstructor; eauto. - red; auto. + inv H. inv H1. inv H6. inv H4. + exploit volatile_load_extends; eauto. intros [v' [A B]]. + exists v'; exists m1'; intuition. constructor; auto. red; auto. (* mem injects *) - destruct H0. - inv H2. inv H9. inv H7. - generalize H; intros [P [Q R]]. - exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ. - exists f; exists (Val.load_result chunk v); exists m1'; intuition. - rewrite Int.add_zero. constructor; auto. - apply val_load_result_inject. eapply eventval_match_inject_2; eauto. - red; auto. - red; auto. - red; intros. congruence. - inv H2. inv H8. - exploit Mem.loadv_inject; eauto. simpl. eauto. intros [v1 [A B]]. - inv H6; simpl in *. - exists f; exists v1; exists m1'; intuition. - econstructor; eauto. - rewrite <- H0. eapply meminj_preserves_block_is_volatile; eauto. - red; auto. - red; auto. - red; intros. congruence. + inv H0. inv H2. inv H7. inversion H5; subst. + exploit volatile_load_inject; eauto. intros [v' [A B]]. + exists f; exists v'; exists m1'; intuition. constructor; auto. + red; auto. red; auto. red; intros. congruence. (* trace length *) - inv H; simpl; omega. + inv H; inv H0; simpl; omega. (* receptive *) - inv H; inv H0. - exploit eventval_match_valid; eauto. intros [A B]. - exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. - intros [v' EVM]. exists (Val.load_result chunk v'); exists m1. - eapply volatile_load_sem_vol; eauto. - exists vres1; exists m1; eapply volatile_load_sem_nonvol; eauto. + inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. + exists v2; exists m1; constructor; auto. (* determ *) - inv H; inv H0; try congruence. + inv H; inv H0. inv H1; inv H7; try congruence. assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0. - exploit eventval_match_valid. eexact H3. intros [V1 T1]. - exploit eventval_match_valid. eexact H11. intros [V2 T2]. + exploit eventval_match_valid. eexact H2. intros [V1 T1]. + exploit eventval_match_valid. eexact H4. intros [V2 T2]. split. constructor; auto. congruence. intros EQ; inv EQ. assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0. @@ -728,31 +790,19 @@ Qed. Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | volatile_load_global_sem_vol: forall b m ev v, - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> - eventval_match ge ev (type_of_chunk chunk) v -> - volatile_load_global_sem chunk id ofs ge - nil m - (Event_vload chunk id ofs ev :: nil) - (Val.load_result chunk v) m - | volatile_load_global_sem_nonvol: forall b m v, - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false -> - Mem.load chunk m b (Int.unsigned ofs) = Some v -> - volatile_load_global_sem chunk id ofs ge - nil m - E0 - v m. + | volatile_load_global_sem_intro: forall b t v m, + Genv.find_symbol ge id = Some b -> + volatile_load ge chunk m b ofs t v -> + volatile_load_global_sem chunk id ofs ge nil m t v m. Remark volatile_load_global_charact: forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m', volatile_load_global_sem chunk id ofs ge vargs m t vres m' <-> exists b, Genv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. Proof. - intros; split. - intros. inv H; exists b; split; auto; constructor; auto. - intros [b [P Q]]. inv Q. - assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto. - econstructor; eauto. + intros; split. + intros. inv H. exists b; split; auto. constructor; auto. + intros [b [P Q]]. inv Q. econstructor; eauto. Qed. Lemma volatile_load_global_ok: @@ -762,117 +812,79 @@ Lemma volatile_load_global_ok: Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. destruct H. + unfold proj_sig_res; simpl. inv H. inv H1. destruct chunk; destruct v; simpl; constructor. eapply Mem.load_type; eauto. (* arity *) - destruct H; simpl; auto. + inv H; inv H1; auto. (* symbols *) - destruct H1. - econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. - econstructor; eauto. rewrite H; auto. + inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) - destruct H; auto. + inv H; auto. (* bounds *) - destruct H; auto. -(* mem extends *) - destruct H. - inv H1. - exists (Val.load_result chunk v); exists m1'; intuition. - econstructor; eauto. - red; auto. - inv H1. - exploit Mem.load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. - econstructor; eauto. - red; auto. -(* mem injects *) - destruct H0. - inv H2. - exists f; exists (Val.load_result chunk v); exists m1'; intuition. - econstructor; eauto. - apply val_load_result_inject. eapply eventval_match_inject_2; eauto. - red; auto. - red; auto. - red; intros. congruence. - inv H2. destruct H as [P [Q R]]. exploit P; eauto. intros EQ. - exploit Mem.load_inject; eauto. rewrite Zplus_0_r. intros [v1 [A B]]. - exists f; exists v1; exists m1'; intuition. - econstructor; eauto. - red; auto. - red; auto. - red; intros. congruence. + inv H; auto. +(* extends *) + inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. + exists v'; exists m1'; intuition. econstructor; eauto. red; auto. +(* inject *) + inv H0. inv H2. + assert (val_inject f (Vptr b ofs) (Vptr b ofs)). + exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto. + exploit volatile_load_inject; eauto. intros [v' [A B]]. + exists f; exists v'; exists m1'; intuition. econstructor; eauto. + red; auto. red; auto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. + inv H; inv H1; simpl; omega. (* receptive *) - inv H; inv H0. - exploit eventval_match_valid; eauto. intros [A B]. - exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. - intros [v' EVM]. exists (Val.load_result chunk v'); exists m1. - eapply volatile_load_global_sem_vol; eauto. - exists vres1; exists m1; eapply volatile_load_global_sem_nonvol; eauto. + inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. + exists v2; exists m1; econstructor; eauto. (* determ *) - inv H; inv H0; try congruence. - assert (b = b0) by congruence. subst b0. - exploit eventval_match_valid. eexact H3. intros [V1 T1]. - exploit eventval_match_valid. eexact H5. intros [V2 T2]. - split. constructor; auto. congruence. - intros EQ; inv EQ. - assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0. - auto. - split. constructor. intuition congruence. + rewrite volatile_load_global_charact in *. + destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. + rewrite A1 in A2; inv A2. + eapply ec_determ. eapply volatile_load_ok. eauto. eauto. Qed. (** ** Semantics of volatile stores *) Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | volatile_store_sem_vol: forall b ofs m id ev v, - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> - eventval_match ge ev (type_of_chunk chunk) v -> - volatile_store_sem chunk ge - (Vptr b ofs :: v :: nil) m - (Event_vstore chunk id ofs ev :: nil) - Vundef m - | volatile_store_sem_nonvol: forall b ofs m v m', - block_is_volatile ge b = false -> - Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> - volatile_store_sem chunk ge - (Vptr b ofs :: v :: nil) m - E0 - Vundef m'. + | volatile_store_sem_intro: forall b ofs m1 v t m2, + volatile_store ge chunk m1 b ofs v t m2 -> + volatile_store_sem chunk ge (Vptr b ofs :: v :: nil) m1 t Vundef m2. -Lemma volatile_store_ok: - forall chunk, - extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None). +Lemma volatile_store_preserved: + forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 b ofs v t m2, + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> + volatile_store ge1 chunk m1 b ofs v t m2 -> + volatile_store ge2 chunk m1 b ofs v t m2. Proof. - intros; constructor; intros. -(* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. -(* arity *) - inv H; simpl; auto. -(* symbols preserved *) - inv H1. - constructor. rewrite H; auto. rewrite H0; auto. eapply eventval_match_preserved; eauto. - constructor; auto. rewrite H0; auto. -(* valid block *) - inv H. auto. eauto with mem. -(* bounds *) - inv H. auto. eapply Mem.bounds_store; eauto. -(* mem extends*) - inv H. - inv H1. inv H6. inv H8. inv H7. - exists Vundef; exists m1'; intuition. - constructor; auto. eapply eventval_match_lessdef; eauto. - red; auto. - inv H1. inv H5. inv H7. inv H6. - exploit Mem.store_within_extends; eauto. intros [m' [A B]]. - exists Vundef; exists m'; intuition. - constructor; auto. + intros. inv H1; constructor; auto. + rewrite H0; auto. + rewrite H; auto. + eapply eventval_match_preserved; eauto. + rewrite H0; auto. +Qed. + +Lemma volatile_store_extends: + forall F V (ge: Genv.t F V) chunk m1 b ofs v t m2 m1' v', + volatile_store ge chunk m1 b ofs v t m2 -> + Mem.extends m1 m1' -> + Val.lessdef v v' -> + exists m2', + volatile_store ge chunk m1' b ofs v' t m2' + /\ Mem.extends m2 m2' + /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'. +Proof. + intros. inv H. + econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto. + split. auto. red; auto. + exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. + exists m2'; intuition. econstructor; eauto. red; split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H1. eapply Mem.load_store_other; eauto. + rewrite <- H4. eapply Mem.load_store_other; eauto. destruct (eq_block b0 b); auto. subst b0; right. exploit Mem.valid_access_in_bounds. eapply Mem.store_valid_access_3. eexact H3. @@ -883,30 +895,37 @@ Proof. (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)). red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega. simpl; omega. simpl; omega. -(* mem injects *) - inv H0. - inv H2. inv H7. inv H9. inv H10. - generalize H; intros [P [Q R]]. - exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ. - exists f; exists Vundef; exists m1'; intuition. - rewrite Int.add_zero. constructor; auto. - eapply eventval_match_inject; eauto. - red; auto. - red; auto. - red; intros; congruence. - inv H2. inv H8. inv H9. inv H6. +Qed. + +Lemma volatile_store_inject: + forall F V (ge: Genv.t F V) f chunk m1 b ofs v t m2 m1' b' ofs' v', + meminj_preserves_globals ge f -> + volatile_store ge chunk m1 b ofs v t m2 -> + val_inject f (Vptr b ofs) (Vptr b' ofs') -> + val_inject f v v' -> + Mem.inject f m1 m1' -> + exists m2', + volatile_store ge chunk m1' b' ofs' v' t m2' + /\ Mem.inject f m2 m2' + /\ mem_unchanged_on (loc_unmapped f) m1 m2 + /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'. +Proof. + intros. inv H0. + inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. + rewrite Int.add_zero. exists m1'. + split. constructor; auto. eapply eventval_match_inject; eauto. + split. auto. split. red; auto. red; auto. assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. - inv H4. - exists f; exists Vundef; exists m2'; intuition. - constructor; auto. rewrite <- H3. eapply meminj_preserves_block_is_volatile; eauto. + inv H1. exists m2'; intuition. + constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H4. eapply Mem.load_store_other; eauto. - left. exploit (H2 ofs0). generalize (size_chunk_pos chunk0). omega. + rewrite <- H6. eapply Mem.load_store_other; eauto. + left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. unfold loc_unmapped. congruence. split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H4. eapply Mem.load_store_other; eauto. - destruct (eq_block b0 b2); auto. subst b0; right. + rewrite <- H6. eapply Mem.load_store_other; eauto. + destruct (eq_block b0 b'); auto. subst b0; right. assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta). eapply Mem.address_inject; eauto with mem. unfold Mem.storev in A. rewrite EQ in A. rewrite EQ. @@ -917,16 +936,48 @@ Proof. generalize (size_chunk_pos chunk). intro G. apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)). - red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega. + red; intros. exploit (H1 x H7). eauto. unfold Intv.In; simpl. omega. simpl; omega. simpl; omega. - red; intros; congruence. +Qed. + +Lemma volatile_store_receptive: + forall F V (ge: Genv.t F V) chunk m b ofs v t1 m1 t2, + volatile_store ge chunk m b ofs v t1 m1 -> match_traces ge t1 t2 -> t1 = t2. +Proof. + intros. inv H; inv H0; auto. +Qed. + +Lemma volatile_store_ok: + forall chunk, + extcall_properties (volatile_store_sem chunk) + (mksignature (Tint :: type_of_chunk chunk :: nil) None). +Proof. + intros; constructor; intros. +(* well typed *) + unfold proj_sig_res; simpl. inv H; constructor. +(* arity *) + inv H; simpl; auto. +(* symbols preserved *) + inv H1. constructor. eapply volatile_store_preserved; eauto. +(* valid block *) + inv H. inv H1. auto. eauto with mem. +(* bounds *) + inv H. inv H1. auto. eapply Mem.bounds_store; eauto. +(* mem extends*) + inv H. inv H1. inv H6. inv H7. inv H4. + exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. + exists Vundef; exists m2'; intuition. constructor; auto. +(* mem inject *) + inv H0. inv H2. inv H7. inv H8. inversion H5; subst. + exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. + exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. + inv H; inv H0; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. - exists vres1; exists m1; congruence. + assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. + subst t2; exists vres1; exists m1; auto. (* determ *) - inv H; inv H0; try congruence. + inv H; inv H0. inv H1; inv H8; try congruence. assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0. assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. split. constructor. auto. @@ -936,20 +987,10 @@ Qed. Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | volatile_store_global_sem_vol: forall b m ev v, - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> - eventval_match ge ev (type_of_chunk chunk) v -> - volatile_store_global_sem chunk id ofs ge - (v :: nil) m - (Event_vstore chunk id ofs ev :: nil) - Vundef m - | volatile_store_global_sem_nonvol: forall b m v m', - Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false -> - Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> - volatile_store_global_sem chunk id ofs ge - (v :: nil) m - E0 - Vundef m'. + | volatile_store_global_sem_intro: forall b m1 v t m2, + Genv.find_symbol ge id = Some b -> + volatile_store ge chunk m1 b ofs v t m2 -> + volatile_store_global_sem chunk id ofs ge (v :: nil) m1 t Vundef m2. Remark volatile_store_global_charact: forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m', @@ -958,9 +999,7 @@ Remark volatile_store_global_charact: Proof. intros; split. intros. inv H; exists b; split; auto; econstructor; eauto. - intros [b [P Q]]. inv Q. - assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto. - econstructor; eauto. + intros [b [P Q]]. inv Q. econstructor; eauto. Qed. Lemma volatile_store_global_ok: @@ -974,13 +1013,11 @@ Proof. (* arity *) inv H; simpl; auto. (* symbols preserved *) - inv H1. - econstructor. rewrite H; eauto. rewrite H0; auto. eapply eventval_match_preserved; eauto. - econstructor; eauto. rewrite H; auto. + inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) - inv H. auto. eauto with mem. + inv H. inv H2. auto. eauto with mem. (* bounds *) - inv H. auto. eapply Mem.bounds_store; eauto. + inv H. inv H2. auto. eapply Mem.bounds_store; eauto. (* mem extends*) rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. @@ -995,16 +1032,14 @@ Proof. exists f'; exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. (* trace length *) - inv H; simpl; omega. + inv H. inv H1; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. + assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2. exists vres1; exists m1; congruence. (* determ *) - inv H; inv H0; try congruence. - assert (b = b0) by congruence. subst b0. - assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. - split. constructor. auto. - split. constructor. intuition congruence. + rewrite volatile_store_global_charact in *. + destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. rewrite A1 in A2; inv A2. + eapply ec_determ. eapply volatile_store_ok. eauto. eauto. Qed. (** ** Semantics of dynamic memory allocation (malloc) *) diff --git a/common/Smallstep.v b/common/Smallstep.v index 63ab5ea..458e8c6 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -817,12 +817,15 @@ End COMPOSE_SIMULATIONS. (** * Receptiveness and determinacy *) +Definition single_events (L: semantics) : Prop := + forall s t s', Step L s t s' -> (length t <= 1)%nat. + Record receptive (L: semantics) : Prop := Receptive { sr_receptive: forall s t1 s1 t2, Step L s t1 s1 -> match_traces (globalenv L) t1 t2 -> exists s2, Step L s t2 s2; - sr_traces: forall s t s', - Step L s t s' -> (length t <= 1)%nat + sr_traces: + single_events L }. Record determinate (L: semantics) : Prop := @@ -830,8 +833,8 @@ Record determinate (L: semantics) : Prop := sd_determ: forall s t1 s1 t2 s2, Step L s t1 s1 -> Step L s t2 s2 -> match_traces (globalenv L) t1 t2 /\ (t1 = t2 -> s1 = s2); - sd_traces: forall s t s', - Step L s t s' -> (length t <= 1)%nat; + sd_traces: + single_events L; sd_initial_determ: forall s1 s2, initial_state L s1 -> initial_state L s2 -> s1 = s2; sd_final_nostep: forall s r, @@ -925,8 +928,6 @@ Record backward_simulation (L1 L2: semantics) : Type := exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) /\ bsim_match_states i' s1' s2'; - bsim_traces: - forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat; bsim_symbols_preserved: forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id }. @@ -960,9 +961,6 @@ Variable L2: semantics. Hypothesis symbols_preserved: forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. -Hypothesis length_traces: - forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat. - Variable match_states: state L1 -> state L2 -> Prop. Hypothesis initial_states_exist: @@ -1085,6 +1083,7 @@ Section COMPOSE_BACKWARD_SIMULATIONS. Variable L1: semantics. Variable L2: semantics. Variable L3: semantics. +Hypothesis L3_single_events: single_events L3. Variable S12: backward_simulation L1 L2. Variable S23: backward_simulation L2 L3. @@ -1117,7 +1116,7 @@ Proof. intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]]. (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). - exploit bsim_traces; eauto. + exploit L3_single_events; eauto. destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. destruct EITHER. (* 1.1 these are silent transitions *) @@ -1202,8 +1201,6 @@ Proof. eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. (* simulation *) exact bb_simulation. -(* trace length *) - exact (bsim_traces S23). (* symbols *) intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto. Qed. @@ -1217,9 +1214,8 @@ Section FORWARD_TO_BACKWARD. Variable L1: semantics. Variable L2: semantics. Variable FS: forward_simulation L1 L2. - -Hypothesis receptive: receptive L1. -Hypothesis determinate: determinate L2. +Hypothesis L1_receptive: receptive L1. +Hypothesis L2_determinate: determinate L2. (** Exploiting forward simulation *) @@ -1391,7 +1387,7 @@ Proof. (* 1. At matching states *) exploit f2b_progress; eauto. intros TRANS; inv TRANS. (* 1.1 L1 can reach final state and L2 is at final state: impossible! *) - exploit (sd_final_nostep determinate); eauto. contradiction. + exploit (sd_final_nostep L2_determinate); eauto. contradiction. (* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *) inv H2. exploit f2b_determinacy_inv. eexact H5. eexact STEP2. @@ -1409,15 +1405,15 @@ Proof. right; split. auto. constructor. econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. (* 1.2.2 L2 makes a non-silent transition, and so does L1 *) - exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ]. + exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. subst t2. rewrite E0_right in H1. (* Use receptiveness to equate the traces *) - exploit (sr_receptive receptive); eauto. intros [s1''' STEP1]. + exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1]. exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. intros [i''' [s2''' [P Q]]]. inv P. (* Exploit determinacy *) - exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ]. + exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. subst t0. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. intros. elim NOT2. inv H8. auto. subst t2. rewrite E0_right in *. @@ -1436,17 +1432,17 @@ Proof. right; split. apply star_refl. constructor. omega. econstructor; eauto. eapply star_right; eauto. (* 2.2 L2 make a non-silent transition *) - exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ]. + exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. subst. rewrite E0_right in *. (* Use receptiveness to equate the traces *) - exploit (sr_receptive receptive); eauto. intros [s1''' STEP1]. + exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1]. exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. intros [i''' [s2''' [P Q]]]. (* Exploit determinacy *) exploit f2b_determinacy_star. eauto. eexact STEP2. auto. apply plus_star; eauto. intro R. inv R. congruence. - exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ]. + exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. subst. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. intros. elim NOT2. inv H7; auto. subst. rewrite E0_right in *. @@ -1482,11 +1478,11 @@ Proof. (* final states *) intros. inv H. exploit f2b_progress; eauto. intros TRANS; inv TRANS. - assert (r0 = r) by (eapply (sd_final_determ determinate); eauto). subst r0. + assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0. exists s1'; auto. - inv H4. exploit (sd_final_nostep determinate); eauto. contradiction. - inv H5. congruence. exploit (sd_final_nostep determinate); eauto. contradiction. - inv H2. exploit (sd_final_nostep determinate); eauto. contradiction. + inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction. + inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction. + inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction. (* progress *) intros. inv H. exploit f2b_progress; eauto. intros TRANS; inv TRANS. @@ -1496,14 +1492,265 @@ Proof. inv H1. right; econstructor; econstructor; eauto. (* simulation *) exact f2b_simulation_step. -(* trace length *) - exact (sd_traces determinate). (* symbols preserved *) exact (fsim_symbols_preserved FS). Qed. End FORWARD_TO_BACKWARD. +(** * Transforming a semantics into a single-event, equivalent semantics *) + +Definition well_behaved_traces (L: semantics) : Prop := + forall s t s', Step L s t s' -> + match t with nil => True | ev :: t' => output_trace t' end. + +Section ATOMIC. + +Variable L: semantics. + +Hypothesis Lwb: well_behaved_traces L. + +Inductive atomic_step (ge: Genv.t (funtype L) (vartype L)): (trace * state L) -> trace -> (trace * state L) -> Prop := + | atomic_step_silent: forall s s', + Step L s E0 s' -> + atomic_step ge (E0, s) E0 (E0, s') + | atomic_step_start: forall s ev t s', + Step L s (ev :: t) s' -> + atomic_step ge (E0, s) (ev :: nil) (t, s') + | atomic_step_continue: forall ev t s, + output_trace (ev :: t) -> + atomic_step ge (ev :: t, s) (ev :: nil) (t, s). + +Definition atomic : semantics := {| + state := (trace * state L)%type; + funtype := funtype L; + vartype := vartype L; + step := atomic_step; + initial_state := fun s => initial_state L (snd s) /\ fst s = E0; + final_state := fun s r => final_state L (snd s) r /\ fst s = E0; + globalenv := globalenv L +|}. + +End ATOMIC. + +(** A forward simulation from a semantics [L1] to a single-event semantics [L2] + can be "factored" into a forward simulation from [atomic L1] to [L2]. *) + +Section FACTOR_FORWARD_SIMULATION. + +Variable L1: semantics. +Variable L2: semantics. +Variable sim: forward_simulation L1 L2. +Hypothesis L2single: single_events L2. + +Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop := + | ffs_match_at: forall i s1 s2, + sim i s1 s2 -> + ffs_match i (E0, s1) s2 + | ffs_match_buffer: forall i ev t s1 s2 s2', + Star L2 s2 (ev :: t) s2' -> sim i s1 s2' -> + ffs_match i (ev :: t, s1) s2. + +Lemma star_non_E0_split': + forall s2 t s2', Star L2 s2 t s2' -> + match t with + | nil => True + | ev :: t' => exists s2x, Plus L2 s2 (ev :: nil) s2x /\ Star L2 s2x t' s2' + end. +Proof. + induction 1. simpl. auto. + exploit L2single; eauto. intros LEN. + destruct t1. simpl in *. subst. destruct t2. auto. + destruct IHstar as [s2x [A B]]. exists s2x; split; auto. + eapply plus_left. eauto. apply plus_star; eauto. auto. + destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto. + simpl in LEN. omegaContradiction. +Qed. + +Lemma ffs_simulation: + forall s1 t s1', Step (atomic L1) s1 t s1' -> + forall i s2, ffs_match i s1 s2 -> + exists i', exists s2', + (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i) + /\ ffs_match i' s1' s2'. +Proof. + induction 1; intros. +(* silent step *) + inv H0. + exploit (fsim_simulation sim); eauto. + intros [i' [s2' [A B]]]. + exists i'; exists s2'; split. auto. constructor; auto. +(* start step *) + inv H0. + exploit (fsim_simulation sim); eauto. + intros [i' [s2' [A B]]]. + destruct t as [ | ev' t]. + (* single event *) + exists i'; exists s2'; split. auto. constructor; auto. + (* multiple events *) + assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto. + exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. + exists i'; exists s2x; split. auto. econstructor; eauto. +(* continue step *) + inv H0. + exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. + destruct t. + exists i; exists s2'; split. left. eapply plus_star_trans; eauto. constructor; auto. + exists i; exists s2x; split. auto. econstructor; eauto. +Qed. + +Theorem factor_forward_simulation: + forward_simulation (atomic L1) L2. +Proof. + apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim). +(* wf *) + apply fsim_order_wf. +(* initial states *) + intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst. + exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]]. + exists i; exists s2; split; auto. constructor; auto. +(* final states *) + intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H. + eapply (fsim_match_final_states sim); eauto. +(* simulation *) + exact ffs_simulation. +(* symbols preserved *) + simpl. exact (fsim_symbols_preserved sim). +Qed. + +End FACTOR_FORWARD_SIMULATION. + +(** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2] + can be "factored" as a backward simulation from [L1] to [atomic L2]. *) + +Section FACTOR_BACKWARD_SIMULATION. + +Variable L1: semantics. +Variable L2: semantics. +Variable sim: backward_simulation L1 L2. +Hypothesis L1single: single_events L1. +Hypothesis L2wb: well_behaved_traces L2. + +Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop := + | fbs_match_intro: forall i s1 t s2 s1', + Star L1 s1 t s1' -> sim i s1' s2 -> + t = E0 \/ output_trace t -> + fbs_match i s1 (t, s2). + +Lemma fbs_simulation: + forall s2 t s2', Step (atomic L2) s2 t s2' -> + forall i s1, fbs_match i s1 s2 -> safe L1 s1 -> + exists i', exists s1', + (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i)) + /\ fbs_match i' s1' s2'. +Proof. + induction 1; intros. +(* silent step *) + inv H0. + exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. + intros [i' [s1'' [A B]]]. + exists i'; exists s1''; split. + destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto. + econstructor. apply star_refl. auto. auto. +(* start step *) + inv H0. + exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. + intros [i' [s1'' [A B]]]. + assert (C: Star L1 s1 (ev :: t) s1''). + eapply star_trans. eauto. destruct A as [P | [P Q]]. apply plus_star; eauto. eauto. auto. + exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]]. + exists i'; exists s1x; split. + left; auto. + econstructor; eauto. + exploit L2wb; eauto. +(* continue step *) + inv H0. unfold E0 in H8; destruct H8; try congruence. + exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]]. + exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto. +Qed. + +Lemma fbs_progress: + forall i s1 s2, + fbs_match i s1 s2 -> safe L1 s1 -> + (exists r, final_state (atomic L2) s2 r) \/ + (exists t, exists s2', Step (atomic L2) s2 t s2'). +Proof. + intros. inv H. destruct t. +(* 1. no buffered events *) + exploit (bsim_progress sim); eauto. eapply star_safe; eauto. + intros [[r A] | [t [s2' A]]]. +(* final state *) + left; exists r; simpl; auto. +(* L2 can step *) + destruct t. + right; exists E0; exists (nil, s2'). constructor. auto. + right; exists (e :: nil); exists (t, s2'). constructor. auto. +(* 2. some buffered events *) + unfold E0 in H3; destruct H3. congruence. + right; exists (e :: nil); exists (t, s3). constructor. auto. +Qed. + +Theorem factor_backward_simulation: + backward_simulation L1 (atomic L2). +Proof. + apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim). +(* wf *) + apply bsim_order_wf. +(* initial states exist *) + intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A]. + exists (E0, s2). simpl; auto. +(* initial states match *) + intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst. + exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]]. + exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto. +(* final states match *) + intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst. + inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto. + intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto. +(* progress *) + exact fbs_progress. +(* simulation *) + exact fbs_simulation. +(* symbols *) + simpl. exact (bsim_symbols_preserved sim). +Qed. + +End FACTOR_BACKWARD_SIMULATION. + +(** Receptiveness of [atomic L]. *) + +Record strongly_receptive (L: semantics) : Prop := + Strongly_receptive { + ssr_receptive: forall s ev1 t1 s1 ev2, + Step L s (ev1 :: t1) s1 -> + match_traces (globalenv L) (ev1 :: nil) (ev2 :: nil) -> + exists s2, exists t2, Step L s (ev2 :: t2) s2; + ssr_well_behaved: + well_behaved_traces L + }. + +Theorem atomic_receptive: + forall L, strongly_receptive L -> receptive (atomic L). +Proof. + intros. constructor; intros. +(* receptive *) + inv H0. + (* silent step *) + inv H1. exists (E0, s'). constructor; auto. + (* start step *) + assert (exists ev2, t2 = ev2 :: nil). inv H1; econstructor; eauto. + destruct H0 as [ev2 EQ]; subst t2. + exploit ssr_receptive; eauto. intros [s2 [t2 P]]. + exploit ssr_well_behaved. eauto. eexact P. simpl; intros Q. + exists (t2, s2). constructor; auto. + (* continue step *) + simpl in H2; destruct H2. + assert (t2 = ev :: nil). inv H1; simpl in H0; tauto. + subst t2. exists (t, s0). constructor; auto. simpl; auto. +(* single-event *) + red. intros. inv H0; simpl; omega. +Qed. + (** * Connections with big-step semantics *) (** The general form of a big-step semantics *) diff --git a/common/Values.v b/common/Values.v index 7fae3b7..54eac86 100644 --- a/common/Values.v +++ b/common/Values.v @@ -160,6 +160,13 @@ Definition notint (v: val) : val := Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. +Definition boolval (v: val) : val := + match v with + | Vint n => of_bool (negb (Int.eq n Int.zero)) + | Vptr b ofs => Vtrue + | _ => Vundef + end. + Definition notbool (v: val) : val := match v with | Vint n => of_bool (Int.eq n Int.zero) -- cgit v1.2.3