ABSTRACT
Static worst-case execution time analysis of real-time tasks is based on abstract models that capture the timing behavior of the processor on which the tasks run. For complex processors, task-level execution time bounds are obtained by a state exploration which involves the abstract model and the program. Partial state space exploration is not sound. A full exploration can become too expensive. We present a novel symbolic method for WCET analysis based on abstract pipeline models which produces sound results and is scalable in terms of the considered hardware states.
- AbsInt. aiT WCET Analyzers. http://www.absint.com/ait, 2000.Google Scholar
- C. Berg. PLRU cache domino effects. In 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. Schloss Dagstuhl, Germany, 2006.Google Scholar
- M. Berndl, O. Lhotak, F. Qian, L. J. Hendren, and N. Umanee. Points-to analysis using BDDs. In PLDI, pages 103--114, 2003. Google ScholarDigital Library
- A. Betts, G. Bernat, R. Kirner, P. Puschner, and I. Wenzel. WCET Coverage for Pipelines. Technical report, 2006.Google Scholar
- D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. STTT, 9(5-6):505--525, 2007. Google ScholarCross Ref
- R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. A. Edwards, S. P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A System for Verification and Synthesis. In CAV, pages 428--432, 1996. Google ScholarDigital Library
- R. Bryant. Graph based algorithms for boolean function manipulation. In IEEE Transactions on Computers, 1986. Google ScholarDigital Library
- J. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. IEEE Comp. Soc. Press, 1990.Google Scholar
- S.-T. Cheng. Compiling Verilog into Automata. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1994.Google Scholar
- E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ Cache Coherence Protocol. In CHDL, pages 15--30, 1993. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, 1977. Google ScholarDigital Library
- EDN. DSP Benchmarks. In EDN - Electronic Design, Strategy, News, Sept. 1988.Google Scholar
- J. Engblom. Processor Pipelines and Static Worst-Case Execution Time Analysis. PhD thesis, Uppsala University, 2002.Google Scholar
- C. Ferdinand. Cache Behavior Prediction for Real-Time Systems. PhD thesis, Saarland University, 1997.Google Scholar
- C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling, S. Thesing, and R. Wilhelm. Reliable and Precise WCET Determination for a Real-Life Processor. In Proceedings of EMSOFT 2001, LNCS 2211, 2001. Google ScholarDigital Library
- M. Fujita, Y. Matsunaga, and T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In Proceedings of the conference on European design automation, 1991. Google ScholarDigital Library
- R. Heckmann, M. Langenbach, S. Thesing, and R. Wilhelm. The influence of processor architecture on the design and the results of WCET tools. Proceedings of the IEEE, 91(7), 2003.Google ScholarCross Ref
- N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. In ICCAD, pages 472--475, 1991.Google ScholarCross Ref
- R. Jhala and K. L. McMillan. Microarchitecture Verification by Compositional Model Checking. In CAV, pages 396--410, 2001. Google ScholarDigital Library
- D. Kastner, R. Wilhelm, R. Heckmann, M. Schlickling, M. Pister, M. Jersak, K. Richter, and C. Ferdinand. Timing Validation of Automotive Software. In 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) 2008, Communications in Computer and Information Science (CCIS). Springer, 2008.Google Scholar
- Y.-T. S. Li and S. Malik. Performance analysis of embedded software using implicit path enumeration. In DAC, pages 456--461, 1995. Google ScholarDigital Library
- G. Logothetis and K. Schneider. Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration. In DATE, pages 10196--10203, 2003. Google ScholarDigital Library
- T. Lundquist and P. Stenstrom. Timing Anomalies in Dynamically Scheduled Microprocessors. In Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999. Google ScholarDigital Library
- F. Martin. PAG - An Efficient Program Analyzer Generator. STTT, 2(1), 1998.Google Scholar
- F. Martin, M. Alt, R. Wilhelm, and C. Ferdinand. Analysis of Loops. In K. Koskimies, editor, Proceedings of the 7th International Conference on Compiler Construction, LNCS 1383, pages 80--94, Berlin, 1998. Springer. Google ScholarDigital Library
- A. Metzner. Why Model Checking Can Improve WCET Analysis. In CAV, 2004.Google Scholar
- R. Ranjan, A. Aziz, R. Brayton, B. Plessier, and C. Pixley. Efficient BDD Algorithms for FSM Synthesis and Verification, 1995.Google Scholar
- J. Reineke. Caches in WCET Analysis. PhD thesis, Saarland University, 2008.Google Scholar
- R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In ICCAD '93: Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, pages 42--47. IEEE Computer Society Press, 1993. Google ScholarDigital Library
- J. Schneider. Combined Schedulability and WCET Analysis for Real-Time Operating Systems. PhD thesis, Saarland University, 2003.Google Scholar
- J. Souyris, E. Le Pavec, G. Himbert, V. Jacgu, G. Borios, and R. Heckmann. Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation. In Proceedings of the 5th Intl Workshop on (WCET) Analysis, 2005.Google Scholar
- L. Tan. The Worst-case Execution Time Tool Challenge 2006. International Journal on Software Tools for Technology Transfer (STTT), 11(2):133 -- 152, 2009.Google Scholar
- H. Theiling. ILP-based Interprocedural Path Analysis. In Proceedings of the Workshop on Embedded Software, Grenoble, France, 2002. Google ScholarDigital Library
- H. Theiling. Control Flow Graphs for Real-Time System Analysis. PhD thesis, Saarland University, 2003.Google Scholar
- S. Thesing. Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University, 2004.Google Scholar
- S. Thesing, J. Souyris, R. Heckmann, F. Randimbivololona, M. Langenbach, R. Wilhelm, and C. Ferdinand. An Abstract Interpretation-Based Timing Validation of Hard Real-Time Avionics Software. In Proceedings of the International Conference on Dependable Systems and Networks. IEEE Computer Society, 2003.Google ScholarCross Ref
- R. Weicker. Dhrystone benchmark: rationale for version 2 and measurement rules. SIGPLAN Notices, 23(8):49--62, 1988. Google ScholarDigital Library
- R. Wilhelm. Why AI + ILP is good for WCET, but MC is not, nor ILP alone. In In Verification, Model Checking and Abstract Interpretation (VMCAI), LNCS 2937, 2004.Google Scholar
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstrom. The Determination of Worst-Case Execution Times--Overview of the Methods and Survey of Tools. 7(3), 2008. ACM Transactions on Embedded Computing Systems (TECS). Google ScholarDigital Library
Index Terms
- Symbolic state traversal for WCET analysis
Recommendations
WCET analysis for a Java processor
JTRES '06: Proceedings of the 4th international workshop on Java technologies for real-time and embedded systemsIn this paper we propose a solution for a worst-case execution time (WCET) analyzable Java system: a combination of a time predictable Java processor and a tool that performs WCET analysis of Java bytecode. We present a Java processor, called JOP, ...
Semi-automatic derivation of timing models for WCET analysis
LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systemsEmbedded systems are widely used for supporting our every day life. In the area of safety-critical systems human life often depends on the system's correct behavior. Many of such systems are hard real-time systems, so that the notion of correctness not ...
WCET-aware hyper-block construction for clustered VLIW processors
LCTES 2019: Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded SystemsHyper-blocks can significantly improve instruction level parallelism on a wide range of super-scalar and VLIW processors. However, most hyper-block construction approaches aim at minimizing the average-case execution time of a program. In real-time ...
Comments