From 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 16 Aug 2009 12:53:19 +0000
Subject: [PATCH] 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
---
 .depend                   |  10 +-
 Makefile                  |   2 +-
 backend/Cminor.v          |  47 ++--
 backend/RTLtyping.v       |  13 +-
 cfrontend/Csem.v          |  56 ++--
 cfrontend/Cshmgenproof3.v |  19 +-
 common/Determinism.v      | 508 +++++++++++++++++++++++++++++++++
 common/Events.v           |  55 ++--
 common/Smallstep.v        | 287 +++++++++++++++++--
 driver/Complements.v      | 576 +++-----------------------------------
 10 files changed, 916 insertions(+), 657 deletions(-)
 create mode 100644 common/Determinism.v

diff --git a/.depend b/.depend
index c6df7798f..6cb74c91c 100644
--- a/.depend
+++ b/.depend
@@ -9,6 +9,8 @@ lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo
 lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo
 lib/UnionFind.vo: lib/UnionFind.v lib/Coqlib.vo
 common/AST.vo: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo
+common/Determinism2.vo: common/Determinism2.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
+common/Determinism.vo: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
 common/Errors.vo: common/Errors.v lib/Coqlib.vo
 common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo
 common/Globalenvs.vo: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo
@@ -64,7 +66,7 @@ backend/Reload.vo: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/
 backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo
 backend/RTLgenspec.vo: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo
 backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo
-backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo common/Globalenvs.vo common/Values.vo common/Mem.vo lib/Integers.vo common/Events.vo common/Smallstep.vo
+backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Mem.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo
 backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo
 backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machabstr.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
 backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo
@@ -72,9 +74,9 @@ backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.
 backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Tailcall.vo
 backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo
 backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
-backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo
+backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo
 backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo
-cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo cfrontend/Cminorgen.vo
+cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo cfrontend/Cminorgen.vo common/Switch.vo
 cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo
 cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Csharpminor.vo: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo
@@ -85,4 +87,4 @@ cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Int
 cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo
 cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo
 driver/Compiler.vo: driver/Compiler.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo $(ARCH)/Selection.vo backend/RTLgen.vo backend/Tailcall.vo $(ARCH)/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo $(ARCH)/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo $(ARCH)/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo
-driver/Complements.vo: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
+driver/Complements.vo: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
diff --git a/Makefile b/Makefile
index 8bae5a05a..f253e3ac4 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ LIB=Coqlib.v Maps.v Lattice.v Ordered.v \
 # Parts common to the front-ends and the back-end (in common/)
 
 COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \
-  Smallstep.v Switch.v
+  Smallstep.v Determinism.v Switch.v
 
 # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT))
 
diff --git a/backend/Cminor.v b/backend/Cminor.v
index b48db2d6e..8cc2185da 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -755,13 +755,10 @@ with execinf_stmt:
 
 End NATURALSEM.
 
-(** Execution of a whole program: [exec_program p beh]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] has [beh] as observable
-  behavior. *)
+(** Big-step execution of a whole program *)
 
-Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
-  | program_terminates:
+Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
+  | bigstep_program_terminates_intro:
       forall b f t m r,
       let ge := Genv.globalenv p in
       let m0 := Genv.init_mem p in
@@ -769,8 +766,10 @@ Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       eval_funcall ge m0 f nil t m (Vint r) ->
-      exec_program_bigstep p (Terminates t r)
-  | program_diverges:
+      bigstep_program_terminates p t r.
+
+Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
+  | bigstep_program_diverges_intro:
       forall b f t,
       let ge := Genv.globalenv p in
       let m0 := Genv.init_mem p in
@@ -778,7 +777,7 @@ Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       evalinf_funcall ge m0 f nil t ->
-      exec_program_bigstep p (Diverges t).
+      bigstep_program_diverges p t.
 
 (** ** Correctness of the big-step semantics with respect to the transition semantics *)
 
@@ -1087,22 +1086,32 @@ Proof.
   traceEq.
 Qed.
 
-Theorem exec_program_bigstep_transition:
-  forall beh,
-  exec_program_bigstep prog beh ->
-  exec_program prog beh.
+Theorem bigstep_program_terminates_exec:
+  forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
 Proof.
   intros. inv H.
-  (* termination *)
   econstructor.
   econstructor. eauto. eauto. auto. 
   apply eval_funcall_steps. eauto. red; auto. 
-  econstructor. 
-  (* divergence *)
   econstructor.
-  econstructor. eauto. eauto. auto. 
-  apply forever_plus_forever. 
-  apply evalinf_funcall_forever. auto.
+Qed.
+
+Theorem bigstep_program_diverges_exec:
+  forall T, bigstep_program_diverges prog T ->
+  exec_program prog (Reacts T) \/
+  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
+Proof.
+  intros. inv H.
+  set (st := Callstate f nil Kstop m0).
+  assert (forever step ge0 st T). 
+    eapply forever_plus_forever.
+    eapply evalinf_funcall_forever; eauto. 
+  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
+  as [A | [t [s' [T' [B [C D]]]]]]. 
+  left. econstructor. econstructor. eauto. eauto. auto. auto.
+  right. exists t. split.
+  econstructor. econstructor; eauto. eauto. auto.  
+  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
 Qed.
 
 End BIGSTEP_TO_TRANSITION.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index f466a90c0..83e82e14b 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -18,6 +18,12 @@ Require Import Maps.
 Require Import AST.
 Require Import Op.
 Require Import Registers.
+Require Import Globalenvs.
+Require Import Values.
+Require Import Mem.
+Require Import Integers.
+Require Import Events.
+Require Import Smallstep.
 Require Import RTL.
 Require Conventions.
 
@@ -398,13 +404,6 @@ Qed.
   here, as a warm-up exercise and because some of the lemmas will be
   useful later. *)
 
-Require Import Globalenvs.
-Require Import Values.
-Require Import Mem.
-Require Import Integers.
-Require Import Events.
-Require Import Smallstep.
-
 Definition wt_regset (env: regenv) (rs: regset) : Prop :=
   forall r, Val.has_type (rs#r) (env r).
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index fb8b8e1ad..e0d05f219 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -1233,27 +1233,25 @@ Inductive final_state: state -> int -> Prop :=
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
 
-(** Big-step execution of a whole program.  
-  [exec_program_bigstep p beh] holds
-  if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] executes without errors and produces
-  the observable behaviour [beh]. *)
-
-Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
-  | program_terminates: forall b f m1 t r,
+(** Big-step execution of a whole program.  *)
+
+Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
+  | bigstep_program_terminates_intro: forall b f m1 t r,
       let ge := Genv.globalenv p in 
       let m0 := Genv.init_mem p in
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
-      exec_program_bigstep p (Terminates t r)
-  | program_diverges: forall b f t,
+      bigstep_program_terminates p t r.
+
+Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
+  | bigstep_program_diverges_intro: forall b f t,
       let ge := Genv.globalenv p in 
       let m0 := Genv.init_mem p in
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       evalinf_funcall ge m0 f nil t ->
-      exec_program_bigstep p (Diverges t).
+      bigstep_program_diverges p t.
 
 (** * Implication from big-step semantics to transition semantics *)
 
@@ -1696,26 +1694,34 @@ Proof.
   traceEq.
 Qed.
 
-(*
-Theorem exec_program_bigstep_transition:
-  forall beh,
-  exec_program_bigstep prog beh ->
-  exec_program prog beh.
+Theorem bigstep_program_terminates_exec:
+  forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
 Proof.
-  intros. inv H.
-  (* termination *)
+  intros. inv H. unfold ge0, m0 in *. 
   econstructor.
   econstructor. eauto. eauto.
   apply eval_funcall_steps. eauto. red; auto. 
-  econstructor. 
-  (* divergence *)
   econstructor.
-  econstructor. eauto. eauto. 
-  eapply forever_N_forever with (order := order).
-  red; intros. constructor; intros. red in H. elim H.
-  apply evalinf_funcall_forever. auto.
 Qed.
-*)
+
+Theorem bigstep_program_diverges_exec:
+  forall T, bigstep_program_diverges prog T ->
+  exec_program prog (Reacts T) \/
+  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
+Proof.
+  intros. inv H.
+  set (st := Callstate f nil Kstop m0).
+  assert (forever step ge0 st T). 
+    eapply forever_N_forever with (order := order).
+    red; intros. constructor; intros. red in H. elim H.
+    eapply evalinf_funcall_forever; eauto. 
+  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
+  as [A | [t [s' [T' [B [C D]]]]]]. 
+  left. econstructor. econstructor. eauto. eauto. auto.
+  right. exists t. split.
+  econstructor. econstructor; eauto. eauto. auto. 
+  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
+Qed.
 
 End BIGSTEP_TO_TRANSITIONS.
 
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 6a8b676f8..836f1e4b5 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1661,6 +1661,8 @@ Theorem transl_program_correct:
   Csharpminor.exec_program tprog beh.
 Proof.
   set (order := fun (S1 S2: Csem.state) => False).
+  assert (WF: well_founded order).
+  unfold order; red. intros. constructor; intros. contradiction.
   assert (transl_step':
      forall S1 t S2, Csem.step ge S1 t S2 ->
      forall T1, match_states S1 T1 ->
@@ -1670,21 +1672,30 @@ Proof.
   intros. exploit transl_step; eauto. intros [T2 [A B]].
   exists T2; split. auto. auto.
   intros. inv H0.
+(* Terminates *)
   assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
   inv H3. inv H2. inv H1. exists t1; exists s2; auto.
   destruct H0 as [t1 [s1 ST]].
   exploit transl_initial_states; eauto. intros [R [A B]].
   exploit simulation_star_star; eauto. intros [R' [C D]]. 
   econstructor; eauto. eapply transl_final_states; eauto.
+(* Diverges *)
   assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
-  inv H2. exists t; exists s2; auto.
+  inv H2. inv H3. exists E0; exists s2; auto. exists t1; exists s2; auto.
   destruct H0 as [t1 [s1 ST]].
   exploit transl_initial_states; eauto. intros [R [A B]].
-  exploit simulation_star_forever; eauto.
-  unfold order; red. intros. constructor; intros. contradiction.
+  exploit simulation_star_star; eauto. intros [R' [C D]]. 
+  econstructor; eauto. eapply simulation_star_forever_silent; eauto.
+(* Reacts *)
+  assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1).
+  inv H2. inv H0. congruence. exists t1; exists s0; auto.
+  destruct H0 as [t1 [s1 ST]].
+  exploit transl_initial_states; eauto. intros [R [A B]].
+  exploit simulation_star_forever_reactive; eauto.
   intro C.
   econstructor; eauto.
-  contradiction.
+(* Goes wrong *)
+  contradiction. contradiction.
 Qed.
 
 End CORRECTNESS.
diff --git a/common/Determinism.v b/common/Determinism.v
new file mode 100644
index 000000000..430ee93de
--- /dev/null
+++ b/common/Determinism.v
@@ -0,0 +1,508 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Characterization and properties of deterministic semantics *)
+
+Require Import Classical.
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Smallstep.
+
+(** This file uses classical logic (the axiom of excluded middle), as
+  well as the following extensionality property over infinite
+  sequences of events.  All these axioms are sound in a set-theoretic
+  model of Coq's logic. *)
+
+Axiom traceinf_extensionality:
+  forall T T', traceinf_sim T T' -> T = T'.
+
+(** * Deterministic worlds *)
+
+(** One source of possible nondeterminism is that our semantics leave
+  unspecified the results of calls to external 
+  functions.  Different results to e.g. a "read" operation can of
+  course lead to different behaviors for the program.
+  We address this issue by modeling a notion of deterministic
+  external world that uniquely determines the results of external calls. *)
+
+(** An external world is a function that, given the name of an
+  external call and its arguments, returns either [None], meaning
+  that this external call gets stuck, or [Some(r,w)], meaning
+  that this external call succeeds, has result [r], and changes
+  the world to [w]. *)
+
+Inductive world: Type :=
+  World: (ident -> list eventval -> option (eventval * world)) -> world.
+
+Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
+                     option (eventval * world) :=
+  match w with World f => f evname evargs end.
+
+(** A trace is possible in a given world if all events correspond
+  to non-stuck external calls according to the given world.
+  Two predicates are defined, for finite and infinite traces respectively:
+- [possible_trace w t w'], where [w] is the initial state of the
+  world, [t] the finite trace of interest, and [w'] the state of the
+  world after performing trace [t].
+- [possible_traceinf w T], where [w] is the initial state of the
+  world and [T] the infinite trace of interest.
+*)
+
+Inductive possible_trace: world -> trace -> world -> Prop :=
+  | possible_trace_nil: forall w,
+      possible_trace w E0 w
+  | possible_trace_cons: forall w0 evname evargs evres w1 t w2,
+      nextworld w0 evname evargs = Some (evres, w1) ->
+      possible_trace w1 t w2 ->
+      possible_trace w0 (mkevent evname evargs evres :: t) w2.
+
+Lemma possible_trace_app:
+  forall t2 w2 w0 t1 w1,
+  possible_trace w0 t1 w1 -> possible_trace w1 t2 w2 ->
+  possible_trace w0 (t1 ** t2) w2.
+Proof.
+  induction 1; simpl; intros.
+  auto.
+  econstructor; eauto.
+Qed.
+
+Lemma possible_trace_app_inv:
+  forall t2 w2 t1 w0,
+  possible_trace w0 (t1 ** t2) w2 ->
+  exists w1, possible_trace w0 t1 w1 /\ possible_trace w1 t2 w2.
+Proof.
+  induction t1; simpl; intros.
+  exists w0; split. constructor. auto.
+  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
+  exists w1; split. econstructor; eauto. auto.
+Qed.
+
+CoInductive possible_traceinf: world -> traceinf -> Prop :=
+  | possible_traceinf_cons: forall w0 evname evargs evres w1 T,
+      nextworld w0 evname evargs = Some (evres, w1) ->
+      possible_traceinf w1 T ->
+      possible_traceinf w0 (Econsinf (mkevent evname evargs evres) T).
+
+Lemma possible_traceinf_app:
+  forall t2 w0 t1 w1,
+  possible_trace w0 t1 w1 -> possible_traceinf w1 t2 ->
+  possible_traceinf w0 (t1 *** t2).
+Proof.
+  induction 1; simpl; intros.
+  auto.
+  econstructor; eauto.
+Qed.
+
+Lemma possible_traceinf_app_inv:
+  forall t2 t1 w0,
+  possible_traceinf w0 (t1 *** t2) ->
+  exists w1, possible_trace w0 t1 w1 /\ possible_traceinf w1 t2.
+Proof.
+  induction t1; simpl; intros.
+  exists w0; split. constructor. auto.
+  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
+  exists w1; split. econstructor; eauto. auto.
+Qed.
+
+Ltac possibleTraceInv :=
+  match goal with
+  | [H: possible_trace _ E0 _ |- _] =>
+      inversion H; clear H; subst; possibleTraceInv
+  | [H: possible_trace _ (_ ** _) _ |- _] =>
+      let P1 := fresh "P" in
+      let w := fresh "w" in
+      let P2 := fresh "P" in
+      elim (possible_trace_app_inv _ _ _ _ H); clear H;
+      intros w [P1 P2];
+      possibleTraceInv
+  | [H: possible_traceinf _ (_ *** _) |- _] =>
+      let P1 := fresh "P" in
+      let w := fresh "w" in
+      let P2 := fresh "P" in
+      elim (possible_traceinf_app_inv _ _ _ H); clear H;
+      intros w [P1 P2];
+      possibleTraceInv
+  | [H: exists w, possible_trace _ _ w |- _] =>
+      let P := fresh "P" in let w := fresh "w" in 
+      destruct H as [w P]; possibleTraceInv
+  | _ => idtac
+  end.
+
+Definition possible_behavior (w: world) (b: program_behavior) : Prop :=
+  match b with
+  | Terminates t r => exists w', possible_trace w t w'
+  | Diverges t => exists w', possible_trace w t w'
+  | Reacts T => possible_traceinf w T
+  | Goes_wrong t => exists w', possible_trace w t w'
+  end.
+
+(** Determinism properties of [event_match]. *)
+
+Remark eventval_match_deterministic:
+  forall ev1 ev2 ty v1 v2,
+  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 ->
+  (ev1 = ev2 <-> v1 = v2).
+Proof.
+  intros. inv H; inv H0; intuition congruence.
+Qed.
+
+Remark eventval_list_match_deterministic:
+  forall ev1 ty v, eventval_list_match ev1 ty v ->
+  forall ev2, eventval_list_match ev2 ty v -> ev1 = ev2.
+Proof.
+  induction 1; intros.
+  inv H. auto.
+  inv H1. decEq.
+  rewrite (eventval_match_deterministic _ _ _ _ _ H H6). auto.
+  eauto.
+Qed.
+
+(** * Deterministic semantics *)
+
+Section DETERM_SEM.
+
+(** We assume given a transition semantics that is internally
+  deterministic: the only source of non-determinism is the return
+  value of external calls. *)
+
+Variable genv: Type.
+Variable state: Type.
+Variable step: genv -> state -> trace -> state -> Prop.
+Variable initial_state: state -> Prop.
+Variable final_state: state -> int -> Prop.
+
+Inductive internal_determinism: trace -> state -> trace -> state -> Prop :=
+  | int_determ_0: forall s,
+      internal_determinism E0 s E0 s
+  | int_determ_1: forall s s' id arg res res',
+      (res = res' -> s = s') ->
+      internal_determinism (mkevent id arg res :: nil) s
+                           (mkevent id arg res' :: nil) s'.
+
+Hypothesis step_internal_deterministic:
+  forall ge s t1 s1 t2 s2,
+  step ge s t1 s1 -> step ge s t2 s2 -> internal_determinism t1 s1 t2 s2.
+
+Hypothesis initial_state_determ:
+  forall s1 s2, initial_state s1 -> initial_state s2 -> s1 = s2.
+
+Hypothesis final_state_determ:
+  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.
+
+Hypothesis final_state_nostep:
+  forall ge st r, final_state st r -> nostep step ge st.
+
+(** Consequently, the [step] relation is deterministic if restricted
+    to traces that are possible in a deterministic world. *)
+
+Lemma step_deterministic:
+  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
+  step ge s0 t1 s1 -> step ge s0 t2 s2 ->
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  s1 = s2 /\ t1 = t2 /\ w1 = w2.
+Proof.
+  intros. exploit step_internal_deterministic. eexact H. eexact H0. intro ID.
+  inv ID.
+  inv H1. inv H2. auto.
+  inv H2. inv H11. inv H1. inv H11. 
+  rewrite H10 in H9. inv H9. 
+  intuition.
+Qed.
+
+Ltac use_step_deterministic :=
+  match goal with
+  | [ S1: step _ _ ?t1 _, P1: possible_trace _ ?t1 _,
+      S2: step _ _ ?t2 _, P2: possible_trace _ ?t2 _ |- _ ] =>
+    destruct (step_deterministic _ _ _ _ _ _ _ _ _ S1 S2 P1 P2)
+    as [EQ1 [EQ2 EQ3]]; subst
+  end.
+
+(** Determinism for finite transition sequences. *)
+
+Lemma star_step_diamond:
+  forall ge s0 t1 s1, star step ge s0 t1 s1 -> 
+  forall t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> 
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  exists t,
+     (star step ge s1 t s2 /\ possible_trace w1 t w2 /\ t2 = t1 ** t)
+  \/ (star step ge s2 t s1 /\ possible_trace w2 t w1 /\ t1 = t2 ** t).
+Proof.
+  induction 1; intros. 
+  inv H0. exists t2; auto. 
+  inv H2. inv H4. exists (t1 ** t2); right. 
+    split. econstructor; eauto. auto.
+  possibleTraceInv. use_step_deterministic.  
+  exploit IHstar. eexact H6. eauto. eauto. 
+  intros [t A]. exists t.
+  destruct A. left; intuition. traceEq. right; intuition. traceEq. 
+Qed.
+
+Ltac use_star_step_diamond :=
+  match goal with
+  | [ S1: star step _ _ ?t1 _, P1: possible_trace _ ?t1 _,
+      S2: star step _ _ ?t2 _, P2: possible_trace _ ?t2 _ |- _ ] =>
+    let t := fresh "t" in let P := fresh "P" in let Q := fresh "Q" in let EQ := fresh "EQ" in
+    destruct (star_step_diamond _ _ _ _ S1 _ _ _ _ _ S2 P1 P2)
+    as [t [ [P [Q EQ]] | [P [Q EQ]] ]]; subst
+  end.
+
+Ltac use_nostep :=
+  match goal with
+  | [ S: step _ ?s _ _, NO: nostep step _ ?s |- _ ] => elim (NO _ _ S)
+  end.
+
+Lemma star_step_triangle:
+  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
+  star step ge s0 t1 s1 -> 
+  star step ge s0 t2 s2 -> 
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  nostep step ge s2 ->
+  exists t,
+  star step ge s1 t s2 /\ possible_trace w1 t w2 /\ t2 = t1 ** t.
+Proof.
+  intros. use_star_step_diamond; possibleTraceInv. 
+  exists t; auto.
+  inv P. inv Q. exists E0. split. constructor. split. constructor. traceEq.
+  use_nostep.
+Qed.
+
+Ltac use_star_step_triangle :=
+  match goal with
+  | [ S1: star step _ _ ?t1 _, P1: possible_trace _ ?t1 _,
+      S2: star step _ _ ?t2 ?s2, P2: possible_trace _ ?t2 _,
+      NO: nostep step _ ?s2 |- _ ] =>
+    let t := fresh "t" in let P := fresh "P" in let Q := fresh "Q" in let EQ := fresh "EQ" in
+    destruct (star_step_triangle _ _ _ _ _ _ _ _ _ S1 S2 P1 P2 NO)
+    as [t [P [Q EQ]]]; subst
+  end.
+
+Lemma steps_deterministic:
+  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
+  star step ge s0 t1 s1 -> star step ge s0 t2 s2 -> 
+  nostep step ge s1 -> nostep step ge s2 ->
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  t1 = t2 /\ s1 = s2.
+Proof.
+  intros. use_star_step_triangle. inv P.
+  inv Q. split; auto; traceEq. use_nostep.
+Qed.
+
+Lemma terminates_not_goes_wrong:
+  forall ge s t1 s1 r w w1 t2 s2 w2,
+  star step ge s t1 s1 -> final_state s1 r -> possible_trace w t1 w1 ->
+  star step ge s t2 s2 -> nostep step ge s2 -> possible_trace w t2 w2 ->
+  (forall r, ~final_state s2 r) -> False.
+Proof.
+  intros.
+  assert (t1 = t2 /\ s1 = s2). 
+    eapply steps_deterministic; eauto. 
+  destruct H6; subst. elim (H5 _ H0).
+Qed.
+
+(** Determinism for infinite transition sequences. *)
+
+Lemma star_final_not_forever_silent:
+  forall ge s t s', star step ge s t s' ->
+  forall w w', possible_trace w t w' -> nostep step ge s' ->
+  forever_silent step ge s -> False.
+Proof.
+  induction 1; intros. 
+  inv H1. use_nostep. 
+  inv H4. possibleTraceInv. assert (possible_trace w E0 w) by constructor. 
+  use_step_deterministic. eauto.
+Qed.
+
+Lemma star2_final_not_forever_silent:
+  forall ge s t1 s1 w w1 t2 s2 w2,
+  star step ge s t1 s1 -> possible_trace w t1 w1 -> nostep step ge s1 ->
+  star step ge s t2 s2 -> possible_trace w t2 w2 -> forever_silent step ge s2 ->
+  False.
+Proof.
+  intros. use_star_step_triangle. possibleTraceInv. 
+  eapply star_final_not_forever_silent. eexact P. eauto. auto. auto.
+Qed.
+
+Lemma star_final_not_forever_reactive:
+  forall ge s t s', star step ge s t s' -> 
+  forall w w' T, possible_trace w t w' -> possible_traceinf w T -> nostep step ge s' ->
+  forever_reactive step ge s T -> False.
+Proof.
+  induction 1; intros.
+  inv H2. inv H3. congruence. use_nostep. 
+  inv H5. possibleTraceInv. inv H6. congruence. possibleTraceInv.
+  use_step_deterministic.
+  eapply IHstar with (T := t4 *** T0). eauto. 
+  eapply possible_traceinf_app; eauto. auto. 
+  eapply star_forever_reactive; eauto.  
+Qed.
+
+Lemma star_forever_silent_inv:
+  forall ge s t s', star step ge s t s' ->
+  forall w w', possible_trace w t w' ->
+  forever_silent step ge s -> 
+  t = E0 /\ forever_silent step ge s'.
+Proof.
+  induction 1; intros.
+  auto.
+  subst. possibleTraceInv. inv H3. assert (possible_trace w E0 w) by constructor.
+  use_step_deterministic. eauto. 
+Qed.
+
+Lemma forever_silent_reactive_exclusive:
+  forall ge s w T,
+  forever_silent step ge s -> forever_reactive step ge s T -> 
+  possible_traceinf w T -> False.
+Proof.
+  intros. inv H0. possibleTraceInv. exploit star_forever_silent_inv; eauto. 
+  intros [A B]. contradiction.
+Qed.
+
+Lemma forever_reactive_inv2:
+  forall ge s t1 s1, star step ge s t1 s1 ->
+  forall t2 s2 T1 T2 w w1 w2,
+  possible_trace w t1 w1 ->
+  star step ge s t2 s2 -> possible_trace w t2 w2 ->
+  t1 <> E0 -> t2 <> E0 ->
+  forever_reactive step ge s1 T1 -> possible_traceinf w1 T1 ->
+  forever_reactive step ge s2 T2 -> possible_traceinf w2 T2 ->
+  exists s', exists e, exists T1', exists T2', exists w',
+  forever_reactive step ge s' T1' /\ possible_traceinf w' T1' /\
+  forever_reactive step ge s' T2' /\ possible_traceinf w' T2' /\
+  t1 *** T1 = Econsinf e T1' /\
+  t2 *** T2 = Econsinf e T2'.
+Proof.
+  induction 1; intros.
+  congruence.
+  inv H3. congruence. possibleTraceInv.
+  assert (ID: internal_determinism t3 s5 t1 s2). eauto. 
+  inv ID.
+  possibleTraceInv. eauto.
+  inv P. inv P1. inv H17. inv H19. rewrite H18 in H16; inv H16.
+  assert (s5 = s2) by auto. subst s5.
+  exists s2; exists (mkevent id arg res');
+  exists (t2 *** T1); exists (t4 *** T2); exists w0.
+  split. eapply star_forever_reactive; eauto. 
+  split. eapply possible_traceinf_app; eauto. 
+  split. eapply star_forever_reactive; eauto. 
+  split. eapply possible_traceinf_app; eauto.
+  auto.
+Qed.
+
+Lemma forever_reactive_determ:
+  forall ge s T1 T2 w,
+  forever_reactive step ge s T1 -> possible_traceinf w T1 ->
+  forever_reactive step ge s T2 -> possible_traceinf w T2 ->
+  traceinf_sim T1 T2.
+Proof.
+  cofix COINDHYP; intros.
+  inv H. inv H1. possibleTraceInv.
+  destruct (forever_reactive_inv2 _ _ _ _ H _ _ _ _ _ _ _ P H3 P1 H6 H4
+                                  H7 P0 H5 P2)
+  as [s' [e [T1' [T2' [w' [A [B [C [D [E G]]]]]]]]]].
+  rewrite E; rewrite G. constructor.
+  eapply COINDHYP; eauto. 
+Qed.
+
+Lemma star_forever_reactive_inv:
+  forall ge s t s', star step ge s t s' ->
+  forall w w' T, possible_trace w t w' -> forever_reactive step ge s T ->
+  possible_traceinf w T ->
+  exists T', forever_reactive step ge s' T' /\ possible_traceinf w' T' /\ T = t *** T'.
+Proof.
+  induction 1; intros. 
+  possibleTraceInv. exists T; auto.
+  inv H3. possibleTraceInv. inv H5. congruence. possibleTraceInv.
+  use_step_deterministic. 
+  exploit IHstar. eauto. eapply star_forever_reactive. 2: eauto. eauto.
+  eapply possible_traceinf_app; eauto. 
+  intros [T' [A [B C]]]. exists T'; intuition. traceEq. congruence. 
+Qed.
+
+Lemma forever_silent_reactive_exclusive2:
+  forall ge s t s' w w' T,
+  star step ge s t s' -> possible_trace w t w' -> forever_silent step ge s' ->
+  forever_reactive step ge s T -> possible_traceinf w T ->
+  False.
+Proof.
+  intros. exploit star_forever_reactive_inv; eauto. 
+  intros [T' [A [B C]]]. subst T.
+  eapply forever_silent_reactive_exclusive; eauto.
+Qed.
+
+(** Determinism for program executions *)
+
+Ltac use_init_state :=
+  match goal with
+  | [ H1: (initial_state _), H2: (initial_state _) |- _ ] =>
+        generalize (initial_state_determ _ _ H1 H2); intro; subst; clear H2
+  | [ H1: (initial_state _), H2: (forall s, ~initial_state s) |- _ ] =>
+        elim (H2 _ H1)
+  | _ => idtac
+  end.
+
+Theorem program_behaves_deterministic:
+  forall ge w beh1 beh2,
+  program_behaves step initial_state final_state ge beh1 -> possible_behavior w beh1 ->
+  program_behaves step initial_state final_state ge beh2 -> possible_behavior w beh2 ->
+  beh1 = beh2.
+Proof.
+  intros until beh2; intros BEH1 POS1 BEH2 POS2.
+  inv BEH1; inv BEH2; simpl in POS1; simpl in POS2;
+  possibleTraceInv; use_init_state.
+(* terminates, terminates *)
+  assert (t = t0 /\ s' = s'0). eapply steps_deterministic; eauto.
+  destruct H2. f_equal; auto. subst. eauto. 
+(* terminates, diverges *)
+  byContradiction. eapply star2_final_not_forever_silent with (s1 := s') (s2 := s'0); eauto.
+(* terminates, reacts *)
+  byContradiction. eapply star_final_not_forever_reactive; eauto.
+(* terminates, goes_wrong *)
+  byContradiction. eapply terminates_not_goes_wrong with (s1 := s') (s2 := s'0); eauto.
+(* diverges, terminates *)
+  byContradiction. eapply star2_final_not_forever_silent with (s2 := s') (s1 := s'0); eauto.
+(* diverges, diverges *)
+  f_equal. use_star_step_diamond.
+  exploit star_forever_silent_inv. eexact P1. eauto. eauto.
+  intros [A B]. subst; traceEq.
+  exploit star_forever_silent_inv. eexact P1. eauto. eauto.
+  intros [A B]. subst; traceEq.
+(* diverges, reacts *)
+  byContradiction. eapply forever_silent_reactive_exclusive2; eauto.
+(* diverges, goes wrong *)
+  byContradiction. eapply star2_final_not_forever_silent with (s1 := s'0) (s2 := s'); eauto.
+(* reacts, terminates *)
+  byContradiction. eapply star_final_not_forever_reactive; eauto.
+(* reacts, diverges *) 
+  byContradiction. eapply forever_silent_reactive_exclusive2; eauto.
+(* reacts, reacts *)
+  f_equal. apply traceinf_extensionality. 
+  eapply forever_reactive_determ; eauto. 
+(* reacts, goes wrong *)
+  byContradiction. eapply star_final_not_forever_reactive; eauto.
+(* goes wrong, terminate *)
+  byContradiction. eapply terminates_not_goes_wrong with (s1 := s'0) (s2 := s'); eauto.
+(* goes wrong, diverges *)
+  byContradiction. eapply star2_final_not_forever_silent with (s1 := s') (s2 := s'0); eauto.
+(* goes wrong, reacts *)
+  byContradiction. eapply star_final_not_forever_reactive; eauto.
+(* goes wrong, goes wrong *)
+  assert (t = t0 /\ s' = s'0). eapply steps_deterministic; eauto.
+  destruct H3. congruence.
+(* goes initially wrong, goes initially wrong *)
+  reflexivity.
+Qed.
+
+End DETERM_SEM.
diff --git a/common/Events.v b/common/Events.v
index 011c454b2..0f5d9d218 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -43,8 +43,7 @@ Record event : Type := mkevent {
 }.
 
 (** The dynamic semantics for programs collect traces of events.
-  Traces are of two kinds: finite (type [trace]) 
-  or possibly infinite (type [traceinf]). *)
+  Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
 
 Definition trace := list event.
 
@@ -57,7 +56,6 @@ Definition Eextcall
 Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.
 
 CoInductive traceinf : Type :=
-  | Enilinf: traceinf
   | Econsinf: event -> traceinf -> traceinf.
 
 Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf :=
@@ -81,6 +79,9 @@ Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed.
 Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
 Proof. intros. unfold Eapp, trace. apply app_ass. Qed.
 
+Lemma Eapp_E0_inv: forall t1 t2, t1 ** t2 = E0 -> t1 = E0 /\ t2 = E0.
+Proof (@app_eq_nil event).
+  
 Lemma E0_left_inf: forall T, E0 *** T = T.
 Proof. auto. Qed.
 
@@ -226,8 +227,6 @@ End EVENT_MATCH_LESSDEF.
 (** Bisimilarity between infinite traces. *)
 
 CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
-  | traceinf_sim_nil:
-      traceinf_sim Enilinf Enilinf
   | traceinf_sim_cons: forall e T1 T2,
       traceinf_sim T1 T2 ->
       traceinf_sim (Econsinf e T1) (Econsinf e T2).
@@ -236,7 +235,7 @@ Lemma traceinf_sim_refl:
   forall T, traceinf_sim T T.
 Proof.
   cofix COINDHYP; intros.
-  destruct T. constructor. constructor. apply COINDHYP.
+  destruct T. constructor. apply COINDHYP.
 Qed.
  
 Lemma traceinf_sim_sym:
@@ -252,15 +251,16 @@ Proof.
   cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
 Qed.
 
-(** The "is prefix of" relation between infinite traces. *)
+(** The "is prefix of" relation between a finite and an infinite trace. *)
 
-CoInductive traceinf_prefix: traceinf -> traceinf -> Prop :=
+Inductive traceinf_prefix: trace -> traceinf -> Prop :=
   | traceinf_prefix_nil: forall T,
-      traceinf_prefix Enilinf T
-  | traceinf_prefix_cons: forall e T1 T2,
-      traceinf_prefix T1 T2 ->
-      traceinf_prefix (Econsinf e T1) (Econsinf e T2).
+      traceinf_prefix nil T
+  | traceinf_prefix_cons: forall e t1 T2,
+      traceinf_prefix t1 T2 ->
+      traceinf_prefix (e :: t1) (Econsinf e T2).
 
+(*
 Lemma traceinf_prefix_compat:
   forall T1 T2 T1' T2',
   traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
@@ -271,31 +271,16 @@ Proof.
 Qed.
 
 Transparent trace E0 Eapp Eappinf.
+*)
 
 Lemma traceinf_prefix_app:
-  forall T1 T2 t,
-  traceinf_prefix T1 T2 ->
-  traceinf_prefix (t *** T1) (t *** T2).
+  forall t1 T2 t,
+  traceinf_prefix t1 T2 ->
+  traceinf_prefix (t ** t1) (t *** T2).
 Proof.
-  induction t; simpl; intros. auto. constructor. auto.
-Qed.
-
-Lemma traceinf_sim_prefix:
-  forall T1 T2,
-  traceinf_sim T1 T2 -> traceinf_prefix T1 T2.
-Proof.
-  cofix COINDHYP; intros. 
-  inv H. constructor. constructor. apply COINDHYP; auto.
-Qed.
-
-Lemma traceinf_prefix_2_sim:
-  forall T1 T2,
-  traceinf_prefix T1 T2 -> traceinf_prefix T2 T1 ->
-  traceinf_sim T1 T2.
-Proof.
-  cofix COINDHYP; intros. 
-  inv H.
-  inv H0. constructor.
-  inv H0. constructor. apply COINDHYP; auto.
+  induction t; simpl; intros. auto.
+  change ((a :: t) ** t1) with (a :: (t ** t1)).
+  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
+  constructor. auto.
 Qed.
 
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 9e9063b08..deab49b68 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.
 
diff --git a/driver/Complements.v b/driver/Complements.v
index dfd3c4547..6fe503818 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -20,6 +20,7 @@ Require Import Values.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
+Require Import Determinism.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Asm.
@@ -29,159 +30,8 @@ Require Import Errors.
 (** * Determinism of Asm semantics *)
 
 (** In this section, we show that the semantics for the Asm language
-  are deterministic, in a sense to be made precise later.
-  There are two sources of apparent non-determinism:
-- The semantics leaves unspecified the results of calls to external 
-  functions.  Different results to e.g. a "read" operation can of
-  course lead to different behaviors for the program.
-  We address this issue by modeling a notion of deterministic
-  external world that uniquely determines the results of external calls.
-- For diverging executions, the trace of I/O events is not uniquely
-  determined: it can contain events that will never be performed
-  because the program diverges earlier.  We address this issue
-  by showing the existence of a minimal trace for diverging executions.
-
-*)
-
-(** ** Deterministic worlds *)
-
-(** An external world is a function that, given the name of an
-  external call and its arguments, returns either [None], meaning
-  that this external call gets stuck, or [Some(r,w)], meaning
-  that this external call succeeds, has result [r], and changes
-  the world to [w]. *)
-
-Inductive world: Type :=
-  World: (ident -> list eventval -> option (eventval * world)) -> world.
-
-Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
-                     option (eventval * world) :=
-  match w with World f => f evname evargs end.
-
-(** A trace is possible in a given world if all events correspond
-  to non-stuck external calls according to the given world.
-  Two predicates are defined, for finite and infinite traces respectively:
-- [possible_trace w t w'], where [w] is the initial state of the
-  world, [t] the finite trace of interest, and [w'] the state of the
-  world after performing trace [t].
-- [possible_traceinf w T], where [w] is the initial state of the
-  world and [T] the possibly infinite trace of interest.
-*)
-
-Inductive possible_trace: world -> trace -> world -> Prop :=
-  | possible_trace_nil: forall w,
-      possible_trace w E0 w
-  | possible_trace_cons: forall w0 evname evargs evres w1 t w2,
-      nextworld w0 evname evargs = Some (evres, w1) ->
-      possible_trace w1 t w2 ->
-      possible_trace w0 (mkevent evname evargs evres :: t) w2.
-
-Lemma possible_trace_app:
-  forall t2 w2 w0 t1 w1,
-  possible_trace w0 t1 w1 -> possible_trace w1 t2 w2 ->
-  possible_trace w0 (t1 ** t2) w2.
-Proof.
-  induction 1; simpl; intros.
-  auto.
-  econstructor; eauto.
-Qed.
-
-Lemma possible_trace_app_inv:
-  forall t2 w2 t1 w0,
-  possible_trace w0 (t1 ** t2) w2 ->
-  exists w1, possible_trace w0 t1 w1 /\ possible_trace w1 t2 w2.
-Proof.
-  induction t1; simpl; intros.
-  exists w0; split. constructor. auto.
-  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
-  exists w1; split. econstructor; eauto. auto.
-Qed.
-
-CoInductive possible_traceinf: world -> traceinf -> Prop :=
-  | possible_traceinf_nil: forall w0,
-      possible_traceinf w0 Enilinf
-  | possible_traceinf_cons: forall w0 evname evargs evres w1 T,
-      nextworld w0 evname evargs = Some (evres, w1) ->
-      possible_traceinf w1 T ->
-      possible_traceinf w0 (Econsinf (mkevent evname evargs evres) T).
-
-Lemma possible_traceinf_app:
-  forall t2 w0 t1 w1,
-  possible_trace w0 t1 w1 -> possible_traceinf w1 t2 ->
-  possible_traceinf w0 (t1 *** t2).
-Proof.
-  induction 1; simpl; intros.
-  auto.
-  econstructor; eauto.
-Qed.
-
-Lemma possible_traceinf_app_inv:
-  forall t2 t1 w0,
-  possible_traceinf w0 (t1 *** t2) ->
-  exists w1, possible_trace w0 t1 w1 /\ possible_traceinf w1 t2.
-Proof.
-  induction t1; simpl; intros.
-  exists w0; split. constructor. auto.
-  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
-  exists w1; split. econstructor; eauto. auto.
-Qed.
-
-Ltac possibleTraceInv :=
-  match goal with
-  | [H: possible_trace _ (_ ** _) _ |- _] =>
-      let P1 := fresh "P" in
-      let w := fresh "w" in
-      let P2 := fresh "P" in
-      elim (possible_trace_app_inv _ _ _ _ H); clear H;
-      intros w [P1 P2];
-      possibleTraceInv
-  | [H: possible_traceinf _ (_ *** _) |- _] =>
-      let P1 := fresh "P" in
-      let w := fresh "w" in
-      let P2 := fresh "P" in
-      elim (possible_traceinf_app_inv _ _ _ H); clear H;
-      intros w [P1 P2];
-      possibleTraceInv
-  | _ => idtac
-  end.
-
-(** Determinism properties of [event_match]. *)
-
-Remark eventval_match_deterministic:
-  forall ev1 ev2 ty v1 v2,
-  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 ->
-  (ev1 = ev2 <-> v1 = v2).
-Proof.
-  intros. inv H; inv H0; intuition congruence.
-Qed.
-
-Remark eventval_list_match_deterministic:
-  forall ev1 ty v, eventval_list_match ev1 ty v ->
-  forall ev2, eventval_list_match ev2 ty v -> ev1 = ev2.
-Proof.
-  induction 1; intros.
-  inv H. auto.
-  inv H1. decEq.
-  rewrite (eventval_match_deterministic _ _ _ _ _ H H6). auto.
-  eauto.
-Qed.
-
-Lemma event_match_deterministic:
-  forall w0 t1 w1 t2 w2 ef vargs vres1 vres2,
-  possible_trace w0 t1 w1 ->
-  possible_trace w0 t2 w2 ->
-  event_match ef vargs t1 vres1 ->
-  event_match ef vargs t2 vres2 ->
-  vres1 = vres2 /\ t1 = t2 /\ w1 = w2.
-Proof.
-  intros. inv H1. inv H2. 
-  assert (eargs = eargs0). eapply eventval_list_match_deterministic; eauto. subst eargs0.
-  inv H. inv H12. inv H0. inv H12.
-  rewrite H11 in H10. inv H10. intuition. 
-  rewrite <- (eventval_match_deterministic _ _ _ _ _ H4 H5). auto.
-Qed.
-
-(** ** Determinism of Asm transitions. *)
+  are deterministic, provided that the program is executed against a
+  deterministic world, as formalized in module [Determinism]. *)
 
 Remark extcall_arguments_deterministic:
   forall rs m sg args args',
@@ -199,22 +49,26 @@ Proof.
   unfold extcall_arguments; intros; eauto.
 Qed.
 
-Lemma step_deterministic:
-  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
-  step ge s0 t1 s1 -> step ge s0 t2 s2 ->
-  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
-  s1 = s2 /\ t1 = t2 /\ w1 = w2.
+Lemma step_internal_deterministic:
+  forall ge s t1 s1 t2 s2,
+  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> internal_determinism _ t1 s1 t2 s2.
 Proof.
   intros. inv H; inv H0.
-  assert (c0 = c) by congruence. subst c0.
-  assert (i0 = i) by congruence. subst i0.
-  split. congruence. split. auto. inv H1; inv H2; auto.
+  assert (c0 = c) by congruence.
+  assert (i0 = i) by congruence.
+  assert (rs'0 = rs') by congruence.
+  assert (m'0 = m') by congruence.
+  subst. constructor.
   congruence.
   congruence.
   assert (ef0 = ef) by congruence. subst ef0.
   assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0.
-  exploit event_match_deterministic. eexact H1. eexact H2. eauto. eauto.
-  intros [A [B C]]. intuition congruence.
+  inv H3; inv H8.
+  assert (eargs0 = eargs). eapply eventval_list_match_deterministic; eauto. subst eargs0.
+  constructor. intros.
+  exploit eventval_match_deterministic. eexact H0. eexact H5. intros. 
+  assert (res = res0). tauto. 
+  congruence.
 Qed.
 
 Lemma initial_state_deterministic:
@@ -224,10 +78,8 @@ Proof.
   intros. inv H; inv H0. reflexivity. 
 Qed.
 
-Definition nostep (ge: genv) (st: state) : Prop := forall t st', ~step ge st t st'.
-
 Lemma final_state_not_step:
-  forall ge st r, final_state st r -> nostep ge st.
+  forall ge st r, final_state st r -> nostep step ge st.
 Proof.
   unfold nostep. intros. red; intros. inv H. inv H0.
   unfold Vzero in H1. congruence.
@@ -240,373 +92,41 @@ Proof.
   intros. inv H; inv H0. congruence.
 Qed.
 
-(** ** Determinism for terminating executions. *)
-
-Lemma steps_deterministic:
-  forall ge s0 t1 s1, star step ge s0 t1 s1 -> 
-  forall t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> 
-  nostep ge s1 -> nostep ge s2 ->
-  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
-  t1 = t2 /\ s1 = s2.
-Proof.
-  induction 1; intros. 
-  inv H. auto. 
-  elim (H0 _ _ H4).
-  inv H2. elim (H4 _ _ H). 
-  possibleTraceInv.
-  exploit step_deterministic. eexact H. eexact H7. eauto. eauto. 
-  intros [A [B C]]. subst s5 t3 w3.
-  exploit IHstar; eauto. intros [A B]. split; congruence.
-Qed.
-
-(** ** Determinism for infinite transition sequences. *)
-
-Lemma forever_star_inv:
-  forall ge s t s', star step ge s t s' ->
-  forall T w w', forever step ge s T ->
-  possible_trace w t w' -> possible_traceinf w T ->
-  exists T',
-  forever step ge s' T' /\ possible_traceinf w' T' /\ T = t *** T'.
-Proof.
-  induction 1; intros.
-  inv H0. exists T; auto.
-  subst t. possibleTraceInv. 
-  inv H2. possibleTraceInv. 
-  exploit step_deterministic.
-    eexact H. eexact H1. eauto. eauto. intros [A [B C]]; subst s4 t1 w1.
-  exploit IHstar; eauto. intros [T' [A [B C]]]. 
-  exists T'; split. auto.
-  split. auto.
-  rewrite C. rewrite Eappinf_assoc; auto.
-Qed.
-
-Lemma star_final_not_forever:
-  forall ge s1 t s2 T w1 w2,
-  star step ge s1 t s2 ->
-  nostep ge s2 -> forever step ge s1 T ->
-  possible_trace w1 t w2 -> possible_traceinf w1 T ->
-  False.
-Proof.
-  intros. exploit forever_star_inv; eauto. intros [T' [A [B C]]]. 
-  inv A. elim (H0 _ _ H4). 
-Qed.
-
-(** ** Minimal traces for divergence. *)
-
-(** There are two mutually exclusive way in which a program can diverge.
-  It can diverge in a reactive fashion: it performs infinitely many
-  external calls, and the internal computations between two external
-  calls are always finite.  Or it can diverge silently: after a finite
-  number of external calls, it enters an infinite sequence of internal
-  computations. *)
-
-Definition reactive (ge: genv) (s: state) (w: world) :=
-  forall t s1 w1,
-  star step ge s t s1 -> possible_trace w t w1 ->
-  exists s2, exists t', exists s3, exists w2,
-  star step ge s1 E0 s2 
-  /\ step ge s2 t' s3
-  /\ possible_trace w1 t' w2
-  /\ t' <> E0.
-
-Definition diverges_silently (ge: genv) (s: state) :=
-  forall s2, star step ge s E0 s2 -> exists s3, step ge s2 E0 s3.
-
-Definition diverges_eventually (ge: genv) (s: state) (w: world) :=
-  exists t, exists s1, exists w1,
-  star step ge s t s1 /\ possible_trace w t w1 /\ diverges_silently ge s1.
-
-(** Using classical logic, we show that any infinite sequence of transitions
-  that is possible in a deterministic world is of one of the two forms 
-  described above. *)
-
-Lemma reactive_or_diverges:
-  forall ge s T w,
-  forever step ge s T -> possible_traceinf w T ->
-  reactive ge s w \/ diverges_eventually ge s w.
-Proof.
-  intros. elim (classic (diverges_eventually ge s w)); intro.
-  right; auto.
-  left. red; intros.
-  generalize (not_ex_all_not trace _ H1 t).
-  intro. clear H1.
-  generalize (not_ex_all_not state _ H4 s1).
-  intro. clear H4.
-  generalize (not_ex_all_not world _ H1 w1).
-  intro. clear H1.
-  elim (not_and_or _ _ H4); clear H4; intro.
-  contradiction.
-  elim (not_and_or _ _ H1); clear H1; intro.
-  contradiction.
-  generalize (not_all_ex_not state _ H1). intros [s2 A]. clear H1.
-  destruct (imply_to_and _ _ A). clear A.
-  exploit forever_star_inv.
-    eapply star_trans. eexact H2. eexact H1. reflexivity.
-    eauto. rewrite E0_right. eauto. eauto. 
-  intros [T' [A [B C]]]. 
-  inv A. possibleTraceInv. 
-  exists s2; exists t0; exists s3; exists w4. intuition.
-  subst t0. apply H4. exists s3; auto.
-Qed.
-
-(** Moreover, a program cannot be both reactive and silently diverging. *)
-
-Lemma reactive_not_diverges:
-  forall ge s w,
-  reactive ge s w -> diverges_eventually ge s w -> False.
-Proof.
-  intros. destruct H0 as [t [s1 [w1 [A [B C]]]]]. 
-  destruct (H _ _ _ A B) as [s2 [t' [s3 [w2 [P [Q [R S]]]]]]].
-  destruct (C _ P) as [s4 T].
-  assert (s3 = s4 /\ t' = E0 /\ w2 = w1).
-    eapply step_deterministic; eauto. constructor.
-  intuition congruence.
-Qed.
-
-(** A program that silently diverges can be given any finite or
-  infinite trace of events.  In particular, taking [T' = Enilinf],
-  it can be given the empty trace of events. *)
-
-Lemma diverges_forever:
-  forall ge s1 T w T',
-  diverges_silently ge s1 ->
-  forever step ge s1 T ->
-  possible_traceinf w T ->
-  forever step ge s1 T'.
-Proof.
-  cofix COINDHYP; intros. inv H0. possibleTraceInv. 
-  assert (exists s3, step ge s1 E0 s3). apply H. constructor.
-  destruct H0 as [s3 C]. 
-  assert (s2 = s3 /\ t = E0 /\ w0 = w). eapply step_deterministic; eauto. constructor.
-  destruct H0 as [Q [R S]]. subst s3 t w0. 
-  change T' with (E0 *** T'). econstructor. eassumption. 
-  eapply COINDHYP; eauto. 
-  red; intros. apply H. eapply star_left; eauto. 
-Qed.
-
-(** The trace of I/O events generated by a reactive diverging program
-  is uniquely determined up to bisimilarity. *)
-
-Lemma reactive_sim:
-  forall ge s w T1 T2,
-  reactive ge s w ->
-  forever step ge s T1 ->
-  forever step ge s T2 ->
-  possible_traceinf w T1 ->
-  possible_traceinf w T2 ->
-  traceinf_sim T1 T2.
-Proof.
-  cofix COINDHYP; intros.
-  elim (H E0 s w); try constructor. 
-  intros s2 [t' [s3 [w2 [A [B [C D]]]]]].
-  assert (star step ge s t' s3). eapply star_right; eauto. 
-  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H0 C H2)
-  as [T1' [P [Q R]]].
-  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H1 C H3)
-  as [T2' [S [T U]]].
-  destruct t'. unfold E0 in D. congruence.
-  assert (t' = nil). inversion B. inversion H7. auto. subst t'.
-  subst T1 T2. simpl. constructor.
-  apply COINDHYP with ge s3 w2; auto.
-  red; intros. eapply H. eapply star_trans; eauto.
-  eapply possible_trace_app; eauto. 
-Qed.
-
-(** A trace is minimal for a program if it is a prefix of all possible
-  traces. *)
-
-Definition minimal_trace (ge: genv) (s: state) (w: world) (T: traceinf) :=
-  forall T',
-  forever step ge s T' -> possible_traceinf w T' ->
-  traceinf_prefix T T'.
-
-(** For any program that diverges with some possible trace [T1],
-  the set of possible traces admits a minimal element [T].
-  If the program is reactive, this trace is [T1]. 
-  If the program silently diverges, this trace is the finite trace
-  of events performed prior to silent divergence. *)
-
-Lemma forever_minimal_trace:
-  forall ge s T1 w,
-  forever step ge s T1 -> possible_traceinf w T1 ->
-  exists T,
-     forever step ge s T
-  /\ possible_traceinf w T
-  /\ minimal_trace ge s w T.
+Theorem asm_exec_program_deterministic:
+  forall p w beh1 beh2,
+  Asm.exec_program p beh1 -> Asm.exec_program p beh2 ->
+  possible_behavior w beh1 -> possible_behavior w beh2 ->
+  beh1 = beh2.
 Proof.
   intros. 
-  destruct (reactive_or_diverges _ _ _ _ H H0).
-  (* reactive *)
-  exists T1; split. auto. split. auto. red; intros.
-  elim (reactive_or_diverges _ _ _ _ H2 H3); intro.
-  apply traceinf_sim_prefix. eapply reactive_sim; eauto. 
-  elimtype False. eapply reactive_not_diverges; eauto.
-  (* diverges *) 
-  elim H1. intros t [s1 [w1 [A [B C]]]].
-  exists (t *** Enilinf); split.
-  exploit forever_star_inv; eauto. intros [T' [P [Q R]]]. 
-  eapply star_forever. eauto. 
-  eapply diverges_forever; eauto.
-  split. eapply possible_traceinf_app. eauto. constructor. 
-  red; intros. exploit forever_star_inv. eauto. eexact H2. eauto. eauto.
-  intros [T2 [P [Q R]]].
-  subst T'. apply traceinf_prefix_app. constructor.
-Qed.
-
-(** ** Refined semantics for program executions. *)
-
-(** We now define the following variant [exec_program'] of the
-  [exec_program] predicate defined in module [Smallstep].
-  In the diverging case [Diverges T], the new predicate imposes that the
-  finite or infinite trace [T] is minimal. *)
-
-Inductive exec_program' (p: program) (w: world): program_behavior -> Prop :=
-  | program_terminates': forall s t s' w' r,
-      initial_state p s ->
-      star step (Genv.globalenv p) s t s' ->
-      possible_trace w t w' ->
-      final_state s' r ->
-      exec_program' p w (Terminates t r)
-  | program_diverges': forall s T,
-      initial_state p s ->
-      forever step (Genv.globalenv p) s T ->
-      possible_traceinf w T ->
-      minimal_trace (Genv.globalenv p) s w T ->
-      exec_program' p w (Diverges T)
-  | program_goes_wrong': forall s t s' w',
-      initial_state p s ->
-      star step (Genv.globalenv p) s t s' ->
-      possible_trace w t w' -> 
-      nostep (Genv.globalenv p) s' ->
-       (forall r, ~final_state s' r) ->
-      exec_program' p w (Goes_wrong t).
-
-(** We show that any [exec_program] execution corresponds to
-  an [exec_program'] execution. *)
-
-Definition possible_behavior (w: world) (b: program_behavior) : Prop :=
-  match b with
-  | Terminates t r => exists w', possible_trace w t w'
-  | Diverges T => possible_traceinf w T
-  | Goes_wrong t => exists w', possible_trace w t w'
-  end.
-
-Inductive matching_behaviors: program_behavior -> program_behavior -> Prop :=
-  | matching_behaviors_terminates: forall t r,
-      matching_behaviors (Terminates t r) (Terminates t r)
-  | matching_behaviors_diverges: forall T1 T2,
-      traceinf_prefix T2 T1 ->
-      matching_behaviors (Diverges T1) (Diverges T2)
-  | matching_behaviors_goeswrong: forall t ,
-      matching_behaviors (Goes_wrong t) (Goes_wrong t).
-
-Theorem exec_program_program':
-  forall p b w,
-  exec_program p b -> possible_behavior w b ->
-  exists b', exec_program' p w b' /\ matching_behaviors b b'.
-Proof.
-  intros. inv H; simpl in H0.
-  (* termination *)
-  destruct H0 as [w' A].
-  exists (Terminates t r).
-  split. econstructor; eauto. constructor.
-  (* divergence *)
-  exploit forever_minimal_trace; eauto. intros [T0 [A [B C]]].
-  exists (Diverges T0); split.
-  econstructor; eauto.
-  constructor. apply C; auto.
-  (* going wrong *)
-  destruct H0 as [w' A].
-  exists (Goes_wrong t).
-  split. econstructor; eauto. constructor.
-Qed.
-
-(** Moreover, [exec_program'] is deterministic, in that the behavior
-  associated with a given program and external world is uniquely
-  defined up to bisimilarity between infinite traces. *)
-
-Inductive same_behaviors: program_behavior -> program_behavior -> Prop :=
-  | same_behaviors_terminates: forall t r,
-      same_behaviors (Terminates t r) (Terminates t r)
-  | same_behaviors_diverges: forall T1 T2,
-      traceinf_sim T2 T1 ->
-      same_behaviors (Diverges T1) (Diverges T2)
-  | same_behaviors_goes_wrong: forall t,
-      same_behaviors (Goes_wrong t) (Goes_wrong t).
-
-Theorem exec_program'_deterministic:
-  forall p b1 b2 w,
-  exec_program' p w b1 -> exec_program' p w b2 ->
-  same_behaviors b1 b2.
-Proof.
-  intros. inv H; inv H0;
-  try (assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0).
-  (* terminates, terminates *)
-  exploit steps_deterministic. eexact H2. eexact H5.
-  eapply final_state_not_step; eauto. eapply final_state_not_step; eauto. eauto. eauto.
-  intros [A B]. subst. 
-  exploit final_state_deterministic. eexact H4. eexact H7.
-  intro. subst. constructor.
-  (* terminates, diverges *)
-  byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto.
-  (* terminates, goes wrong *)
-  exploit steps_deterministic. eexact H2. eexact H5.
-  eapply final_state_not_step; eauto. auto. eauto. eauto.
-  intros [A B]. subst. elim (H8 _ H4).
-  (* diverges, terminates *)
-  byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto.
-  (* diverges, diverges *)
-  constructor. apply traceinf_prefix_2_sim; auto.
-  (* diverges, goes wrong *)
-  byContradiction. eapply star_final_not_forever; eauto.
-  (* goes wrong, terminates *)
-  exploit steps_deterministic. eexact H2. eexact H6. eauto. 
-  eapply final_state_not_step; eauto. eauto. eauto.
-  intros [A B]. subst. elim (H5 _ H8).
-  (* goes wrong, diverges *)
-  byContradiction. eapply star_final_not_forever; eauto.
-  (* goes wrong, goes wrong *)
-  exploit steps_deterministic. eexact H2. eexact H6.
-  eauto. eauto. eauto. eauto.
-  intros [A B]. subst. constructor.
-Qed.
-
-Lemma matching_behaviors_same:
-  forall b b1' b2',
-  matching_behaviors b b1' -> same_behaviors b1' b2' ->
-  matching_behaviors b b2'.
-Proof.
-  intros. inv H; inv H0. 
-  constructor.
-  constructor. apply traceinf_prefix_compat with T2 T1.
-  auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl.
-  constructor.
+  eapply (program_behaves_deterministic _ _ step (initial_state p) final_state); eauto.
+  exact step_internal_deterministic.
+  exact (initial_state_deterministic p).
+  exact final_state_deterministic.
+  exact final_state_not_step.
 Qed.
 
 (** * Additional semantic preservation property *)
 
-(** Combining the semantic preservation theorem from module [Main]
+(** Combining the semantic preservation theorem from module [Compiler]
   with the determinism of Asm executions, we easily obtain
   additional, stronger semantic preservation properties.
   The first property states that, when compiling a Clight
   program that has well-defined semantics, all possible executions
   of the resulting Asm code correspond to an execution of
-  the source Clight program, in the sense of the [matching_behaviors]
-  predicate. *)
+  the source Clight program. *)
 
-Theorem transf_c_program_correct_strong:
+Theorem transf_c_program_is_refinement:
   forall p tp w,
   transf_c_program p = OK tp ->
   (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->
-  (forall b, exec_program' tp w b -> exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b).
+  (forall b, Asm.exec_program tp b -> possible_behavior w b -> Csem.exec_program p b).
 Proof.
   intros. destruct H0 as [b0 [A [B C]]]. 
   assert (Asm.exec_program tp b0).
     eapply transf_c_program_correct; eauto.
-  exploit exec_program_program'; eauto. 
-  intros [b1 [D E]].
-  assert (same_behaviors b1 b). eapply exec_program'_deterministic; eauto.
-  exists b0. split. auto. eapply matching_behaviors_same; eauto.
+  assert (b = b0). eapply asm_exec_program_deterministic; eauto.
+  subst b0. auto.
 Qed.
 
 Section SPECS_PRESERVED.
@@ -619,37 +139,19 @@ Section SPECS_PRESERVED.
 
 Variable spec: program_behavior -> Prop.
 
-(* Since the execution trace for a diverging Clight program
-   is not uniquely defined (the trace can contain events that
-   the program will never perform because it loops earlier),
-   this result holds only if the specification is closed under
-   prefixes in the case of diverging executions.  This is the
-   case for all safety properties (some undesirable event never
-   occurs), but not for liveness properties (some desirable event
-   always occurs). *)
-
-Hypothesis spec_safety:
-  forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T).
+Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.
 
 Theorem transf_c_program_preserves_spec:
   forall p tp w,
   transf_c_program p = OK tp ->
-  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->
-  (forall b, Csem.exec_program p b -> possible_behavior w b -> spec b) ->
-  (forall b, exec_program' tp w b -> not_wrong b /\ spec b).
+  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ spec b) ->
+  (forall b, Asm.exec_program tp b -> possible_behavior w b -> spec b).
 Proof.
   intros. destruct H0 as [b1 [A [B C]]].
   assert (Asm.exec_program tp b1).
     eapply transf_c_program_correct; eauto.
-  exploit exec_program_program'; eauto. 
-  intros [b' [D E]].
-  assert (same_behaviors b b'). eapply exec_program'_deterministic; eauto.
-  inv E; inv H3. 
-  auto.
-  split. simpl. auto. apply spec_safety with T1. 
-  eapply traceinf_prefix_compat. eauto. auto. apply traceinf_sim_refl.
-  auto.
-  simpl in C. contradiction.
+  assert (b1 = b). eapply asm_exec_program_deterministic; eauto. 
+  subst b1. auto.
 Qed.
 
 End SPECS_PRESERVED.
-- 
GitLab