research-article

Path-sensitive resource analysis compliant with assertions

Authors:

Joxan JaffarAuthors Info & Claims

EMSOFT '13: Proceedings of the Eleventh ACM International Conference on Embedded Software

Article No.: 15, Pages 1 - 10

Published: 29 September 2013 Publication History

Abstract

We consider the problem of bounding the worst-case resource usage of programs, where assertions about valid program executions may be enforced at selected program points. It is folklore that to be precise, path-sensitivity (up to loops) is needed. This entails unrolling loops in the manner of symbolic simulation. To be tractable, however, the treatment of the individual loop iterations must be greedy in the sense once analysis is finished on one iteration, we cannot backtrack to change it. We show that under these conditions, enforcing assertions produces unsound results. The fundamental reason is that complying with assertions requires the analysis to be fully sensitive (also with loops) wrt. the assertion variables.

We then present an algorithm where the treatment of each loop is separated in two phases. The first phase uses a greedy strategy in unrolling the loop. This phase explores what is conceptually a symbolic execution tree, which is of enormous size, while eliminates infeasible paths and dominated paths that guaranteed not to contribute to the worst case bound. A compact representation is produced at the end of this phase. Finally, the second phase attacks the remaining problem, to determine the worst-case path in the simplified tree, excluding all paths that violate the assertions from bound calculation. Scalability, in both phases, is achieved via an adaptation of a dynamic programming algorithm.

References

[1]

aiT Worst-Case Execution Time Analyzers. URL http://www.abs-int.com/ait/index.htm.

[2]

Bound-T time and stack analyser. URL http://www.bound-t.com.

[3]

D. H. Chu and J. Jaffar. Symbolic simulation on complicated loops for wcet path analysis. In EMSOFT, pages 319--328, 2011.

Digital Library

[4]

P. Cousot and R. Cousot. Abstract Interpretation: A unified lattice model for static analysis. In POPL, pages 238--252, 1977.

Digital Library

[5]

W. Craig. Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22(3):269--285, 1957.

[6]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453--457, 1975.

Digital Library

[7]

J. Engblom and A. Ermedahl. Modeling complex flows for worst-case execution time analysis. In RTSS, pages 163--174, 2000.

Digital Library

[8]

A. Ermedahl and J. Gustafsson. Deriving annotations for tight calculation of execution time. In Euro-Par, pages 1298--1307, 1997.

Digital Library

[9]

A. Ermedahl, F. Stappert, and J. Engblom. Clustered calculation of worst-case execution times. In CASES, pages 51--62, 2003.

Digital Library

[10]

D. Esteban and S. Genaim. On the limits of the classical approach to cost analysis. In SAS, pages 405--421, 2012.

Digital Library

[11]

S. Gulwani and F. Zuleger. The reachability-bound problem. In PLDI, pages 292--304, 2010.

Digital Library

[12]

J. Gustafsson, A. Ermedahl, and B. Lisper. Towards a flow analysis for embedded system C programs. In WORDS, pages 287--300, 2005.

Digital Library

[13]

J. Gustafsson, A. Ermedahl, and B. Lisper. Algorithms for infeasible path calculation. In WCET, 2006.

[14]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. In POPL, pages 357--370, 2011.

Digital Library

[15]

J. Jaffar, S. Michaylov, P. J. Stuckey, and R. H. C. Yap. The CLP(&Rscr;) language and system. ACM TOPLAS, 14(3):339--395, 1992.

Digital Library

[16]

J. Jaffar, A. E. Santosa, and R. Voicu. Efficient memoization for dynamic programming with ad-hoc constraints. In AAAI, pages 297--303, 2008.

Digital Library

[17]

H. C. Joksch. The shortest route problem with constraints. Journal of Mathematical Analysis and Applications, 14(2):191--197, 1966.

[18]

Y.-T. S. Li and S. Malik. Performance analysis of embedded software using implicit path enumeration. In DAC, pages 456--461, 1995.

Digital Library

[19]

T. Lundqvist and P. Stenström. An integrated path and timing analysis method based on cycle-level symbolic execution. Real-Time Systems, 17(2):183--207, 1999.

Digital Library

[20]

Mälardalen WCET research group benchmarks. URL http://www.mrtc.mdh.se/projects/wcet/benchmarks.html, 2006.

[21]

A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. In VMCAI, pages 346--362, 2007.

Digital Library

[22]

A. Thakur and R. Govindarajan. Comprehensive path-sensitive data-flow analysis. In CGO, pages 55--63, 2008.

Digital Library

[23]

H. Theiling, C. Ferdinand, and R. Wilhelm. Fast and precise WCET prediction by seperate cache and path analyses. Real-Time Systems, 18(2):157--179, 2000.

Digital Library

Cited By

Chu DJaffar JMaghareh R(2016)Symbolic execution for memory consumption analysisACM SIGPLAN Notices10.1145/2980930.290795551:5(62-71)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2980930.2907955
Chu DJaffar JMaghareh RKuo TWhalley D(2016)Symbolic execution for memory consumption analysisProceedings of the 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems10.1145/2907950.2907955(62-71)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2907950.2907955

Recommendations

Comprehensive path-sensitive data-flow analysis
CGO '08: Proceedings of the 6th annual IEEE/ACM international symposium on Code generation and optimization

Data-flow analysis is an integral part of any aggressive optimizing compiler. We propose a framework for improving the precision of data-flow analysis in the presence of complex control-flow. We initially perform data-flow analysis to determine those ...
Towards Path-Sensitive Points-to Analysis
SCAM '07: Proceedings of the Seventh IEEE International Working Conference on Source Code Analysis and Manipulation

Points-to analysis is a static program analysis aiming at analyzing the reference structure of dynamically allocated objects at compile-time. It constitutes the basis for many analyses and optimizations in software engineering and compiler construction. ...
Semi-sparse flow-sensitive pointer analysis
POPL '09

Pointer analysis is a prerequisite for many program analyses, and the effectiveness of these analyses depends on the precision of the pointer information they receive. Two major axes of pointer analysis precision are flow-sensitivity and context-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

EMSOFT '13: Proceedings of the Eleventh ACM International Conference on Embedded Software

September 2013

300 pages

ISBN:9781479914432

Program Chairs:
Rolf Ernst
Technical University of Braunschweig, Germany
,
Oleg Sokolsky
University of Pennsylvania

Sponsors

Publisher

IEEE Press

Publication History

Published: 29 September 2013

Check for updates

Qualifiers

Research-article

Conference

ESWEEK'13

Sponsor:

ESWEEK'13: Ninth Embedded System Week

September 29 - October 4, 2013

Quebec, Montreal, Canada

Acceptance Rates

EMSOFT '13 Paper Acceptance Rate 27 of 97 submissions, 28%;

Overall Acceptance Rate 60 of 203 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
46
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chu DJaffar JMaghareh R(2016)Symbolic execution for memory consumption analysisACM SIGPLAN Notices10.1145/2980930.290795551:5(62-71)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2980930.2907955
Chu DJaffar JMaghareh RKuo TWhalley D(2016)Symbolic execution for memory consumption analysisProceedings of the 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems10.1145/2907950.2907955(62-71)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2907950.2907955

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents