Article

r-TuBound: loop bounds for WCET analysis (tool paper)

Authors:

LPAR'12: Proceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

Pages 435 - 444

https://doi.org/10.1007/978-3-642-28717-6_34

Published: 11 March 2012 Publication History

Publisher Site

Abstract

We describe the structure and the usage of a new software tool, called r-TuBound, for deriving symbolic loop iteration bounds in the worst-case execution time (WCET) analysis of programs. r-TuBound implements algorithms for pattern-based recurrence solving and program flow refinement, and it was successfully tested on a wide range of examples. The purpose of this article is to illustrate what r-TuBound can do and how it can be used to derive the WCET of programs.

References

[1]

Blanc, R., Henzinger, T. A., Hottelier, T., Kovács, L.: ABC: Algebraic Bound Computation for Loops. In: Clarke, E. M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 103-118. Springer, Heidelberg (2010)

Digital Library

Google Scholar

[2]

Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174-177. Springer, Heidelberg (2009)

Digital Library

Google Scholar

[3]

Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, vol. 104. American Mathematical Society (2003)

Google Scholar

[4]

Gustafsson, J., Ermedahl, A., Sandberg, C., Lisper, B.:Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. In: Proc. of RTSS, pp. 57-66 (2006)

Digital Library

Google Scholar

[5]

Knoop, J., Kovacs, L., Zwirchmayr, J.: An Evaluation of WCET Analysis using Symbolic Loop Bounds. In: Proc. of WCET (2011)

Google Scholar

[6]

Knoop, J., Kovacs, L., Zwirchmayr, J.: Symbolic Loop Bound Computation forWCET Analysis. In: Proc. of PSI, p. 116 (2011)

Digital Library

Google Scholar

[7]

De Michiel, M., Bonenfant, A., Cassé, H., Sainrat, P.: Static Loop Bound Analysis of C Programs Based on Flow Analysis and Abstract Interpretation. In: RTCSA, pp. 161-166 (2008)

Digital Library

Google Scholar

[8]

Schoeberl, M., Puffitsch, W., Pedersen, R. U., Huber, B.:Worst-case Execution Time Analysis for a Java Processor. Software: Practice and Experience 40/6, 507-542 (2010)

Digital Library

Google Scholar

[9]

Prantl, A.: The Termite Library, http://www.complang.tuwien.ac.at/adrian/termite/Manual/

Google Scholar

[10]

Prantl, A., Schordan, M., Knoop, J.: TuBound - A Conceptually New Tool for WCET Analysis. In: Proc. of WCET, pp. 141-148 (2008)

Google Scholar

[11]

von Hanxleden, R., et al.: The WCET Tool Challenge 2011: Report. In: Proc. of WCET (2011) (under journal submission)

Google Scholar

Cited By

View all

Schuster SWägemann PUlbrich PSchröder-Preikschat WHenkel JLiu X(2021)Annotate once – analyze anywhere: context-aware WCET analysis by user-defined abstractionsProceedings of the 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3461648.3463847(54-66)Online publication date: 22-Jun-2021
https://dl.acm.org/doi/10.1145/3461648.3463847
Chen HDavid CKroening DSchrammel PWachter B(2017)Bit-Precise Procedure-Modular Termination AnalysisACM Transactions on Programming Languages and Systems10.1145/312113640:1(1-38)Online publication date: 10-Dec-2017
https://dl.acm.org/doi/10.1145/3121136
Knoop JKovács LZwirchmayr J(2017)Replacing conjectures by positive knowledgeJournal of Symbolic Computation10.1016/j.jsc.2016.07.02380:P1(101-124)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.023
Show More Cited By

Recommendations

The R-LRPD Test: Speculative Parallelization of Partially Parallel Loops
IPDPS '02: Proceedings of the 16th International Parallel and Distributed Processing Symposium

Current parallelizing compilers cannot identify a significant fraction of parallelizable loops because they have complex or statically insufficiently defined access patterns. In our previously proposed framework we have speculatively executed a loop as ...
The R-LRPD Test: Speculative Parallelization of Partially Parallel Loops
IPDPS '02: Proceedings of the 16th International Symposium on Parallel and Distributed Processing

Current parallelizing compilers cannot identify a significant fraction of parallelizable loops because they have complex or statically insufficiently defined access patterns. In our previously proposed framework we have speculatively executed a loop as ...
An upper bound for the k-power domination number in r-uniform hypergraphs
Abstract
Generalizing work on graphs, Chang and Roussel introduced k-power domination in hypergraphs and conjectured the upper bound for the k-power domination number for r-uniform hypergraphs on n vertices was n r + k. This upper bound was ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LPAR'12: Proceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

March 2012

444 pages

ISBN:9783642287169

Editors:
Nikolaj Bjørner
Microsoft Research, One Microsoft Way, Redmond, WA
,
Andrei Voronkov
School of computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, WA, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 March 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Schuster SWägemann PUlbrich PSchröder-Preikschat WHenkel JLiu X(2021)Annotate once – analyze anywhere: context-aware WCET analysis by user-defined abstractionsProceedings of the 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3461648.3463847(54-66)Online publication date: 22-Jun-2021
https://dl.acm.org/doi/10.1145/3461648.3463847
Chen HDavid CKroening DSchrammel PWachter B(2017)Bit-Precise Procedure-Modular Termination AnalysisACM Transactions on Programming Languages and Systems10.1145/312113640:1(1-38)Online publication date: 10-Dec-2017
https://dl.acm.org/doi/10.1145/3121136
Knoop JKovács LZwirchmayr J(2017)Replacing conjectures by positive knowledgeJournal of Symbolic Computation10.1016/j.jsc.2016.07.02380:P1(101-124)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.023
Brockschmidt MEmmes FFalke SFuhs CGiesl J(2016)Analyzing Runtime and Size Complexity of Integer ProgramsACM Transactions on Programming Languages and Systems10.1145/286657538:4(1-50)Online publication date: 2-Aug-2016
https://dl.acm.org/doi/10.1145/2866575
Knoop JKovács LZwirchmayr JAuguin Mde Simone RDavis RGrolleau E(2013)WCET squeezingProceedings of the 21st International conference on Real-Time Networks and Systems10.1145/2516821.2516847(161-170)Online publication date: 16-Oct-2013
https://dl.acm.org/doi/10.1145/2516821.2516847
Bonenfant ACassé Hde Michiel MKnoop JKovács LZwirchmayr JCucu-Grosjean LNavet NRochange CAnderson J(2012)FFXProceedings of the 20th International Conference on Real-Time and Network Systems10.1145/2392987.2392999(91-100)Online publication date: 8-Nov-2012
https://dl.acm.org/doi/10.1145/2392987.2392999

Abstract

References

Cited By

Recommendations

The R-LRPD Test: Speculative Parallelization of Partially Parallel Loops

The R-LRPD Test: Speculative Parallelization of Partially Parallel Loops

An upper bound for the k-power domination number in r-uniform hypergraphs

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations