diff options
| -rw-r--r-- | .depend | 10 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Cminor.v | 47 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 13 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 56 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 19 | ||||
| -rw-r--r-- | common/Determinism.v | 508 | ||||
| -rw-r--r-- | common/Events.v | 55 | ||||
| -rw-r--r-- | common/Smallstep.v | 287 | ||||
| -rw-r--r-- | driver/Complements.v | 576 |
10 files changed, 916 insertions, 657 deletions
@@ -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 @@ -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 b48db2d..8cc2185 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 f466a90..83e82e1 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 fb8b8e1..e0d05f2 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 6a8b676..836f1e4 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 0000000..430ee93 --- /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 011c454..0f5d9d2 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 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. diff --git a/driver/Complements.v b/driver/Complements.v index dfd3c45..6fe5038 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. |