WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction
| Autor: | Armel Mangean, Sébastien Faucou, Mikaël Briday, Jean-Luc Bechennec |
|---|---|
| Přispěvatelé: | Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Kamel Barkaoui, Hanifa Boucheneb, Ali Mili, Sofiène Tahar |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Instruction prefetch [INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] Computer science 020207 software engineering 02 engineering and technology Parallel computing Static analysis Branch predictor 020202 computer hardware & architecture Power (physics) Microarchitecture Branch target predictor 0202 electrical engineering electronic engineering information engineering [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Cache Hardware_CONTROLSTRUCTURESANDMICROPROGRAMMING ComputingMilieux_MISCELLANEOUS |
| Zdroj: | Verification and Evaluation of Computer and Communication Systems. VECoS 2017 Verification and Evaluation of Computer and Communication Systems. VECoS 2017, Aug 2017, Montréal, Canada. pp.64--78, ⟨10.1007/978-3-319-66176-6_5⟩ Lecture Notes in Computer Science ISBN: 9783319661759 VECoS |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|