More Web Proxy on the site http://driver.im/

article

ResAna: a resource analysis toolset for real-time JAVA

Authors:

Rody W.J. Kersten,

Bernard E. Gastel,

Olha Shkaravska,

Manuel Montenegro,

Marko C.J.D. EekelenAuthors Info & Claims

Concurrency and Computation: Practice & Experience, Volume 26, Issue 14

Pages 2432 - 2455

https://doi.org/10.1002/cpe.3154

Published: 25 September 2014 Publication History

Abstract

For real-time and embedded systems, limiting the consumption of time and memory resources is often an important part of the requirements. Being able to predict bounds on the consumption of such resources during the development process of the code can be of great value. In this paper, we focus mainly on memory-related bounds. Recent research results have advanced the state of the art of resource consumption analysis. In this paper, we present a toolset that makes it possible to apply these research results in practice for real-time systems enabling JAVA developers to analyse symbolic loop bounds, symbolic bounds on heap size and both symbolic and numeric bounds on stack size. We describe which theoretical additions were needed in order to achieve this. We give an overview of the capabilities of the RESANA Radboud University Nijmegen, The Netherlands toolset that is the result of this effort. The toolset can not only perform generally applicable analyses, but it also contains a part of the analysis that is dedicated to the developers' real-time virtual machine, such that the results apply directly to the actual development environment that is used in practice. Copyright © 2013 John Wiley & Sons, Ltd.

References

[1]

<familyNamePrefix>de</familyNamePrefix>Mol MJ, Rensink A, Hunt JJ. Graph transforming Java data. In Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering FASE 2012, Talinn, Estonia, Vol.Volume 7212, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2012; pp.209-223.

[2]

Kersten R, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Gastel B, Montenegro M, <familyNamePrefix>van</familyNamePrefix>Eekelen M. Making resource analysis practical for real-time Java. In Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, <bookSeriesTitle>JTRES '12</bookSeriesTitle>. ACM: New York, NY, USA, 2012; pp.135-144. Available from: "http://doi.acm.org/10.1145/2388936.2388959".

[3]

Wedzinga G, Wiegmink K. Using charter tools to develop a safety-critical avionics application in Java. In Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, <bookSeriesTitle>JTRES '12</bookSeriesTitle>. ACM: New York, NY, USA, 2012; pp.125-134. Available from: http://doi.acm.org/10.1145/2388936.2388958.

Digital Library

[4]

Albert E, Arenas P, Genaim S, Puebla G. Closed-form upper bounds in static cost analysis. Journal of Automated Reasoning February 2011; Volume 46 Issue 2: pp.161-203.

[5]

<familyNamePrefix>van</familyNamePrefix>Kesteren R, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M. Inferring static non-monotonically sized types through testing. In 16th International Workshop on Functional and Constraint Logic Programming WFLP'07, Vol.Volume 216C, <bookSeriesTitle>Electronic Notes in Theoretical Computer Science</bookSeriesTitle>: Paris, France, 2008; pp.45-63.

[6]

Gulwani S, Zuleger F. The reachability-bound problem. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, <bookSeriesTitle>PLDI '10</bookSeriesTitle>. ACM: New York, NY, USA, 2010; pp.292-304.

[7]

Hoffmann J, Aehlig K, Hofmann M. Multivariate amortized resource analysis. In POPL'11, Ball T, Sagiv M eds. ACM: New York, NY, USA, 2011; pp.357-370.

Digital Library

[8]

Amadio RM. Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae August 2005; Volume 65 Issue 1-2: pp.29-60. Available from: "http://portal.acm.org/citation.cfm?id=1227143.1227146".

[9]

<familyNamePrefix>de</familyNamePrefix>Dios J, Montenegro M, Peña R. Certified absence of dangling pointers in a language with explicit deallocation. In 8th International Conference on Integrated Formal Methods, IFM 2010, <bookSeriesTitle>LNCS 6396</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2010; pp.305-319.

[10]

<familyNamePrefix>van</familyNamePrefix>Eekelen M, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Kesteren R, Jacobs B, Poll E, Smetsers S. AHA: amortized heap space usage analysis. In Selected Papers of the 8^th International Symposium on Trends in Functional Programming TFP'07, New York, USA, Morazán M ed. Intellect Publishers: UK, 2007; pp.36-53.

[11]

Leavens GT, Poll E, Clifton C, Cheon Y, Ruby C, Cok D, Müller P, Kiniry J, Chalin P. JML reference manual. Draft revision 1.200, February 2007.

[12]

Beckert B, Hähnle R, Schmitt PH eds. Verification of Object-Oriented Software: the KeY Approach, LNCS 4334. Springer: Berlin, Heidelberg, 2007.

[13]

Brown CW. QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin December 2003; Volume 37 Issue 4: pp.97-108. Available from: http://doi.acm.org/10.1145/968708.968710.

[14]

Shkaravska O, Kersten R, VanEekelen M. Test-based inference of polynomial loop-bound functions. In PPPJ'10: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java, Krall A, Mössenböck H eds. ACM: New York, NY, USA, 2010; pp.99-108.

[15]

Albert E, Arenas P, Genaim S, Puebla G, Zanardini D. COSTA: design and implementation of a cost and termination analyzer for Java bytecode. In Formal Methods for Components and Objects, vol.Volume 5382, <familyNamePrefix>de</familyNamePrefix>Boer F, Bonsangue M, Graf S, <familyNamePrefix>de</familyNamePrefix>Roever W eds, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2008; pp.113-132.

Digital Library

[16]

Siebert F. Hard realtime garbage collection in modern object oriented programming languages. PhD Thesis, University of Karlsruhe, 2002.

[17]

Montenegro M, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M, Peña R. Interpolation-based height analysis for improving a recurrence solver. In Proceedings of the 2nd Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA 2011, <bookSeriesTitle>LNCS 7177</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2012; pp.36-53.

Digital Library

[18]

Hunt JJ, Tonin I, Siebert FB. Using global data flow analysis on bytecode to aid worst case execution time analysis for real-time Java programs. In JTRES '08: Proceedings of the 6th International Workshop on Java Technologies for Real-Time and Embedded Systems. ACM: New York, NY, USA, 2008; pp.97-105. Available from: http://doi.acm.org/10.1145/1434790.1434806.

[19]

Chui CK, Lai MJ. Vandermonde determinants and Lagrange interpolation in R^s. Nonlinear and Convex Analysis 1987; Volume 107: pp.23-35.

[20]

Poll E, Chalin P, Cok D, Kiniry J, Leavens GT. Beyond assertions: advanced specification and verification with JML and ESC/Java2. In Formal Methods for Components and Objects FMCO 2005, Vol.Volume 4111 of LNCS, <bookSeriesTitle>Revised Lectures</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2006; pp.342-363.

[21]

King JC. Symbolic execution and program testing. Communications of the ACM July 1976; Volume 19: pp.385-394.

[22]

Ranise S, Tinelli C. The SMT-LIB format: an initial proposal, 2003. Available from: "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.9580".

[23]

Albert E, Genaim S, Gómez-Zamalloa M. Parametric inference of memory requirements for garbage collected languages. In ISMM'10, Vitek J, Lea D eds. ACM: New York, NY, USA, 2010; pp.121-130.

Digital Library

[24]

Wegbreit B. Mechanical program analysis. Communications of the ACM 1975; Volume 18 Issue 9: pp.528-539.

[25]

Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, Vol.Volume 2937, Steffen B, Levi G eds, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2004; pp.465-486.

[26]

Hunt JJ, Siebert FB, Schmitt PH, Tonin I. Provably correct loops bounds for realtime java programs. In JTRES '06: Proceedings of the 4th International Workshop on Java Technologies for Real-Time and Embedded Systems. ACM: New York, NY, USA, 2006; pp.162-169. Available from: http://doi.acm.org/10.1145/1167999.1168026.

[27]

Schoofs T, Jenn E, Leriche S, Nilsen K, Gauthier L, Richard-Foy M. Use of PERC Pico in the AIDA avionics platform. In Proceedings of the 7th International Workshop on Java Technologies for Real-Time and Embedded Systems. ACM: New York, NY, USA, 2009; pp.169-178.

[28]

Kalibera T, Hagelberg J, Pizlo F, Plsek A, Titzer B, Vitek J. Cd _x: a family of real-time Java benchmarks. In Proceedings of the 7Th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2009, Madrid, Spain, September 23-25, 2009. ACM: New York, NY, USA, 2009; pp.41-50.

[29]

Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Kesteren R, <familyNamePrefix>van</familyNamePrefix>Eekelen M. Polynomial size analysis for first-order functions. In Typed Lambda Calculi and Applications TLCA'2007, Paris, France, Vol.Volume 4583, Rocca SRD ed., <bookSeriesTitle>LNCS</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2007; pp.351-366.

[30]

Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M, Tamalet A. Collected size semantics for functional programs over lists. In Proceedings of the 20th International Conference on Implementation and Application of Functional Languages, <bookSeriesTitle>IFL'08</bookSeriesTitle>. Springer-Verlag: Berlin, Heidelberg, 2011; pp.118-137. Available from: "http://dl.acm.org/citation.cfm?id=2044476.2044483".

[31]

Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M, <familyNamePrefix>van</familyNamePrefix>Kesteren R. Polynomial size analysis of first-order shapely functions. Logic in Computer Science 2009; Volume 2:10 Issue 5. Available from: "http://arxiv.org/abs/arxiv:0902.2073".

[32]

Tamalet A, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M. Size analysis of algebraic data types. In Trends in Functional Programming, Vol.Volume 9, Achten P, Koopman P, Morazán M eds, <bookSeriesTitle>Intellect</bookSeriesTitle>: Bristol, United Kingdom, 2009; pp.33-48. ISBN 978-1-84150-277-9.

[33]

Gobi A, Shkaravska O, <familyNamePrefix>van</familyNamePrefix>Eekelen M. Higher-order size checking without subtyping. In Proceedings of the 13th International Symposium on Trends in Functional Programming TFP2012, Vol.Volume 7829, Loidl HW, Hammond K eds, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2013; pp.53-68.

Digital Library

[34]

Albert E, Bubel R, Genaim S, Hähnle R, Puebla G, Román-Díez G. Verified resource guarantees using COSTA and KeY. In Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, <bookSeriesTitle>PEPM '11</bookSeriesTitle>. ACM: New York, NY, USA, 2011; pp.73-76.

[35]

DeMichiel M, Bonenfant A, Cassé H, Sainrat P. Static loop bound analysis of C programs based on flow analysis and abstract interpretation. In RTCSA '08: Proceedings of the 2008 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications. IEEE Computer Society: Washington, DC, USA, 2008; pp.161-166.

[36]

Ermedahl A, Sandberg C, Gustafsson J, Bygde S, Lisper B. Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In 7th International Workshop On Worst-Case Execution Time WCET Analysis, Rochange C ed. Internationales Begegnungs- und Forschungszentrum für Informatik IBFI, Schloss Dagstuhl, Germany: Dagstuhl, Germany, 2007; pp.58-63.

[37]

Lokuciejewski P, Cordes D, Falk H, Marwedel P. A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models. In CGO '09: Proceedings of the 7th Annual IEEE/ACM International Symposium on Code Generation and Optimization. IEEE Computer Society: Washington, DC, USA, 2009; pp.136-146.

[38]

Gulwani S. SPEED: symbolic complexity bound analysis. In CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification. Springer-Verlag: Berlin, Heidelberg, 2009; pp.51-62.

Digital Library

[39]

Fulara J, Jakubczyk K. Practically applicable formal methods. In SOFSEM '10: Proceedings of the 36th Conference on Current Trends in Theory and Practice of Computer Science. Springer: Berlin, Heidelberg, 2010; pp.407-418.

Digital Library

[40]

Gulwani S, Jain S, Koskinen E. Control-flow refinement and progress invariants for bound analysis. In PLDI '09: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM: New York, NY, USA, 2009; pp.375-385.

[41]

Sharma R, Gupta S, Hariharan B, Aiken A, Liang P, Nori A. A data driven approach for algebraic loop invariants. In Programming Languages and Systems, Vol.Volume 7792, Felleisen M, Gardner P eds, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2013; pp.574-592. Available from: "http://dx.doi.org/10.1007/978-3-642-37036-6_31".

[42]

Reineke J, Grund D, Berg C, Wilhelm R. Timing predictability of cache replacement policies. Real-Time Systems November 2007; Volume 37 Issue 2: pp.99-122. Available from: "http://rw4.cs.uni-saarland.de/~grund/papers/rts07-predictability.pdf".

[43]

Wilhelm R, Engblom J, Ermedahl A, Holsti N, Thesing S, Whalley D, Bernat G, Ferdinand C, Heckmann R, Mitra T, Mueller F, Puaut I, Puschner P, Staschulat J, Stenström P. The worst-case execution-time problemoverview of methods and survey of tools. ACM Transactions on Embedded Computing Systems May 2008; Volume 7 Issue 3: pp.36:1-36:53. Available from: http://doi.acm.org/10.1145/1347375.1347389.

[44]

Herter J, Backes P, Haupenthal F, Reineke J. CAMA: a predictable cache-aware memory allocator. In Proceedings of the 23rd Euromicro Conference on Real-Time Systems ECRTS '11. IEEE Computer Society: Washington, DC, USA, July 2011. Available from: "http://rw4.cs.uni-sb.de/~jherter/papers/CAMAecrts11.pdf".

Digital Library

[45]

Albert E, Genaim S, Masud AN. More precise yet widely applicable cost analysis. In VMCAI'11, Vol.Volume 6538, Jhala R, Schmidt DA eds, <bookSeriesTitle>Lecture Notes in Computer Science</bookSeriesTitle>. Springer: Berlin, Heidelberg, 2011; pp.38-53.

[46]

Hofmann M, Jost S. Static prediction of heap space usage for first-order functional programs. In POPL'03. ACM Press: New York, NY, USA, 2003; pp.185-197. Available from: http://doi.acm.org/10.1145/604131.604148.

Digital Library

[47]

Hoffmann J, Hofmann M. Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. In ESOP'10, <bookSeriesTitle>LNCS 6012</bookSeriesTitle>. Springer, ACM: New York, NY, USA, 2010; pp.287-306.

[48]

Wang S, Qiu Z, Qin S, Chin WN. Stack bound inference for abstract Java bytecode. In Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, <bookSeriesTitle>TASE '10</bookSeriesTitle>. IEEE Computer Society: Washington, DC, USA, 2010; pp.57-66. Available from: "http://dx.doi.org/10.1109/TASE.2010.24".

Cited By

Gastel PGastel BEekelen MMarr SSartor J(2018)Detecting energy bugs and hotspots in control software using model checkingCompanion Proceedings of the 2nd International Conference on the Art, Science, and Engineering of Programming10.1145/3191697.3213805(93-98)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3191697.3213805
Kersten RSchäf MKahsai T(2017)Resource Contracts for JavaACM SIGSOFT Software Engineering Notes10.1145/3011286.301129441:6(1-5)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1145/3011286.3011294
Morton JMaier PTrinder P(2016)JIT-Based Cost Analysis for Dynamic Program TransformationsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.12.012330:C(5-25)Online publication date: 10-Dec-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.12.012

ResAna: a resource analysis toolset for real-time JAVA
1. Computer systems organization

Recommendations

Making resource analysis practical for real-time Java
JTRES '12: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems

For real-time and embedded systems limiting the consumption of time and memory resources is often an important part of the requirements. Being able to predict bounds on the consumption of these resources during the development process of the code can be ...
Static Loop Bound Analysis of C Programs Based on Flow Analysis and Abstract Interpretation
RTCSA '08: Proceedings of the 2008 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications

One of the important steps in processing the worst case execution time (WCET) of a program is to determine the loops upper bounds. Such bounds are crucial when verifying real-time systems. In this paper, we propose a static loop bound analysis which ...
Robust Resource Bounds with Static Analysis and Bayesian Inference

There are two approaches to automatically deriving symbolic worst-case resource bounds for programs: static analysis of the source code and data-driven analysis of cost measurements obtained by running the program. Static resource analysis is usually ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Concurrency and Computation: Practice & Experience

Concurrency and Computation: Practice & Experience Volume 26, Issue 14

September 2014

143 pages

ISSN:1532-0626

EISSN:1532-0634

Issue’s Table of Contents

Publisher

John Wiley and Sons Ltd.

United Kingdom

Publication History

Published: 25 September 2014

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gastel PGastel BEekelen MMarr SSartor J(2018)Detecting energy bugs and hotspots in control software using model checkingCompanion Proceedings of the 2nd International Conference on the Art, Science, and Engineering of Programming10.1145/3191697.3213805(93-98)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3191697.3213805
Kersten RSchäf MKahsai T(2017)Resource Contracts for JavaACM SIGSOFT Software Engineering Notes10.1145/3011286.301129441:6(1-5)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1145/3011286.3011294
Morton JMaier PTrinder P(2016)JIT-Based Cost Analysis for Dynamic Program TransformationsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.12.012330:C(5-25)Online publication date: 10-Dec-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.12.012

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents