Abstract
Hard real-time systems require programs to react on time. Static timing analysis derives timing guarantees by analyzing the behavior of programs running on the underlying execution platform. Efficient abstractions have been found for the analysis of caches. Unfortunately, this is not the case for the analysis of processor pipelines. Pipeline analysis typically uses an expensive powerset domain of concrete pipeline states. Therefore, pipeline analysis is the most complex part of timing analysis. We propose a compact abstract domain for pipeline analysis. This pipeline analysis determines the minimal progress of instructions in the program through the pipeline.
We give a concrete semantics for an in-order pipeline, which forms the basis for an abstract semantics. On the way, we found out that in-order pipelines are not guaranteed to be free of timing anomalies, i.e. local worst decisions do not lead to the global worst case. We prove this by giving an example. A major problem is how to find an abstract semantics that guarantees progress on the abstract side. It turns out that monotonicity on the partial progress order is sufficient to guarantee this.
This work was supported by the Deutsche Forschungsgemeinschaft (DFG) as part of the Transregional Collaborative Research Centre SFB/TR 14 (AVACS) and by the Saarbrücken Graduate School of Computer Science which receives funding from the DFG as part of the Excellence Initiative of the German Federal and State Governments.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Ferdinand, C., Wilhelm, R.: Efficient and precise cache behavior prediction for real-time systems. Real-Time Systems 17(2–3), 131–181 (1999)
Gebhard, G.: Timing anomalies reloaded. In: Lisper, B. (ed.) 10th International Workshop on Worst-Case Execution Time Analysis, WCET. OASICS, vol. 15, pp. 1–10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany (2010)
Langenbach, M., Thesing, S., Heckmann, R.: Pipeline modeling for timing analysis. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 294–309. Springer, Heidelberg (2002)
Liu, I., Reineke, J., Lee, E.A.: A PRET architecture supporting concurrent programs with composable timing properties. In: Conference Record of the Forty Fourth Asilomar Conference on Signals, Systems and Computers, pp. 2111–2115. IEEE (2010)
Reineke, J., Wachter, B., Thesing, S., Wilhelm, R., Polian, I., Eisinger, J., Becker, B.: A definition and classification of timing anomalies. In: Mueller, F. (ed.) 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. OASICS, vol. 4. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)
Rochange, C., Sainrat, P.: A time-predictable execution mode for superscalar pipelines with instruction prescheduling. In: Bagherzadeh, N., Valero, M., Ramírez, A. (eds.) Proceedings of the Second Conference on Computing Frontiers, pp. 307–314. ACM (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1999, pp. 105–118. ACM, New York (1999)
Thesing, S.: Safe and precise WCET determination by abstract interpretation of pipeline models. Ph.D. thesis, Saarland University (2005)
Wenzel, I., Kirner, R., Puschner, P., Rieder, B.: Principles of timing anomalies in superscalar processors. In: Fifth International Conference on Quality Software (QSIC 2005). IEEE (2005)
Wilhelm, S.: Efficient analysis of pipeline models for WCET computation. In: Wilhelm, R. (ed.) 5th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. OASICS, vol. 1. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Hahn, S., Reineke, J., Wilhelm, R. (2015). Toward Compact Abstractions for Processor Pipelines. In: Meyer, R., Platzer, A., Wehrheim, H. (eds) Correct System Design. Lecture Notes in Computer Science(), vol 9360. Springer, Cham. https://doi.org/10.1007/978-3-319-23506-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-23506-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23505-9
Online ISBN: 978-3-319-23506-6
eBook Packages: Computer ScienceComputer Science (R0)