Changeset 2914


Ignore:
Timestamp:
Mar 20, 2013, 8:39:37 AM (4 years ago)
Author:
campbell
Message:

Use single definition for stack measurement.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2897 r2914  
    130130  (λg,s. RTLabs_classify (Ras_state … s))
    131131  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
    132 
    133 definition lift_some : ∀A,B:Type[0]. (A → B) → A → option B ≝
    134 λA,B,f,a. Some B (f a).
    135 
    136 definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → nat → nat ≝
    137 λS,s1,s2,tlr,stack_cost,currentfn,initial.
    138   maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)).
    139132
    140133lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
     
    731724] qed.
    732725
     726definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → stacksize_info → stacksize_info ≝
     727λS,s1,s2,tlr,stack_cost,currentfn,initial.
     728  update_stacksize_info stack_cost initial (extract_call_ud_from_tlr S s1 s2 tlr currentfn).
     729
    733730
    734731
     
    743740  measurable RTLabs_pcsys p m n stack_cost max →
    744741  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
    745   let midstack ≝ \fst (measure_stack stack_cost 0 prefix) in
     742  let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in
    746743  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    747744  state_at RTLabs_ext_pcsys p m = return sm ∧
    748745  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    749   le (max_stack_of_tlr ??? tlr (lift_some … stack_cost) fn midstack) max ∧
     746  le (maximum (max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧
    750747  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
    751748#p #m #n #stack_cost #max #prefix #interesting
  • src/common/Measurable.ma

    r2896 r2914  
    11include "common/Executions.ma".
    2 include "common/StructuredTraces.ma".  (* just for status_class *)
     2include "common/stacksize.ma".
    33
    44(* A small-step executable semantics, together with some kind of global
     
    255255] qed.
    256256
    257 (* Measuring stack usage.  TODO: I think there's another version of this from
    258    the back-end that should be merged. *) 
    259 
    260 definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
    261 λcosts,start.
    262   foldl ?? (λx. λev.
    263     match ev with
    264     [ IEVcall id ⇒
    265         let 〈current_stack,max_stack〉 ≝ x in
    266         let new_stack ≝ current_stack + costs id in
    267         〈new_stack, max new_stack max_stack〉
    268     | IEVret id ⇒
    269         let 〈current_stack,max_stack〉 ≝ x in
    270         〈current_stack - costs id, max_stack〉
    271     | _ ⇒ x
    272     ]) 〈start,start〉.
    273 
    274 definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
    275 λcosts, start, trace. \snd (measure_stack costs start trace).
    276 
    277 lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
    278   (∀acc,el. P acc → P (f acc el)) →
    279   ∀l,acc. P acc →
    280   P (foldl A B f acc l).
    281 #A #B #P #f #IH #l elim l
    282 [ //
    283 | #h #t #IH' #acc #H @IH' @IH @H
    284 ] qed.
    285 (*
    286 lemma max_stack_step : ∀C,a,m,a',m',tr,s.
    287   measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
    288   m' = max m a'.
    289 #C #a #m #a' #m' #tr #s
    290 whd in match (measure_stack_aux ???);
    291 generalize in match (cs_stack C s); cases (cs_classify C s) #f
    292 normalize nodelta #E destruct //
    293 qed.
    294 
    295 lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
    296   measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
    297   measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
    298   a1' = a2'.
    299 #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
    300 whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
    301 generalize in match (cs_stack C s); cases (cs_classify C s) #f
    302 normalize nodelta
    303 #E1 #E2 destruct
    304 %
    305 qed.
    306 
    307 
    308 lemma max_stack_steps : ∀C,trace,a,m.
    309   \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
    310   max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
    311 #C #trace elim trace
    312 [ #a #m >max_n_O %
    313 | * #tr #s #tl #IH #a #m
    314   whd in match (foldl ?????);
    315   letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
    316   whd in match (foldl ??? 〈a,O〉 ?);
    317   letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
    318   >(IH a'') >IH
    319   >(max_stack_step … M)
    320   >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
    321 ] qed.
    322 
    323 lemma max_stack_append : ∀C,c1,ex1,ex2.
    324   max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
    325 #C #c1 #ex1 #ex2
    326 whd in match (max_stack ???); whd in match (stack_after ???);
    327 whd in match (max_stack ?? (ex1@ex2));
    328 whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
    329 generalize in match O; generalize in match c1; elim ex1
    330 [ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
    331 | * #tr #s #tl #IH #c #m
    332   whd in match (foldl ?????); whd in ⊢ (???(???%));
    333   lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
    334   cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
    335   >IH %
    336 ] qed.
    337 *) 
     257(* Measuring stack usage.  The intensional_event to cost part is handled by a
     258   common function with the structured traces version in common/stacksize.ma. *) 
     259
     260definition measure_stack : (ident → option nat) → stacksize_info → list intensional_event → stacksize_info ≝
     261λcosts,start,ev.
     262  update_stacksize_info costs start (extract_call_ud_from_observables ev).
     263
    338264
    339265(* Check that the trace ends with the return from the starting function and one
     
    379305definition measurable : ∀C:preclassified_system.
    380306  ∀p:program ?? C. nat → nat →
    381   (ident → nat) (* stack cost *) →
     307  (ident → option nat) (* stack cost *) →
    382308  nat → Prop ≝
    383309λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
     
    389315  trace_is_label_to_return C' interesting ∧
    390316  bool_to_Prop (will_return' C' interesting) ∧
    391   le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
     317  le (maximum (measure_stack stack_cost (mk_stacksize_info 0 0) (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting))))) max_allowed_stack.
    392318
    393319
Note: See TracChangeset for help on using the changeset viewer.