Abstract
In this paper, we investigate the case for model checking in the WCET analysis of pipelined processors with dynamic branch and target prediction. We consider a microarchitecture inspired by the e200z4 Power 32-bit architecture, with an instruction cache, a dynamic branch prediction mechanism, a branch target buffer (BTB) and an instruction prefetch buffer. The conjoint operation of all these components produce a very complex behaviour that is difficult to analyse with tight and sound static analysis techniques. We show that model checking techniques can actually be used to compute WCET bounds for this kind of architectures.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Metzner use dynamic analysis to designate techniques that analyze concrete paths in the system, as opposed to static analysis that consider abstract paths.
- 2.
The main difference is that the e200z4 is actually a two issues statically scheduled superscalar processor, whereas we consider a single issue processor.
- 3.
A bubble, or pipeline stall, is a delay cycle. When a bubble enters a stage, this stage has no activity during the current cycle.
- 4.
The Advanced High-performance Bus is part of the open standard ARM-AMBA on-chip interconnect specification.
- 5.
In the case where the instruction in the decode stage requires a result produced by an instruction ahead in the pipeline, bubbles are inserted until the availability of the result. This is a data hazard. Bypasses are used between stages to propagate results and limits these bubbles.
- 6.
Available at https://github.com/TrampolineRTOS/BEST.
References
Bate, I., Reutemann, R.D.: Worst-case execution time analysis for dynamic branch predictors. In: 16th Euromicro Conference on Real-Time Systems, ECRTS, pp. 215–222 (2004)
Cassez, F., Béchennec, J.: Timing analysis of binary programs with UPPAAL. In: 13th International Conference on Application of Concurrency to System Design, ACSD, pp. 41–50 (2013)
Colin, A., Puaut, I.: Worst case execution time analysis for a processor with branch prediction. Real-Time Syst. 18(2/3), 249–274 (2000)
Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: METAMOC: modular execution time analysis using model checking. In: 10th International Workshop on Worst-Case Execution Time Analysis, WCET, pp. 113–123 (2010)
Engblom, J.: Analysis of the execution time unpredictability caused by dynamic branch prediction. In: 9th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, pp. 152–159 (2003)
Freescale semiconductors/NXP: e200z4 Power ArchitectureTM Core Reference Manual, rev. 0 edn., October 2009
Freescale semiconductors/NXP: MPC5643L Microcontroller Reference Manual, rev, 10 edn., June 2013
Grund, D., Reineke, J., Gebhard, G.: Branch target buffers: WCET analysis framework and timing predictability. J. Syst. Architect. 57(6), 625–637 (2011)
Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The Mälardalen WCET benchmarks - past, present and future. In: International Workshop on Worst-Case Execution Time Analysis (WCET) (2010)
Gustavsson, A., Ermedahl, A., Lisper, B., Pettersson, P.: Towards WCET analysis of multicore architectures using UPPAAL. In: 10th International Workshop on Worst-Case Execution Time Analysis, WCET, pp. 101–112 (2010)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997)
Maiza, C., Rochange, C.: A framework for the timing analysis of dynamic branch predictors. In: 19th International Conference on Real-Time and Network Systems, RTNS, pp. 65–74 (2011)
Mangean, A., Béchennec, J.L., Briday, M., Faucou, S.: BEST: a binary executable slicing tool. In: 16th International Workshop on Worst-Case Execution Time Analysis, WCET, pp. 7:1–7:10 (2016)
Metzner, A.: Why model checking can improve WCET analysis. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 334–347. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_26
Puffitsch, W.: Efficient worst-case execution time analysis of dynamic branch prediction. In: 28th Euromicro Conference on Real-Time Systems, ECRTS, pp. 152–162 (2016)
Wilhelm, R.: Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 309–322. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_25
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 36:1–36:53 (2008)
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 Trans. CAD Integr. Circuits Syst. 28(7), 966–978 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Mangean, A., Béchennec, JL., Briday, M., Faucou, S. (2017). WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction. In: Barkaoui, K., Boucheneb, H., Mili, A., Tahar, S. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2017. Lecture Notes in Computer Science(), vol 10466. Springer, Cham. https://doi.org/10.1007/978-3-319-66176-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-66176-6_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66175-9
Online ISBN: 978-3-319-66176-6
eBook Packages: Computer ScienceComputer Science (R0)