source: src/common/Measurable.ma @ 2541

Last change on this file since 2541 was 2534, checked in by campbell, 7 years ago

Tweak measurable definition to stop at the return from a function.

File size: 5.3 KB
Line 
1include "common/Executions.ma".
2include "common/StructuredTraces.ma".  (* just for status_class *)
3
4record classified_system : Type[2] ≝ {
5  cs_exec :> fullexec io_out io_in;
6  cs_global : global … cs_exec;
7  cs_labelled : state … cs_exec cs_global → bool;
8  cs_classify : state … cs_exec cs_global → status_class;
9  cs_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
10}.
11
12definition cs_state : classified_system → Type[0] ≝
13λC. state … C (cs_global … C).
14
15definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
16
17let rec split_trace FE (g:global io_out io_in FE) (x:execution (state ?? FE g) io_out io_in) (n:nat) on n : option (execution_prefix (state … FE g) × (execution (state ?? FE g) io_out io_in)) ≝
18match n with
19[ O ⇒ Some ? 〈[ ], x〉
20| S n' ⇒
21  match x with
22  [ e_step tr s x' ⇒
23    ! 〈pre,x''〉 ← split_trace FE g x' n';
24    Some ? 〈〈tr,s〉::pre,x''〉
25    (* Necessary for a measurable trace at the end of the program *)
26  | e_stop tr r s ⇒
27    match n' with
28    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
29    | _ ⇒ None ?
30    ]
31  | _ ⇒ None ?
32  ]
33].
34
35(* Ideally we would also allow measurable traces to be from one cost label to
36   another (in the same function call), but due to time constraints we'll stick
37   to ending measurable traces at the end of the function only.
38 *)
39
40definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝
41λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
42
43definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
44λC.
45  foldl … (λx, trs.
46    let 〈current,max_stack〉 ≝ x in
47    let 〈tr,s〉 ≝ trs in
48    let new ≝
49      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
50      [ cl_call ⇒ λsc. current + sc I
51      | cl_return ⇒ λsc. current - sc I
52      | _ ⇒ λ_. current
53      ] (cs_stack C s) in
54    〈new, max max_stack new〉) 〈0,0〉.
55
56definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
57λC,x. \fst (measure_stack C x).
58
59definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
60λC,x. \snd (measure_stack C x).
61
62(* Check that the trace ends with the return from the starting function and one
63   further state. *)
64
65let rec will_return_aux C (depth:nat)
66                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
67match trace with
68[ nil ⇒ false
69| cons h tl ⇒
70  let 〈tr,s〉 ≝ h in
71  match cs_classify C s with
72  [ cl_call ⇒ will_return_aux C (S depth) tl
73  | cl_return ⇒
74      match depth with
75       (* We need to see the state after the return to build the structured
76          trace. *)
77      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
78      | S d ⇒ will_return_aux C d tl
79      ]
80  | _ ⇒ will_return_aux C depth tl
81  ]
82].
83definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
84
85record preclassified_system : Type[2] ≝ {
86  pcs_exec :> fullexec io_out io_in;
87  pcs_labelled : ∀g. state … pcs_exec g → bool;
88  pcs_classify : ∀g. state … pcs_exec g → status_class
89}.
90
91(* FIXME: this definition is unreasonable because it presumes we can easily
92   identify the change in stack usage from return states, but that information
93   is rather implicit (we only really record the function called in the
94   extended RTLabs states when building the structured traces). *)
95
96definition measurable : ∀C:preclassified_system.
97  ∀p:program ?? C. nat → nat →
98  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
99  nat → Prop ≝
100λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
101  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
102  let cl_trace ≝ exec_inf … (cs_exec … C') p in
103  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
104  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
105  trace_is_label_to_return C' interesting ∧
106  bool_to_Prop (will_return' C' interesting) ∧
107  le (max_stack C' (prefix@interesting)) max_allowed_stack.
108
109(* TODO: probably ought to be elsewhere
110
111   Note that this does not include stack space
112 *)
113
114definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
115λFE,p,m,n.
116  let trace ≝ exec_inf … FE p in
117  match split_trace FE ? trace m with
118  [ Some x ⇒
119    let 〈prefix,suffix〉 ≝ x in
120    match split_trace FE ? suffix n with
121    [ Some y ⇒
122      let interesting ≝ \fst y in
123      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
124    | _ ⇒ None ?
125    ]
126  | _ ⇒ None ?
127  ].
128
129definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
130λFE,p,m.
131  let trace ≝ exec_inf … FE p in
132  match split_trace FE ? trace m with
133  [ Some x ⇒
134    match \snd x with
135    [ e_step _ s _ ⇒ Some ? s
136    | e_stop _ _ s ⇒ Some ? s
137    | _ ⇒ None ?
138    ]
139  | _ ⇒ None ?
140  ].
Note: See TracBrowser for help on using the repository browser.