Timed Games for Computing WCET for Pipelined Processors with Caches. Cassez, F. In 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011, pages 195–204, 2011. IEEE.
Paper
Slides
Link doi abstract bibtex In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms 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 modeling 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. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution.
@inproceedings{cassez-acsd-2011,
author = {Franck Cassez},
title = {Timed Games for Computing {WCET} for Pipelined Processors with Caches},
booktitle = {11th International Conference on Application of Concurrency to System
Design, {ACSD} 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011},
pages = {195--204},
year = {2011},
publisher = {{IEEE}},
url = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.15},
doi = {10.1109/ACSD.2011.15},
timestamp = {Wed, 15 Feb 2012 09:59:43 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/acsd/Cassez11},
bibsource = {dblp computer science bibliography, http://dblp.org},
urlpaper = {papers/acsd-2011.pdf},
urlslides = {papers/slides-acsd-2011.pdf},
ABSTRACT = {In this paper we introduce a framework for computing upper bounds yet
accurate WCET for hardware platforms 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 modeling 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. We also show that this framework can easily
be extended to take into account dynamic changes in the speed of the processor
during program execution.
},
ee = {http://dx.doi.org/10.1109/ACSD.2011.15},
keywords = {wcet, timed automata},
category = {wcet},
show = {},
category= {wcet},
mywebpage = {wcet},
Type = {B - International Conferences},
}
Downloads: 0
{"_id":"vRdMFjgiLCnqTFE8w","bibbaseid":"cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011","author_short":["Cassez, F."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]}],"title":"Timed Games for Computing WCET for Pipelined Processors with Caches","booktitle":"11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011","pages":"195–204","year":"2011","publisher":"IEEE","url":"http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.15","doi":"10.1109/ACSD.2011.15","timestamp":"Wed, 15 Feb 2012 09:59:43 +0100","biburl":"http://dblp.uni-trier.de/rec/bib/conf/acsd/Cassez11","bibsource":"dblp computer science bibliography, http://dblp.org","urlpaper":"papers/acsd-2011.pdf","urlslides":"papers/slides-acsd-2011.pdf","abstract":"In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms 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 modeling 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. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution. ","ee":"http://dx.doi.org/10.1109/ACSD.2011.15","keywords":"wcet, timed automata","category":"wcet","show":"","mywebpage":"wcet","bibtex":"@inproceedings{cassez-acsd-2011,\n author = {Franck Cassez},\n title = {Timed Games for Computing {WCET} for Pipelined Processors with Caches},\n booktitle = {11th International Conference on Application of Concurrency to System\n Design, {ACSD} 2011, Newcastle Upon Tyne, UK, 20-24 June, 2011},\n pages = {195--204},\n year = {2011},\n publisher = {{IEEE}},\n url = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.15},\n doi = {10.1109/ACSD.2011.15},\n timestamp = {Wed, 15 Feb 2012 09:59:43 +0100},\n biburl = {http://dblp.uni-trier.de/rec/bib/conf/acsd/Cassez11},\n bibsource = {dblp computer science bibliography, http://dblp.org},\n urlpaper = {papers/acsd-2011.pdf},\n urlslides = {papers/slides-acsd-2011.pdf},\n ABSTRACT = {In this paper we introduce a framework for computing upper bounds yet\naccurate WCET for hardware platforms with caches and pipelines. The methodology\nwe propose consists of 3 steps: 1) given a program to analyse, compute an\nequivalent (WCET-wise) abstract program; 2) build a timed game by composing\nthis abstract program with a network of timed automata modeling the\narchitecture; and 3) compute the WCET as the optimal time to reach a winning\nstate in this game. We demonstrate the applicability of our framework on\nstandard benchmarks for an ARM9 processor with instruction and data caches, and\ncompute the WCET with UPPAAL-TiGA. We also show that this framework can easily\nbe extended to take into account dynamic changes in the speed of the processor\nduring program execution.\n},\nee = {http://dx.doi.org/10.1109/ACSD.2011.15},\n keywords = {wcet, timed automata},\n category = {wcet},\n show = {},\n category= {wcet},\n mywebpage = {wcet},\n Type = {B - International Conferences},\n\n}\n\n\n","author_short":["Cassez, F."],"key":"cassez-acsd-2011","id":"cassez-acsd-2011","bibbaseid":"cassez-timedgamesforcomputingwcetforpipelinedprocessorswithcaches-2011","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/acsd-2011.pdf","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/slides-acsd-2011.pdf","Link":"http://dx.doi.org/10.1109/ACSD.2011.15"},"keyword":["wcet","timed automata"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["qbqYFWskmoonRB43F","8742EsvjQfyP2fYBW","yYF8uwWqay28JyxZC"],"keywords":["wcet","timed automata"],"search_terms":["timed","games","computing","wcet","pipelined","processors","caches","cassez"],"title":"Timed Games for Computing WCET for Pipelined Processors with Caches","year":2011}