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

1 files changed, 262 insertions, 25 deletions

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.