Timed games for computing WCET for pipelined processors with caches

Franck Cassez

doi:10.1109/ACSD.2011.15

Timed games for computing WCET for pipelined processors with caches

Franck Cassez^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

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 language	English
Title of host publication	2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011)
Editors	Benoît Caillaud, Josep Carmona, Kunihiko Hiraishi
Place of Publication	Los Alamitos, CA
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	195-204
Number of pages	10
ISBN (Electronic)	9780769543871
ISBN (Print)	9781612849744
DOIs	https://doi.org/10.1109/ACSD.2011.15
Publication status	Published - 2011
Externally published	Yes
Event	11th International Conference on Application of Concurrency to System Design, ACSD 2011 - Newcastle Upon Tyne, United Kingdom Duration: 20 Jun 2011 → 24 Jun 2011

Publication series

Name	Application of Concurrency to System Design
Publisher	IEEE Computer Society
ISSN (Print)	1550-4808

Other

Other	11th International Conference on Application of Concurrency to System Design, ACSD 2011
Country/Territory	United Kingdom
City	Newcastle Upon Tyne
Period	20/06/11 → 24/06/11

Keywords

Cache
Pipeline
Timed Automata
Worst-Case Execution Time

Access to Document

10.1109/ACSD.2011.15

Cite this

Cassez, F. (2011). Timed games for computing WCET for pipelined processors with caches. In B. Caillaud, J. Carmona, & K. Hiraishi (Eds.), 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011) (pp. 195-204). (Application of Concurrency to System Design). Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/ACSD.2011.15

Cassez, Franck. / Timed games for computing WCET for pipelined processors with caches. 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011). editor / Benoît Caillaud ; Josep Carmona ; Kunihiko Hiraishi. Los Alamitos, CA : Institute of Electrical and Electronics Engineers (IEEE), 2011. pp. 195-204 (Application of Concurrency to System Design).

@inproceedings{8184edabf63f4c4e958797a8a00a3571,

title = "Timed games for computing WCET for pipelined processors with caches",

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.",

keywords = "Cache, Pipeline, Timed Automata, Worst-Case Execution Time",

author = "Franck Cassez",

year = "2011",

doi = "10.1109/ACSD.2011.15",

language = "English",

isbn = "9781612849744",

series = "Application of Concurrency to System Design",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "195--204",

editor = "Beno{\^i}t Caillaud and Josep Carmona and Kunihiko Hiraishi",

booktitle = "2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011)",

address = "United States",

note = "11th International Conference on Application of Concurrency to System Design, ACSD 2011 ; Conference date: 20-06-2011 Through 24-06-2011",

}

Cassez, F 2011, Timed games for computing WCET for pipelined processors with caches. in B Caillaud, J Carmona & K Hiraishi (eds), 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011). Application of Concurrency to System Design, Institute of Electrical and Electronics Engineers (IEEE), Los Alamitos, CA, pp. 195-204, 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, United Kingdom, 20/06/11. https://doi.org/10.1109/ACSD.2011.15

Timed games for computing WCET for pipelined processors with caches. / Cassez, Franck.

2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011). ed. / Benoît Caillaud; Josep Carmona; Kunihiko Hiraishi. Los Alamitos, CA : Institute of Electrical and Electronics Engineers (IEEE), 2011. p. 195-204 (Application of Concurrency to System Design).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Timed games for computing WCET for pipelined processors with caches

AU - Cassez, Franck

PY - 2011

Y1 - 2011

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

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

KW - Cache

KW - Pipeline

KW - Timed Automata

KW - Worst-Case Execution Time

UR - http://www.scopus.com/inward/record.url?scp=80052622628&partnerID=8YFLogxK

U2 - 10.1109/ACSD.2011.15

DO - 10.1109/ACSD.2011.15

M3 - Conference proceeding contribution

AN - SCOPUS:80052622628

SN - 9781612849744

T3 - Application of Concurrency to System Design

SP - 195

EP - 204

BT - 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011)

A2 - Caillaud, Benoît

A2 - Carmona, Josep

A2 - Hiraishi, Kunihiko

PB - Institute of Electrical and Electronics Engineers (IEEE)

CY - Los Alamitos, CA

T2 - 11th International Conference on Application of Concurrency to System Design, ACSD 2011

Y2 - 20 June 2011 through 24 June 2011

ER -

Cassez F. Timed games for computing WCET for pipelined processors with caches. In Caillaud B, Carmona J, Hiraishi K, editors, 2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011). Los Alamitos, CA: Institute of Electrical and Electronics Engineers (IEEE). 2011. p. 195-204. (Application of Concurrency to System Design). https://doi.org/10.1109/ACSD.2011.15

Timed games for computing WCET for pipelined processors with caches

Abstract

Publication series

Other

Keywords

Access to Document

Other files and links

Fingerprint

Cite this