基于抽象解释的嵌入式软件模块化Cache行为分析框架  

Abstract-Interpretation-Based Framework of Modular Cache Behavior Analysis for Embedded Software

作　　者：喻垚慎 黄志球[1,2,3] 沈国华 王飞[1] 崔少轩 YU Yao-Shen;HUANG Zhi-Qiu;SHEN Guo-Hua;WANG Fei;CUI Shao-Xuan(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106;Key Laboratory of Safety-Critical Software(Nanjing University of Aeronautics and Astronautics),Ministry of Industry and Information Technology,Nanjing 211106;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 210093)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学),南京211106 [3]软件新技术与产业化协同创新中心,南京210093

出　　处：《计算机学报》2019年第10期2251-2266,共16页Chinese Journal of Computers

基　　金：国家“八六三”高技术研究发展计划基金项目（2015AA105303）;国家重点研发计划（2016YFB1000802）;国家自然科学基金（61502231）资助~~

摘　　要：程序最坏执行时间(Worst Case Execution Time,WCET)是嵌入式实时系统时间属性验证的基础,在采用静态分析技术的WCET估算中需要分阶段对不同的执行环境约束条件进行分析,并整合所有约束信息、结合程序控制流结构估算全局最坏路径,因此各阶段分析的中间结果对最终的WCET估算性能具有较大影响.在现代嵌入式系统中,硬件平台中的Cache机制成为对执行时间影响较大的硬件体系结构,对其进行精确的行为分析在WCET估算中具有重要的现实意义.采用抽象解释理论对Cache行为进行分析已有较为成熟的技术成果和相关工具,但由于静态分析技术具有较难理解和使用的特点,对于技术没有覆盖、工具没有支持的硬件架构,针对这类硬件架构进行相关研究和验证工具开发都具有较大难度和挑战.该文以抽象解释为理论基础,以复用Cache分析过程为目标,提出了基于抽象解释的模块化Cache行为分析框架,对Cache行为分析过程进行了层次划分,提出了易于复用的Cache行为分析方法设计,能够针对不同架构的Cache机制分析方法进行建模,并以统一的分析框架对分析过程进行复用.案例实验表明,该框架可支持采用抽象解释对使用LRU策略的Cache行为进行建模分析,并能够得到Cache命中情况标记信息以支持后续WCET的估算过程.The Worst-Case Execution Time(WCET)estimation is the basis of timing validation for embedded real-time system.In WCET estimation research which use static analysis techniques,it will separate into different stages for different execution environments like cache and pipeline to analyze the constraints which will affect the execution time of the program.Then it integrates all these constraints from different analysis stages and combines them with the control flow structure of the program to explore the global worst-case execution path and calculate the worst-case execution time based on the worst-case path.Therefore,the intermediate results of each stage analysis such as cache behavior analysis,have a great influence on the performance of final WCET estimation.In modern embedded system,the cache mechanism in the processor is an execution environment that affects the execution time very prominently.So,it has a practical significance for an accurate and safe cache behavior analysis in WCET estimation process which will be applied in embedded system especially in safety-critical system.Using abstract interpretation to analyze cache behavior is a very mature technology and there are some related tools for industrial WCET estimation like aiT,OTAWA and so on.However,because static analysis is difficult to understand and use,if there exist any hardware architecture which will not supported by existing analysis techniques or verification tools,it is very difficult to study the analysis method and develop related tool to deal with these architectures.In this paper,it takes the abstract interpretation as the theoretical basis and takes the reuse of the cache behavior analysis process as the goal,proposes an abstract-interpretation-based framework for modular cache behavior analysis.This framework divides the cache behavior analysis process hierarchically,formalize the design method of the cache behavior analysis which is easily reusable.The design can be used to model the cache analysis methods for different architectures an

关 键 词：嵌入式软件 Cache行为分析 静态代码分析 模块化分析 抽象解释 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]