Timed games for computing WCET for pipelined processors with caches

Franck Cassez*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

10 Citations (Scopus)

Abstract

We introduce a framework for computing upper bounds of WCET for hardware with caches and pipelines. The methodology we propose consists of 3 steps: 1) given a program to analyse, compute an equivalent (WCET-wise) abstract program, 2) build a timed game by composing this abstract program with a network of timed automata modelling the architecture, and 3) compute the WCET as the optimal time to reach a winning state in this game. We demonstrate the applicability of our framework on standard benchmarks for an ARM9 processor with instruction and data caches, and compute the WCET with UPPAAL-TiGA.

Original languageEnglish
Title of host publication 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011)
EditorsBenoît Caillaud, Josep Carmona, Kunihiko Hiraishi
Place of PublicationLos Alamitos, CA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages195-204
Number of pages10
ISBN (Electronic)9780769543871
ISBN (Print)9781612849744
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event11th International Conference on Application of Concurrency to System Design, ACSD 2011 - Newcastle Upon Tyne, United Kingdom
Duration: 20 Jun 201124 Jun 2011

Publication series

NameApplication of Concurrency to System Design
PublisherIEEE Computer Society
ISSN (Print)1550-4808

Other

Other11th International Conference on Application of Concurrency to System Design, ACSD 2011
CountryUnited Kingdom
CityNewcastle Upon Tyne
Period20/06/1124/06/11

Keywords

  • Cache
  • Pipeline
  • Timed Automata
  • Worst-Case Execution Time

Fingerprint Dive into the research topics of 'Timed games for computing WCET for pipelined processors with caches'. Together they form a unique fingerprint.

Cite this