Analysing memory resource bounds for low-level programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Analysing memory resource bounds for low-level programs

Full text

Pdf (276 KB)

Source

International Symposium on Memory Management archive
Proceedings of the 7th international symposium on Memory management table of contents

Tucson, AZ, USA

SESSION: Heap measurement and analysis II table of contents

Pages 151-160

Year of Publication: 2008

ISBN:978-1-60558-134-7

Authors

Wei-Ngan Chin	National University of Singapore, Singapore, Singapore
Huu Hai Nguyen	National University of Singapore, Singapore, Singapore
Corneliu Popeea	National University of Singapore, Singapore, Singapore
Shengchao Qin	Durham University, Durham, United Kingdom

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 20, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1375634.1375656 What is a DOI?

ABSTRACT

Embedded systems are becoming more widely used but these systems are often resource constrained. Programming models for these systems should take into formal consideration resources such as stack and heap. In this paper, we show how memory resource bounds can be inferred for assembly-level programs. Our inference process captures the memory needs of each method in terms of the symbolic values of its parameters. For better precision, we infer path-sensitive information through a novel guarded expression format. Our current proposal relies on a Presburger solver to capture memory requirements symbolically, and to perform fixpoint analysis for loops and recursion. Apart from safety in memory adequacy, our proposal can provide estimate on memory costs for embedded devices and improve performance via fewer runtime checks against memory bound.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	AbsInt. StackAnalyzer - Stack Usage Analysis. http://www.absint.com/stackanalyzer.
	2	E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In European Symposium on Programming (ESOP), March 2007.
	3	E. Albert, S. Genaim, and M. Gomez-Zamalloa. Heap Space Analysis for Java Bytecode. In Proceedings of the International Symposium on Memory Management (ISMM '07), June 2007.
	4	R. M. Amadio, S. Coupet-Grimal, S. Dal Zilio, and L. Jakubiec. A Functional Scenario for Bytecode Verification of Resource Bounds. In 18th Int'l Conf. on Computer Science Logic (CSL04). Springer, LNCS, September 2004.
	5	D. Aspinall, S. Gilmore, M. Hofmann, D.Sannella, and I. Stark. Mobile Resource Guarantees for Smart Devices. In Int'l Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Springer LNCS, 2004.
	6	G. Balakrishnan, R. Gruian, T. Reps, and T. Teitelbaum. CodeSurfer/x86-A Platform for Analyzing x86 Executables. In Intl Symp. on Compiler Construction, 2005.
	7	M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In Int'l Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Springer LNCS, 2004.
	8	V. Braberman, F. Fernandez, D. Garbervetsky, and S. Yovine. Parametric Prediction of Heap Memory Requirements. In Proceedings of the International Symposium on Memory Management (ISMM '08), Tucson, Arizona, June 2008.
	9	V. Braberman, D. Garbervetsky, and S. Yovine. A static analysis for synthesizing parametric specifications of dynamic memory consumption. Journal of Object Technology. Special Issue: ECOOP 2005 Workshop FTfJP, 5(5):31--58, 2006.
	10	D. Brylow, N. Damgaard, and J. Palsberg. Static Checking of Interrupt-Driven Software. In Proceedings of the International Conference on Software Engineering (ICSE'01), Toronto, Canada, May 2001.
	11	D. Cachera, T. Jensen, D. Pichardie, and G. Schneider. Certified Memory Usage Analysis. In 13th International Symposium of Formal Methods Europe (FM'05), July 2005.
	12	K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg. Stack Size Analysis for Interrupt-Driven Programs. In 10th Annual International Static Analysis Symposium (SAS '03), San Diego, California, June 2003. Springer-Verlag.
	13	W.N. Chin, H.H. Nguyen, S.C. Qin, and M. Rinard. Memory Usage Verification for OO Programs. In Static Analysis Symposium, Springer LNCS, London, UK, September 2005.
	14	P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In ACM POPL, pages 84--96, 1978.
	15	M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69(1--3):35--45, December 2007.
	16	M. Guthaus, J. Ringenberg, D. Ernst, T. Austin, T. Mudge, and T. Brown. MiBench: A free, commercially representative embedded benchmark suite. In 4th IEEE International Workshop on Workload Characteristics, 2001.
	17	J. V. Guttag and J. J. Horning, editors. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
	18	C. A. R. Hoare and J. He. Unifying Theories of Programming. Prentice-Hall, 1998.
	19	M. Hofmann and S. Jost. Static prediction of heap space usage for first order functional programs. In ACM POPL, New Orleans, Louisiana, January 2003.
	20	M. Hofmann and S. Jost. Type-based amortised heap-space analysis. In European Symposium on Programming (ESOP), Vienna, Austria, March 2006.
	21	J. Hughes and L. Pareto. Recursion and Dynamic Data-Structures in Bounded Space: Towards Embedded ML Programming. In ICFP, September 1999.
	22	G.C. Necula, S. McPeak, S.P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. 2002.
	23	National Institute of Standards and Technology. Java SciMark benchmark for scientific computing. http://math.nist.gov/scimark2/.
	24	S. Peyton-Jones and et al. Glasgow Haskell Compiler. Available at http://www.haskell.org/ ghc.
	25	C. Popeea and W.N. Chin. Inferring disjunctive postconditions. In Asian Computing Science Conference (ASIAN), volume 4435 of Lecture Notes in Computer Science, pages 331--345. Springer, 2006.
	26	W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102--114, 1992.
	27	S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In Static Analysis Symposium, Springer LNCS, August 2006.
	28	M. Sitaraman, G. Kulczycki, J. Krone, W. F. Ogden, and A. L. N. Reddy. Performance specification of software components. In Symposium on Software Reusability: Putting Software Reuse in Context, Toronto, Canada, May 2001.