Library Determinism

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.






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.






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).






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.






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).






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.

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.






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).






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.






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.






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.

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.






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.






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.






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'.






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.






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'.






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.






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'.






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.

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.






End DETERM_SEM.