Changeset 2914 for src/common
 Timestamp:
 Mar 20, 2013, 8:39:37 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.