From 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 12:53:19 +0000 Subject: Distinguish two kinds of nonterminating behaviors: silent divergence and reactive divergence. As a consequence: - Removed the Enilinf constructor from traceinf (values of traceinf type are always infinite traces). - Traces are now uniquely defined. - Adapted proofs big step -> small step for Clight and Cminor accordingly. - Strengthened results in driver/Complements accordingly. - Added common/Determinism to collect generic results about deterministic semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Determinism.v | 508 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 508 insertions(+) create mode 100644 common/Determinism.v (limited to 'common/Determinism.v') diff --git a/common/Determinism.v b/common/Determinism.v new file mode 100644 index 00000000..430ee93d --- /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. -- cgit