Article

Static timing analysis for hard real-time systems

Authors:

Reinhard Wilhelm,

Sebastian Altmeyer,

Claire Burguière,

Björn Wachter,

Stephan WilhelmAuthors Info & Claims

VMCAI'10: Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation

Pages 3 - 22

https://doi.org/10.1007/978-3-642-11319-2_3

Published: 17 January 2010 Publication History

Abstract

Hard real-time systems have to satisfy strict timing constraints. To prove that these constraints are met, timing analyses aim to derive safe upper bounds on tasks’ execution times. Processor components such as caches, out-of-order pipelines, and speculation cause a large variation of the execution time of instructions, which may induce a large variability of a task’s execution time. The architectural platform also determines the precision and the complexity of timing analysis.

This paper provides an overview of our timing-analysis technique and in particular the methodological aspects of interest to the verification community.

References

[1]

Wilhelm, R., et al.: The worst-case execution-time problem--overview of methods and survey of tools. Trans. on Embedded Computing Sys. 7(3), 1-53 (2008).

Digital Library

[2]

Petters, S.M.: Worst-Case Execution-Time Estimation for Advanced Processor Architectures. PhD thesis, Technische Universität München, Munich, Germany (2002).

[3]

Bernat, G., Colin, A., Petters, S.M.: WCET analysis of probabilistic hard realtime systems. In: Proceedings of the 23rd IEEE Real-Time Systems Symposium, Washington, DC, USA, p. 279. IEEE Computer Society, Los Alamitos (2002).

Digital Library

[4]

Wenzel, I.: Measurement-Based Timing Analysis of Superscalar Processors. PhD thesis, Technische Universität Wien, Vienna, Austria (2006).

[5]

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).

Digital Library

[6]

Thiele, L., Wilhelm, R.: Design for timing predictability. Real-Time Sys. 28, 157- 177 (2004).

Digital Library

[7]

Wilhelm, R., Grund, D., Reineke, J., Schlickling, M., Pister, M., Ferdinand, C.: Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Transactions on CAD of Integrated Circuits and Systems 28(7), 966-978 (2009).

Digital Library

[8]

Reineke, J., Grund, D., Berg, C., Wilhelm, R.: Timing predictability of cache replacement policies. Real-Time Sys. 37(2), 99-122 (2007).

Digital Library

[9]

Reineke, J.: Caches in WCET Analysis. PhD thesis, Saarland University, Saarbrücken, Germany (2008).

[10]

Wilhelm, S., Wachter, B.: Symbolic state traversal for WCET analysis. In: International Conference on Embedded Software, pp. 137-146 (2009).

Digital Library

[11]

Wilhelm, R.: Determining bounds on execution times. In: Zurawski, R. (ed.) Handbook on Embedded Systems, pp. 14-23. CRC Press, Boca Raton (2005).

[12]

Reineke, J., Wachter, B., Thesing, S., Wilhelm, R., Polian, I., Eisinger, J., Becker, B.: A definition and classification of timing anomalies. In: Proceedings of 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis (2006).

[13]

Heckmann, R., Langenbach, M., Thesing, S., Wilhelm, R.: The influence of processor architecture on the design and the results ofWCET tools. Real-Time Sys. 91(7), 1038-1054 (2003).

[14]

Theiling, H.: Control-Flow Graphs For Real-Time Systems Analysis. PhD thesis, Saarland University, Saarbrücken, Germany (2002).

[15]

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).

Digital Library

[16]

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, pp. 1298-1307. Springer, Heidelberg (1997).

Digital Library

[17]

Healy, C., Sjödin, M., Rustagi, V., Whalley, D., van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Sys., 129-156 (2000).

Digital Library

[18]

Stein, I., Martin, F.: Analysis of path exclusion at the machine code level. In: Proceedings of the 7th Intl. Workshop on Worst-Case Execution-Time Analysis (2007).

[19]

Engblom, J.: Processor Pipelines and Static Worst-Case Execution Time Analysis. PhD thesis, Dept. of Information Technology, Uppsala University (2002).

[20]

Thesing, S.: Safe and Precise WCET Determinations by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University, Saarbrücken, Germany (2004).

[21]

Ferdinand, C., Wilhelm, R.: Efficient and precise cache behavior prediction for real-time systems. Real-Time Sys. 17(2-3), 131-181 (1999).

Digital Library

[22]

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).

Digital Library

[23]

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).

Digital Library

[24]

Thesing, S., Souyris, J., Heckmann, R., Randimbivololona, F., Langenbach, M., Wilhelm, R., Ferdinand, C.: An abstract interpretation-based timing validation of hard real-time avionics software systems. In: Proceedings of the 2003 Intl. Conference on Dependable Systems and Networks, pp. 625-632. IEEE Computer Society, Los Alamitos (2003).

[25]

Berg, C.: PLRU cache domino effects. In: Mueller, F. (ed.) 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2006).

[26]

Altmeyer, S., Burguière, C.: A new notion of useful cache block to improve the bounds of cache-related preemption delay. In: Proceedings of the 21st Euromicro Conference on Real-Time Systems, pp. 109-118. IEEE Computer Society Press, Los Alamitos (2009).

Digital Library

[27]

White, R.T., Healy, C.A., Whalley, D.B., Mueller, F., Harmon, M.G.: Timing analysis for data caches and set-associative caches. In: Proceedings of the 3rd IEEE Real-Time Technology and Applications Symposium, Washington, DC, USA, p. 192. IEEE Computer Society, Los Alamitos (1997).

Digital Library

[28]

Ghosh, S., Martonosi, M., Malik, S.: Precise miss analysis for program transformations with caches of arbitrary associativity. In: Proceedings of the 8th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 228-239 (1998).

Digital Library

[29]

Chatterjee, S., Parker, E., Hanlon, P.J., Lebeck, A.R.: Exact analysis of the cache behavior of nested loops. In: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 286-297. ACM Press, New York (2001).

Digital Library

[30]

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, pp. 51-60. ACM, New York (2008).

Digital Library

[31]

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).

Digital Library

[32]

Herter, J., Reineke, J.: Making dynamic memory allocation static to support WCET analyses. In: Proceedings of 9th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis (2009).

[33]

Herter, J., Reineke, J., Wilhelm, R.: CAMA: Cache-aware memory allocation for WCET analysis. In: Caccamo, M. (ed.) Proceedings Work-In-Progress Session of the 20th Euromicro Conference on Real-Time Systems, pp. 24-27 (2008).

[34]

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Programming Languages and Sys. 24(3), 217-298 (2002).

Digital Library

[35]

Bryant, R.: Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers (1986).

Digital Library

[36]

Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, J.: Symbolic model checking: 10²⁰ states and beyond. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science. IEEE Comp. Soc. Press, Los Alamitos (1990).

[37]

Ranjan, R., Aziz, A., Brayton, R., Plessier, B., Pixley, C.: Efficient BDD Algorithms for FSM Synthesis and Verification. In: Proceedings of IEEE/ACM International Workshop on Logic Synthesis, Lake Tahoe, USA (1995).

Cited By

Guo SChen YYu JWu MZuo ZLi PCheng YWang H(2020)Exposing cache timing side-channel leaks through out-of-order symbolic executionProceedings of the ACM on Programming Languages10.1145/34282154:OOPSLA(1-32)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428215
(2019)Impact of software architecture on execution timeInternational Journal of Grid and Utility Computing10.5555/3319245.331924910:2(132-140)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.5555/3319245.3319249
Wu MWang CMcKinley KFisher K(2019)Abstract interpretation under speculative executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314647(802-815)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314647
Show More Cited By

Recommendations

Hardware support for WCET analysis of hard real-time multicore systems
ISCA '09: Proceedings of the 36th annual international symposium on Computer architecture

The increasing demand for new functionalities in current and future hard real-time embedded systems like automotive, avionics and space industries is driving an increase in the performance required in embedded processors. Multicore processors represent ...
Hardware support for WCET analysis of hard real-time multicore systems

The increasing demand for new functionalities in current and future hard real-time embedded systems like automotive, avionics and space industries is driving an increase in the performance required in embedded processors. Multicore processors represent ...
A Survey of WCET Analysis of Real-Time Operating Systems
ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems

Timing correctness of hard real-time systems is guaranteed by schedulability analysis and worst-case execution time (WCET) analysis of programs. Traditional WCET analysis mainly deals with application programs and has achieved success in industry. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

VMCAI'10: Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation

January 2010

396 pages

ISBN:3642113184

Editors:
Gilles Barthe
Facultad de Informatica (UPM), IMDEA Software, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain
,
Manuel Hermenegildo
Facultad de Informatica (UPM), IMDEA Software and Technical University of Madrid, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

Sponsors

EAPLS: European Assoc for Programming Languages and Systems
IMDEA Software: IMDEA Software
ACM: Association for Computing Machinery

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 January 2010

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Guo SChen YYu JWu MZuo ZLi PCheng YWang H(2020)Exposing cache timing side-channel leaks through out-of-order symbolic executionProceedings of the ACM on Programming Languages10.1145/34282154:OOPSLA(1-32)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428215
(2019)Impact of software architecture on execution timeInternational Journal of Grid and Utility Computing10.5555/3319245.331924910:2(132-140)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.5555/3319245.3319249
Wu MWang CMcKinley KFisher K(2019)Abstract interpretation under speculative executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314647(802-815)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314647
Hamad MHammadeh ZSaidi SPrevelakis VErnst RHaddad HWainwright RChbeir R(2018)Prediction of abnormal temporal behavior in real-time systemsProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167172(359-367)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167172
Nagar KSrikant Y(2016)Fast and Precise Worst-Case Interference Placement for Shared Cache AnalysisACM Transactions on Embedded Computing Systems10.1145/285415115:3(1-26)Online publication date: 7-Mar-2016
https://dl.acm.org/doi/10.1145/2854151
Cerny PHenzinger TRadhakrishna A(2013)Quantitative abstraction refinementACM SIGPLAN Notices10.1145/2480359.242908548:1(115-128)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429085
Cerny PHenzinger TRadhakrishna AGiacobazzi RCousot R(2013)Quantitative abstraction refinementProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429085(115-128)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429085
Autili MDi Benedetto PInverardi P(2013)A hybrid approach for resource-based comparison of adaptable Java applicationsScience of Computer Programming10.1016/j.scico.2012.01.00578:8(987-1009)Online publication date: 1-Aug-2013
https://dl.acm.org/doi/10.1016/j.scico.2012.01.005
Triki ACombaz JBensalem SSifakis J(2013)Model-Based implementation of parallel real-time systemsProceedings of the 16th international conference on Fundamental Approaches to Software Engineering10.1007/978-3-642-37057-1_18(235-249)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37057-1_18
Černý PHenzinger TChakraborty SJerraya ABaruah SFischmeister S(2011)From boolean to quantitative synthesisProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038666(149-154)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038666
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents