Abstract
Abstract interpretation is successfully used for determining execution-time bounds of real-time programs. The particular problem it solves is the determination of invariants at all program points that describe the set of all execution states that are possible at these program points. These invariants are then used to exclude some of the possible costly executions of instructions, thereby reducing the execution-time bounds. This article considers the properties of this application of abstract interpretation that differ from those in the standard applications of abstract interpretation in compilation and in verification. It also shows how some particular designs of the underlying abstract domains made efficient timing analysis possible.
Work reported herein was supported by the Deutsche Forschungsgemeinschaft in the Transregional Research Center AVACS, Automatic Verification and Analysis of Complex Systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In interval analysis for example a set of values is abstracted by its least and their greatest element.
References
Abel, A.: Impact of resource sharing on performance and performance prediction: a survey. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 25–43. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-40184-8_3
Abel, A., Reineke, J.: Measurement-based modeling of the cache replacement policy. In: RTAS, April 2013. http://embedded.cs.uni-saarland.de/publications/CacheModelingRTAS2013.pdf
Alt, M., Ferdinand, C., Martin, F., Wilhelm, R.: Cache behavior prediction by abstract interpretation. In: Static Analysis, Third International Symposium, SAS 1996, pp. 52–66 (1996). http://dx.doi.org/10.1007/3-540-61739-6_33
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282. ACM Press (1979). http://doi.acm.org/10.1145/567752.567778
Cullmann, C.: Cache persistence analysis: theory and practice. ACM Trans. Embed. Comput. Syst. 12(1s), 40:1–40:25 (2013)
Cullmann, C., Martin, F.: Data-flow based detection of loop bounds. In: Rochange, C. (ed.) 7th International Workshop on Worst-Case Execution Time Analysis (WCET 2007), Dagstuhl, Germany (2007). http://drops.dagstuhl.de/opus/volltexte/2007/1193
Engblom, J.: Processor Pipelines and Static Worst-Case Execution Time Analysis. Ph.D. thesis, Uppsala University, Sweden (2002). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.5355
Ermedahl, A., Gustafsson, J.: Deriving annotations for tight calculation of execution time. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds.) Euro-Par 1997. LNCS, vol. 1300. Springer, Heidelberg (1997)
Ferdinand, C.: Cache Behavior Prediction for Real-Time Systems. Ph.D. thesis, Saarland University, Saarbruecken, Germany (1997). ISBN: 3-9307140-31-0
Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469–485. Springer, Heidelberg (2001)
Ferdinand, C., Wilhelm, R.: Efficient and precise cache behavior prediction for real-time systems. Real-Time Syst. 17(2–3), 131–181 (1999)
Grund, D., Reineke, J.: Abstract interpretation of FIFO replacement. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 120–136. Springer, Heidelberg (2009)
Grund, D., Reineke, J.: Precise and efficient FIFO-replacement analysis based on static phase detection. In: Proceedings of the 22nd Euromicro Conference on Real-Time Systems (ECRTS), pp. 155–164, July 2010
Grund, D., Reineke, J.: Toward precise PLRU cache analysis. In: Lisper, B. (ed.) 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010), pp. 23–35 (2010). http://drops.dagstuhl.de/opus/volltexte/2010/2822
Guan, N., Lv, M., Yi, W., Yu, G.: WCET analysis with MRU cache: challenging LRU for predictability. ACM Trans. Embed. Comput. Syst. 13(4s), 123:1–123:26 (2014). http://doi.acm.org/10.1145/2584655
Guan, N., Yang, X., Lv, M., Yi, W.: FIFO cache analysis for WCET estimation: a quantitative approach. In: Proceedings of Design, Automation Test in Europe Conference Exhibition (DATE), 2013, pp. 296–301, March 2013
Hahn, S., Reineke, J., Wilhelm, R.: Toward compact abstractions for processor pipelines. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 205–220. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-319-23506-6_14
Healy, C., Sjödin, M., Rustagi, V., Whalle, D., van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Syst. 18(2), 129–156 (2000)
Li, Y.T.S., Malik, S.: Performance analysis of embedded software using implicit path enumeration. In: Proceedings of the 32nd ACM/IEEE Design Automation Conference, pp. 456–461 (1995)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005). http://dx.doi.org/10.1007/978-3-540-31987-0_2
Reineke, J., Grund, D.: Relative competitive analysis of cache replacement policies. In: Proceedings of the 2008 ACM SIGPLAN-SIGBED Conference On Languages, Compilers, And Tools For Embedded Systems, LCTES 2008, pp. 51–60. ACM, June 2008. http://rw4.cs.uni-saarland.de/grund/papers/lctes08-rel_comp.pdf
Reineke, J., Grund, D., Berg, C., Wilhelm, R.: Timing predictability of cache replacement policies. Real Time Syst. 37(2), 99–122 (2007)
Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002). http://doi.acm.org/10.1145/514188.514190
Schlickling, M., Pister, M.: Semi-automatic derivation of timing models for WCET analysis. In: Proceedings of the ACM SIGPLAN/SIGBED 2010 Conference on Languages, Compilers, and Tools For Embedded Systems, pp. 67–76. ACM, April 2010
Seidl, H., Wilhelm, R., Hack, S.: Compiler Design - Analysis and Transformation. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-17548-0
Stein, I., Martin, F.: Analysis of path exclusion at the machine code level. In: Rochange, C. (ed.) 7th International Workshop on Worst-Case Execution Time Analysis (WCET 2007). OpenAccess Series in Informatics (OASIcs), Dagstuhl, Germany (2007). http://drops.dagstuhl.de/opus/volltexte/2007/1196
Theiling, H.: ILP-based interprocedural path analysis. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 349–363. Springer, Heidelberg (2002)
Thesing, S.: Safe and Precise WCET Determinations by Abstract Interpretation of Pipeline Models. Ph.D. thesis, Saarland University, Saarbrücken, Germany (2004). http://scidok.sulb.uni-saarland.de/volltexte/2005/466/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Reineke, J., Wilhelm, R. (2016). Static Timing Analysis – What is Special?. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-27810-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27809-4
Online ISBN: 978-3-319-27810-0
eBook Packages: Computer ScienceComputer Science (R0)