Advertisement

Eliminating Stack Overflow by Abstract Interpretation

  • John Regehr
  • Alastair Reid
  • Kirk Webb
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2855)

Abstract

An important correctness criterion for software running on embedded microcontrollers is stack safety: a guarantee that the call stack does not overflow. We address two aspects of the problem of creating stack-safe embedded software that also makes efficient use of memory: statically bounding worst-case stack depth, and automatically reducing stack memory requirements. Our first contribution is a method for statically guaranteeing stack safety by performing whole-program analysis, using an approach based on context-sensitive abstract interpretation of machine code. Abstract interpretation permits our analysis to accurately model when interrupts are enabled and disabled, which is essential for accurately bounding the stack depth of typical embedded systems. We have implemented a stack analysis tool that targets Atmel AVR microcontrollers, and tested it on embedded applications compiled from up to 30,000 lines of C . We experimentally validate the accuracy of the tool, which runs in a few seconds on the largest programs that we tested. The second contribution of this paper is a novel framework for automatically reducing stack memory requirements. We show that goal-directed global function inlining can be used to reduce the stack memory requirements of component-based embedded software, on average, to 40% of the requirement of a system compiled without inlining, and to 68% of the requirement of a system compiled with aggressive whole-program inlining that is not directed towards reducing stack usage.

Keywords

Embed System Abstract Interpretation Code Size Assembly Language Embed Software 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    AbsInt. StackAnalyzer, http://www.absint.com/stackanalyzer
  2. 2.
    Ayers, A., Gottlieb, R., Schooler, R.: Aggressive inlining. In: Proc. of Programming Language Design and Implementation, Las Vegas, NV, June 1997, pp. 134–145(1997)Google Scholar
  3. 3.
    Brylow, D., Damgaard, N., Palsberg, J.: Static checking of interrupt-driven software. In: Proc. of the 23rd Intl. Conf. on Software Engineering, Toronto, Canada, May 2001, pp. 47–56 (2001)Google Scholar
  4. 4.
    Engblom, J.: Static properties of commercial embedded real-time programs, and their implication for worst-case execution time analysis. In: Proc. of the 5th IEEE Real-Time Technology and Applications Symp., Vancouver, Canada (June 1999)Google Scholar
  5. 5.
    Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesC language: Aholistic approach to networked embedded systems. In: Proc. of Programming Language Design and Implementation, San Diego, CA, June 2003, pp. 1–11 (2003)Google Scholar
  6. 6.
    Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In: Proc. of the 9th Intl. Conf. on Architectural Support for Programming Languages and Operating Systems, Cambridge, MA, November 2000, pp. 93–104 (2000)Google Scholar
  7. 7.
    Leupers, R., Marwedel, P.: Function inlining under code size constraints for embedded processors. In: Proc. of the International Conference on Computer-Aided Design, San Jose, CA, November 1999, pp. 253–256 (1999)Google Scholar
  8. 8.
    Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. The Java Series. Addison-Wesley, Reading (1997)Google Scholar
  9. 9.
    Palsberg, J., Ma, D.: A typed interrupt calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 291–310. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    The Autopilot Project, http://autopilot.sourceforge.net
  11. 11.
    Reid, A., Flatt, M., Stoller, L., Lepreau, J., Eide, E.: Knit: Component composition for systems software. In: Proc. of the 4th Symp. on Operating Systems Design and Implementation, San Diego, CA, October 2000, pp. 347–360(2000)Google Scholar
  12. 12.
    Stephenson, M., Babb, J., Amarasinghe, S.: Bitwidth analysis with application to silicon compilation. In: Proc. of Programming Language Design and Implementation, Vancouver, Canadap, June 2000, pp. 108–120 (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • John Regehr
    • 1
  • Alastair Reid
    • 1
  • Kirk Webb
    • 1
  1. 1.School of ComputingUniversity of Utah 

Personalised recommendations