From 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 12:53:19 +0000 Subject: Distinguish two kinds of nonterminating behaviors: silent divergence and reactive divergence. As a consequence: - Removed the Enilinf constructor from traceinf (values of traceinf type are always infinite traces). - Traces are now uniquely defined. - Adapted proofs big step -> small step for Clight and Cminor accordingly. - Strengthened results in driver/Complements accordingly. - Added common/Determinism to collect generic results about deterministic semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Smallstep.v | 287 ++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 262 insertions(+), 25 deletions(-) (limited to 'common/Smallstep.v') diff --git a/common/Smallstep.v b/common/Smallstep.v index 9e9063b..deab49b 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -46,6 +46,11 @@ Variable state: Type. Variable step: genv -> state -> trace -> state -> Prop. +(** No transitions: stuck state *) + +Definition nostep (ge: genv) (s: state) : Prop := + forall t s', ~(step ge s t s'). + (** Zero, one or several transitions. Also known as Kleene closure, or reflexive transitive closure. *) @@ -280,28 +285,102 @@ Proof. subst. econstructor; eauto. Qed. +(** Infinitely many silent transitions *) + +CoInductive forever_silent (ge: genv): state -> Prop := + | forever_silent_intro: forall s1 s2, + step ge s1 E0 s2 -> forever_silent ge s2 -> + forever_silent ge s1. + +(** An alternate definition. *) + +CoInductive forever_silent_N (ge: genv) : A -> state -> Prop := + | forever_silent_N_star: forall s1 s2 a1 a2, + star ge s1 E0 s2 -> + order a2 a1 -> + forever_silent_N ge a2 s2 -> + forever_silent_N ge a1 s1 + | forever_silent_N_plus: forall s1 s2 a1 a2, + plus ge s1 E0 s2 -> + forever_silent_N ge a2 s2 -> + forever_silent_N ge a1 s1. + +Lemma forever_silent_N_inv: + forall ge a s, + forever_silent_N ge a s -> + exists s', exists a', + step ge s E0 s' /\ forever_silent_N ge a' s'. +Proof. + intros ge a0. pattern a0. apply (well_founded_ind order_wf). + intros. inv H0. + (* star case *) + inv H1. + (* no transition *) + apply H with a2. auto. auto. + (* at least one transition *) + exploit Eapp_E0_inv; eauto. intros [P Q]. subst. + exists s0; exists x. + split. auto. eapply forever_silent_N_star; eauto. + (* plus case *) + inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst. + exists s0; exists a2. + split. auto. inv H3. auto. + eapply forever_silent_N_plus. econstructor; eauto. eauto. +Qed. + +Lemma forever_silent_N_forever: + forall ge a s, forever_silent_N ge a s -> forever_silent ge s. +Proof. + cofix COINDHYP; intros. + destruct (forever_silent_N_inv H) as [s' [a' [P Q]]]. + apply forever_silent_intro with s'. auto. + apply COINDHYP with a'; auto. +Qed. + +(** Infinitely many non-silent transitions *) + +CoInductive forever_reactive (ge: genv): state -> traceinf -> Prop := + | forever_reactive_intro: forall s1 s2 t T, + star ge s1 t s2 -> t <> E0 -> forever_reactive ge s2 T -> + forever_reactive ge s1 (t *** T). + +Lemma star_forever_reactive: + forall ge s1 t s2 T, + star ge s1 t s2 -> forever_reactive ge s2 T -> + forever_reactive ge s1 (t *** T). +Proof. + intros. inv H0. rewrite <- Eappinf_assoc. econstructor. + eapply star_trans; eauto. + red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction. + auto. +Qed. + (** * Outcomes for program executions *) -(** The three possible outcomes for the execution of a program: +(** The four possible outcomes for the execution of a program: - Termination, with a finite trace of observable events and an integer value that stands for the process exit code (the return value of the main function). -- Divergence with an infinite trace of observable events. - (The actual events generated by the execution can be a - finite prefix of this trace, or the whole trace.) +- Divergence with a finite trace of observable events. + (At some point, the program runs forever without doing any I/O.) +- Reactive divergence with an infinite trace of observable events. + (The program performs infinitely many I/O operations separated + by finite amounts of internal computations.) - Going wrong, with a finite trace of observable events performed before the program gets stuck. *) Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior - | Diverges: traceinf -> program_behavior + | Diverges: trace -> program_behavior + | Reacts: traceinf -> program_behavior | Goes_wrong: trace -> program_behavior. Definition not_wrong (beh: program_behavior) : Prop := match beh with | Terminates _ _ => True | Diverges _ => True + | Reacts _ => True | Goes_wrong _ => False end. @@ -319,16 +398,23 @@ Inductive program_behaves (ge: genv): program_behavior -> Prop := star ge s t s' -> final_state s' r -> program_behaves ge (Terminates t r) - | program_diverges: forall s T, + | program_diverges: forall s t s', initial_state s -> - forever ge s T -> - program_behaves ge (Diverges T) + star ge s t s' -> forever_silent ge s' -> + program_behaves ge (Diverges t) + | program_reacts: forall s T, + initial_state s -> + forever_reactive ge s T -> + program_behaves ge (Reacts T) | program_goes_wrong: forall s t s', initial_state s -> star ge s t s' -> - (forall t1 s1, ~step ge s' t1 s1) -> + nostep ge s' -> (forall r, ~final_state s' r) -> - program_behaves ge (Goes_wrong t). + program_behaves ge (Goes_wrong t) + | program_goes_initially_wrong: + (forall s, ~initial_state s) -> + program_behaves ge (Goes_wrong E0). End CLOSURES. @@ -363,7 +449,6 @@ Variable ge2: genv2. This matching relation must be compatible with initial states and with final states. *) - Variable match_states: state1 -> state2 -> Prop. Hypothesis match_initial_states: @@ -414,23 +499,35 @@ Proof. auto. Qed. -Lemma simulation_star_forever: - forall st1 st2 T, - forever step1 ge1 st1 T -> match_states st1 st2 -> - forever step2 ge2 st2 T. +Lemma simulation_star_forever_silent: + forall st1 st2, + forever_silent step1 ge1 st1 -> match_states st1 st2 -> + forever_silent step2 ge2 st2. Proof. - assert (forall st1 st2 T, - forever step1 ge1 st1 T -> match_states st1 st2 -> - forever_N step2 order ge2 st1 st2 T). + assert (forall st1 st2, + forever_silent step1 ge1 st1 -> match_states st1 st2 -> + forever_silent_N step2 order ge2 st1 st2). cofix COINDHYP; intros. inversion H; subst. destruct (simulation H1 H0) as [st2' [A B]]. destruct A as [C | [C D]]. - apply forever_N_plus with t st2' s2 T0. - auto. apply COINDHYP. assumption. assumption. auto. - apply forever_N_star with t st2' s2 T0. - auto. auto. apply COINDHYP. assumption. auto. auto. - intros. eapply forever_N_forever; eauto. + apply forever_silent_N_plus with st2' s2. + auto. apply COINDHYP. assumption. assumption. + apply forever_silent_N_star with st2' s2. + auto. auto. apply COINDHYP. assumption. auto. + intros. eapply forever_silent_N_forever; eauto. +Qed. + +Lemma simulation_star_forever_reactive: + forall st1 st2 T, + forever_reactive step1 ge1 st1 T -> match_states st1 st2 -> + forever_reactive step2 ge2 st2 T. +Proof. + cofix COINDHYP; intros. + inv H. + destruct (simulation_star_star H1 H0) as [st2' [A B]]. + econstructor. eexact A. auto. + eapply COINDHYP. eauto. auto. Qed. Lemma simulation_star_wf_preservation: @@ -444,9 +541,13 @@ Proof. destruct (simulation_star_star H2 B) as [s2' [C D]]. econstructor; eauto. destruct (match_initial_states H1) as [s2 [A B]]. + destruct (simulation_star_star H2 B) as [s2' [C D]]. econstructor; eauto. - eapply simulation_star_forever; eauto. - contradiction. + eapply simulation_star_forever_silent; eauto. + destruct (match_initial_states H1) as [s2 [A B]]. + econstructor; eauto. eapply simulation_star_forever_reactive; eauto. + contradiction. + contradiction. Qed. End SIMULATION_STAR_WF. @@ -579,4 +680,140 @@ End SIMULATION_OPT. End SIMULATION. +(** * Additional results about infinite reduction sequences *) + +(** We now show that any infinite sequence of reductions is either of + the "reactive" kind or of the "silent" kind (after a finite number + of non-silent transitions). The proof necessitates the axiom of + excluded middle. This result is used in [Csem] and [Cminor] to + relate the coinductive big-step semantics for divergence with the + small-step notions of divergence. *) + +Require Import Classical. +Unset Implicit Arguments. + +Section INF_SEQ_DECOMP. + +Variable genv: Type. +Variable state: Type. +Variable step: genv -> state -> trace -> state -> Prop. + +Variable ge: genv. + +Inductive State: Type := + ST: forall (s: state) (T: traceinf), forever step ge s T -> State. + +Definition state_of_State (S: State): state := + match S with ST s T F => s end. +Definition traceinf_of_State (S: State) : traceinf := + match S with ST s T F => T end. + +Inductive Step: trace -> State -> State -> Prop := + | Step_intro: forall s1 t T s2 S F, + Step t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F)) + (ST s2 T F). + +Inductive Steps: State -> State -> Prop := + | Steps_refl: forall S, Steps S S + | Steps_left: forall t S1 S2 S3, Step t S1 S2 -> Steps S2 S3 -> Steps S1 S3. + +Remark Steps_trans: + forall S1 S2, Steps S1 S2 -> forall S3, Steps S2 S3 -> Steps S1 S3. +Proof. + induction 1; intros. auto. econstructor; eauto. +Qed. + +Let Reactive (S: State) : Prop := + forall S1, + Steps S S1 -> + exists S2, exists S3, exists t, Steps S1 S2 /\ Step t S2 S3 /\ t <> E0. + +Let Silent (S: State) : Prop := + forall S1 t S2, Steps S S1 -> Step t S1 S2 -> t = E0. + +Lemma Reactive_or_Silent: + forall S, Reactive S \/ (exists S', Steps S S' /\ Silent S'). +Proof. + intros. destruct (classic (exists S', Steps S S' /\ Silent S')). + auto. + left. red; intros. + generalize (not_ex_all_not _ _ H S1). intros. + destruct (not_and_or _ _ H1). contradiction. + unfold Silent in H2. + generalize (not_all_ex_not _ _ H2). intros [S2 A]. + generalize (not_all_ex_not _ _ A). intros [t B]. + generalize (not_all_ex_not _ _ B). intros [S3 C]. + generalize (imply_to_and _ _ C). intros [D F]. + generalize (imply_to_and _ _ F). intros [G J]. + exists S2; exists S3; exists t. auto. +Qed. + +Lemma Steps_star: + forall S1 S2, Steps S1 S2 -> + exists t, star step ge (state_of_State S1) t (state_of_State S2) + /\ traceinf_of_State S1 = t *** traceinf_of_State S2. +Proof. + induction 1. + exists E0; split. apply star_refl. auto. + inv H. destruct IHSteps as [t' [A B]]. + exists (t ** t'); split. + simpl; eapply star_left; eauto. + simpl in *. subst T. traceEq. +Qed. + +Lemma Silent_forever_silent: + forall S, + Silent S -> forever_silent step ge (state_of_State S). +Proof. + cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros. + assert (Step t (ST s1 (t *** T0) (forever_intro s1 t s0 f0)) + (ST s2 T0 f0)). + constructor. + assert (t = E0). + red in H. eapply H; eauto. apply Steps_refl. + apply forever_silent_intro with (state_of_State (ST s2 T0 f0)). + rewrite <- H1. assumption. + apply COINDHYP. + red; intros. eapply H. eapply Steps_left; eauto. eauto. +Qed. + +Lemma Reactive_forever_reactive: + forall S, + Reactive S -> forever_reactive step ge (state_of_State S) (traceinf_of_State S). +Proof. + cofix COINDHYP; intros. + destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply Steps_refl. + destruct (Steps_star _ _ A) as [t' [P Q]]. + inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. + apply forever_reactive_intro with s2. + eapply star_right; eauto. + red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction. + change (forever_reactive step ge (state_of_State (ST s2 T F)) (traceinf_of_State (ST s2 T F))). + apply COINDHYP. + red; intros. apply H. + eapply Steps_trans. eauto. + eapply Steps_left. constructor. eauto. +Qed. + +Theorem forever_silent_or_reactive: + forall s T, + forever step ge s T -> + forever_reactive step ge s T \/ + exists t, exists s', exists T', + star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'. +Proof. + intros. + destruct (Reactive_or_Silent (ST s T H)). + left. + change (forever_reactive step ge (state_of_State (ST s T H)) (traceinf_of_State (ST s T H))). + apply Reactive_forever_reactive. auto. + destruct H0 as [S' [A B]]. + exploit Steps_star; eauto. intros [t [C D]]. simpl in *. + right. exists t; exists (state_of_State S'); exists (traceinf_of_State S'). + split. auto. + split. apply Silent_forever_silent. auto. + auto. +Qed. + +End INF_SEQ_DECOMP. -- cgit v1.2.3