Changeset 2914
 Timestamp:
 Mar 20, 2013, 8:39:37 AM (4 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2897 r2914 130 130 (λg,s. RTLabs_classify (Ras_state … s)) 131 131 (λ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)).139 132 140 133 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. … … 731 724 ] qed. 732 725 726 definition 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 733 730 734 731 … … 743 740 measurable RTLabs_pcsys p m n stack_cost max → 744 741 observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → 745 let midstack ≝ \fst (measure_stack stack_cost 0 prefix)in742 let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in 746 743 ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 747 744 state_at RTLabs_ext_pcsys p m = return sm ∧ 748 745 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 ∧ 750 747 pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. 751 748 #p #m #n #stack_cost #max #prefix #interesting 
src/common/Measurable.ma
r2896 r2914 1 1 include "common/Executions.ma". 2 include "common/ StructuredTraces.ma". (* just for status_class *)2 include "common/stacksize.ma". 3 3 4 4 (* A smallstep executable semantics, together with some kind of global … … 255 255 ] qed. 256 256 257 (* Measuring stack usage. TODO: I think there's another version of this from 258 the backend 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 260 definition 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 338 264 339 265 (* Check that the trace ends with the return from the starting function and one … … 379 305 definition measurable : ∀C:preclassified_system. 380 306 ∀p:program ?? C. nat → nat → 381 (ident → nat) (* stack cost *) →307 (ident → option nat) (* stack cost *) → 382 308 nat → Prop ≝ 383 309 λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. … … 389 315 trace_is_label_to_return C' interesting ∧ 390 316 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. 392 318 393 319
Note: See TracChangeset
for help on using the changeset viewer.