abstract interpretation with applications to timing validation:应用到时序验证的抽象解释

上传人:a**** 文档编号:243317342 上传时间:2024-09-20 格式:PPT 页数:136 大小:1.53MB
返回 下载 相关 举报
abstract interpretation with applications to timing validation:应用到时序验证的抽象解释_第1页
第1页 / 共136页
abstract interpretation with applications to timing validation:应用到时序验证的抽象解释_第2页
第2页 / 共136页
abstract interpretation with applications to timing validation:应用到时序验证的抽象解释_第3页
第3页 / 共136页
点击查看更多>>
资源描述
Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Klicken Sie, um das Titelformat zu bearbeiten,Klicken Sie, um die Formate des Vorlagentextes zu bearbeiten,Zweite Ebene,Dritte Ebene,Vierte Ebene,Fnfte Ebene,Structure of the Lecture,Introduction,Static timing analysis,the problem,our approach,the success,tool architecture,Cache analysis,Pipeline analysis,Value analysis,Worst-case path determination,-,Timing Predictability,caches,non-cache-like devices,future architectures,Conclusion,Industrial Needs,Hard real-time systems, often in safety-critical applications abound,Aeronautics, automotive, train industries, manufacturing control,Wing vibration of airplane,sensing every 5 mSec,Sideairbag in car,Reaction in 10 mSec,crankshaft-synchronous tasks,have very tight deadlines, 45uS,Hard Real-Time Systems,Embedded controllers are expected to finish their tasks reliably within time bounds.,Task scheduling must be performed,Essential:,upper bound on the execution times,of all tasks statically known,Commonly called the,Worst-Case Execution Time (WCET),Analogously,Best-Case Execution Time (BCET),Timing Analysis,Embedded controllers are expected to finish their tasks reliably within time bounds.,The problem:,Given,a software to produce some reaction,a hardware platform, on which to execute the software,required reaction time.,Derive: a guarantee for timeliness.,Timing Analysis,provides parameters for schedulability analysis:,Execution time, C,i, of tasks, and if that is impossible,upper bounds and maybe also lower bounds on execution times of tasks, often called Worst-Case Execution Times (WCET) and Best-Case Execution Times (BCET).,Architecture,(constant,execution,times),Timing Analysis the Search Space,all control-flow paths (through the binary executable) depending on the possible,inputs,.,Feasible as search for a longest path if,iteration and recursion are bounded,execution time of instructions are (positive) constants.,Elegant method: Timing Schemata (Shaw 89) inductive calculation of upper bounds.,Software,Input,ub (,if,b,then,S1,else,S2) := ub (b) + max (ub (S1), ub (S2),High-Performance Microprosessors,increase (average-case) performance by using:,Caches, Pipelines, Branch Prediction, Speculation,These features make timing analysis difficult:Execution times of instructions vary widely,Best case,-,everything goes smoothly,: no cache miss, operands ready, resources free, branch correctly predicted,Worst case,-,everything goes wrong,: all loads miss the cache, resources are occupied, operands not ready,Span may be several hundred cycles,Variability of Execution Times,LOAD r2, _a,LOAD r1, _b,ADD r3,r2,r1,PPC 755,x = a + b;,In most cases, execution,will be fast.,So, assuming the worst case,is safe, but very pessimistic!,AbsInt,s,WCET Analyzer,aiT,IST Project DAEDALUS final review report:,The AbsInt tool is probably the,best of its kind in the world and it,is justified to consider this result,as a breakthrough.,”,Several time-critical subsystems of the Airbus A380,have been certified using aiT;,aiT is the only validated tool for these applications.,Tremendous Progressduring the past 15 Years,1995,2002,2005,over-estimation,20-30%,15%,30-50%,4,25,60,200,cache-miss penalty,Lim et al.,Thesing et al.,Souyris et al.,The explosion of penalties has been compensated,by the improvement of the analyses!,10%,25%,State-dependent Execution Times,Execution time depend on the execution state.,Execution state results from the execution history.,semantics state,:,values of variables,execution state,:,occupancy of,resources,state,Architecture,Timing Analysis the Search Spacewith,State-dependent Execution Times,all control-flow paths depending on the possible,inputs,all paths through the architecture for potential,initial,states,Software,Input,initial,state,mul rD, rA, rB,execution states for paths reaching this program point,instruction,in I-cache,instruction,not in I-cache,1,bus occupied,bus not occupied,small operands,large operands,1,4, 40,Architecture,Timing Analysis the Search Spacewith,out-of-order execution,all control-flow paths depending on the possible,inputs,all paths through the architecture for potential,initial,states,including,different schedules,for instruction sequences,Software,Input,initial,state,Architecture,Timing Analysis the Search Spacewith,multi-threading,all control-flow paths depending on the possible,inputs,all paths through the architecture for potential,initial,states,including,different schedules,for instruction sequences,including,different interleavings of accesses to shared resources,Software,Input,initial,state,Why Exhaustive Exploration?,Naive attempt: follow local worst-case transitions only,Unsound in the presence of,Timing Anomalies:,A path starting with a local worst case may have a lower overall execution time,Ex.: a cache miss preventing a branch mis-prediction,Caused by the interference between processor components: Ex.:,cache,hit/miss influences,branch prediction,;,branch prediction,causes,prefetching,;,prefetching,pollutes the,I-cache,.,State Space Explosion in Timing Analysis,constant,execution,times,state-dependentexecution times,out-of-orderexecution,preemptivescheduling,concurrency +shared resources,years +,methods,1995,2000,2010,Timing schemata,Static analysis,?,Caches, pipelines,speculation:combined cache andpipeline analysis,Superscalar processors:interleavingsof all schedules,Multi-core withshared resources:interleavingsof several threads,Notions in Timing Analysis,Hard or impossible to determine,Determine upper bounds instead,High-Level Requirements for Timing Analysis,Upper bounds must be,safe, i.e. not underestimated,Upper bounds should be,tight, i.e. not far away from real execution times,Analogous for lower bounds,Analysis effort must be,tolerable,Note: all analyzed programs are terminating,loop bounds need to be known,no decidability problem, but a complexity problem!,Our Approach,End-to-end measurement,is not possible because of the large state space.,We compute,bounds,for the execution times of,instructions,and,basic blocks,and determine a longest path in the basic-block graph of the program.,The,variability of execution times,may cancel out in end-to-end measurements, but that,s hard to quantify,exists,“,in pure form,”,on the instruction level.,Timing Accidents and Penalties,Timing Accident, cause for an increase of the execution time of an instruction,Timing Penalty, the associated increase,Types of timing accidents,Cache misses,Pipeline stalls,Branch mispredictions,Bus collisions,Memory refresh of DRAM,TLB miss,Execution Time is History-Sensitive,Contribution,of the execution of an instruction to a program,s execution time,depends on the execution state, e.g.,the time for a memory access depends on the cache state,the execution state depends on the execution history,needed: an,invariant,about the,set of execution states produced by all executions reaching a program point,.,We use,abstract interpretation,to compute these invariants.,Deriving Run-Time Guarantees,Our method and tool, aiT, derives,Safety Properties,from these invariants :,Certain timing accidents will never happen,.,Example:,At program point p, instruction fetch will never cause a cache miss.,The more accidents,excluded, the,lower,the,upper,bound.,Murphy,s,invariant,FastestVariance of execution timesSlowest,Abstract Interpretation in Timing Analysis,Abstract interpretation statically analyzes a program for a given property without executing it.,Derived properties therefore hold for all executions.,It is based on the semantics of the analyzed language.,A,semantics,of a programming language that talks about,time,needs to incorporate the,execution platform!,Static timing analysis is thus based on such a semantics.,The Architectural Abstraction inside the Timing Analyzer,Timing analyzer,Architectural abstractions,Cache,Abstraction,Pipeline,Abstraction,Value,Analysis,Control-Flow,Analysis,Loop-Bound,Analysis,abstractions of,the processor,s,arithmetic,Abstract Interpretation in Timing Analysis,Determines,invariants about the values of variables (in registers, on the stack),to compute loop bounds,to eliminate infeasible paths,to determine effective memory addresses,invariants on architectural execution state,Cache contents,predict hits & misses,Pipeline states,predict or exclude pipeline stalls,Tool Architecture,Abstract Interpretations,Abstract Interpretation,Integer Linear,Programming,Value,Analysis,Determines enclosing,intervals for the set of,values in registers and,local variables, used for,determining addresses.,Loop bound,analysis,Determines,loop bounds,Control Flow,Analysis,Determines infeasible paths,The Story in Detail,Tool Architecture,Value Analysis,Motivation,:,Provide access information to data-cache/pipeline analysis,Detect infeasible paths,Derive loop bounds,Method,:,calculate intervals at all program points, i.e. lower and upper bounds for the set of possible values occurring in the machine program (addresses, register contents, local and global variables) (Cousot/Halbwachs78),Value Analysis II,Intervals are computed along the CFG edges,At joins, intervals are unioned,“,D1: -2,+2,D1: -4,0,D1: -4,+2,move.l #4,D0,add.l D1,D0,move.l (A0,D0),D1,D1: -4,4, A0x1000,0x1000,D04,4, D1: -4,4,A0x1000,0x1000,D00,8, D1: -4,4,A0x1000,0x1000,access,0x1000,0x1008,Which address is accessed here?,Value Analysis (Airbus Benchmark),1Ghz Athlon, Memory usage Cache sets are,independent,:,Everything explained in terms of one set,LRU-Replacement Strategy,:,Replace the block that has been,L,east,R,ecently,U,sed,Modeled by,Ages,Example: 4-way set associative cache,age,0,1,2,3,m,0,m,1,Access,m,4,(miss),m,4,m,2,m,1,Access,m,1,(hit),m,0,m,4,m,2,m,1,m,5,Access,m,5,(miss),m,4,m,0,m,0,m,1,m,2,m,3,Cache Analysis,How to statically precompute cache contents:,Must Analysis,:For each program point (and context), find out which blocks,are,in the cache, prediction of cache hits,May Analysis,:,For each program point (and context), find out which blocks,may,be in the cacheComplement says what,is not,in the cache, prediction of cache misses,In the following, we consider must analysis until otherwise stated.,(Must) Cache Analysis,Consider one instruction in the program.,There may be many paths leading to this instruction.,How can we compute whether,a,will always be in cache independently of which path execution takes?,load a,Question:,Is the access to a,always a cache hit?,Determine Cache-Information(abstract cache states) at each Program Point,a, b,x,youngest age - 0,oldest age - 3,Interpretation of this cache information:,describes the set of all concrete cache states,in which,x, a,and,b,occur,x,with an age not older than 1,a,and,b,with an age not older than,2,Cache information contains,only memory blocks guaranteed to be in cache.,they are associated with their maximal age.,Cache- Information,Cache analysis,determines safe information about,Cache Hits.,Each predicted Cache Hit reduces the upper bound by the cache-miss penalty.,load a,a, b,Computed,cache information,Access to,a,is a cache hit;,assume 1 cycle access time.,x,Cache Analysis how does it work?,How to compute for each program point an,abstract cache state,representing a set of memory blocks guaranteed to be in cache each time execution reaches this program point?,Can we expect to compute the,largest set,?,Trade-off between precision and efficiency, quite typical for abstract interpretation,(Must) Cache analysis of a memory access,a, b,x,access to,a,b, x,a,After the access to,a,a,is the youngest memory block in cache,and we must assume that,x,has aged.,What about b?,b,a,access to,a,b,a,x,y,y,x,concrete,transfer,function,(cache),abstract,transfer,function,(analysis),Combining Cache Information,Consider two control-flow paths to a program point:,for one, prediction says, set of memory blocks S1 in cache,for the other, the set of memory blocks S2.,Cache analysis should not predict more than S1, S2 after the merge of paths.,the elements in the intersection should have their maximal age from S1 and S2.,Suggests the following method: Compute cache information along all paths to a program point and calculate their intersection but too many paths!,More efficient method:,combine cache information on the way,iterate until least fixpoint is reached.,There is a risk of losing precision, not in case of distributive transfer functions,.,What happens when control-paths merge?, a , , c, f , d , c , e , a , d , , , a, c , d ,“,intersection,+ maximal age,”,We can,guarantee,this content,on this path,.,We can,guarantee,this content,on this path,.,Which content,can we,guarantee,on this path?,combine cache information at each control-flow merge point,Must-Cache and May-Cache- Information,The presented cache analysis is a,Must Analysis.,It determines safe information about,cache hits,.,Each predicted cache hit reduces,the upper bound.,We can also perform a,May Analysis.,It determines safe information about,cache misses,Each predicted cache miss increases,the lower bound.,(May) Cache analysis of a memory access,a, b,x,access to,a,x,a,Why?,After the access to,a,a,is the youngest memory block in cache,and we must assume that,x, y,and,b,have aged.,b, z,y,z,y,Cache Analysis: Join (may), a , , c, f , d , c , e , a , d , a,c , e, f , d ,“,union,+ minimal age,”,Join (may),Abstract Domain: Must Cache,z,s,x,a,x,s,z,t,z,s,x,t,s,z,x,t,z,t,x,s,Abstraction,Representing sets of concrete caches by their description,concrete caches, , ,z,x,s,abstract cache,Abstract Domain: Must Cache, , ,z,x,s,Concretization,s,z, x,Sets of concrete caches described by an abstract cache,remaining line filled up,with any other block,concrete caches,abstract cache,over-approximation!,Abstract Domain: May Cache,z,s,x,a,x,s,z,t,z,s,x,t,s,z,x,t,z,t,x,s,z ,s, x,t, , a ,Abstraction,abstract cache,concrete caches,Abstract Domain: May Cache,Concretization,z,s,x, t , , a ,abstract may-caches say,what definitely is not in cache,and what the minimal age of,those is that may be in cache.,z,s,x,z,s,x,t,z,s,x,t,z,s,x,t,a,concrete caches,abstract cache,Lessons Learned,Cache analysis, an important ingredient of static timing analysis, provides for abstract domains,which proved to be,sufficiently precise,have,compact representation,have,efficient transfer functions,which are,quite natural,.,Problem Solved?,We have shown a solution for LRU caches.,LRU-cache analysis works smoothly,Favorable structure,“,of domain,Essential information can be summarized compactly,LRU is the best strategy under several aspects,performance, predictability, sensitivity, and yet: LRU is not the only strategy,Pseudo-LRU (PowerPC 755 Airbus),FIFO,worse under almost all aspects, but average-case performance!,Contribution to WCET,while . . . do,max,n,.,.,.,ref to s,.,.,.,od,time,t,miss,t,hit,loop time,n,t,miss,n,t,hit,t,miss,(,n,1),t,hit,t,hit,(,n,1),t,miss,Contexts,Cache contents depends on the,Context,i.e. calls and loops,while,cond,do,join (must),First Iteration loads the cache,=,Intersection loses most of the information,!,Distinguish basic blocks by contexts,Transform loops into tail recursive procedures,Treat loops and procedures in the same way,Use interprocedural analysis techniques,VIVU,virtual inlining of procedures,virtual unrolling of loops,Distinguish as many contexts as useful,1 unrolling for caches,1 unrolling for branch prediction (pipeline),Structure of the Lectures,Introduction,Static timing analysis,the problem,our approach,the success,tool architecture,Cache analysis,Pipeline analysis,Value analysis,Worst-case path analysis,-,Timing Predictability,caches,non-cache-like devices,future architectures,Conclusion,Tool Architecture,Abstract Interpretations,Abstract Interpretation,Integer Linear,Programming,Pipelines,Hardware Features: Pipelines,Ideal Case: 1 Instruction per Cycle,Fetch,
展开阅读全文
相关资源
正为您匹配相似的精品文档
相关搜索

最新文档


当前位置:首页 > 商业管理 > 商业计划


copyright@ 2023-2025  zhuangpeitu.com 装配图网版权所有   联系电话:18123376007

备案号:ICP2024067431-1 川公网安备51140202000466号


本站为文档C2C交易模式,即用户上传的文档直接被用户下载,本站只是中间服务平台,本站所有文档下载所得的收益归上传人(含作者)所有。装配图网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私,请立即通知装配图网,我们立即给予删除!