Skip to main content
SpringerLink
Log in

Inserting Safe Memory Reuse Commands into ML-Like Programs

  • Conference paper
  • First Online:
Static Analysis (SAS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2694))

Included in the following conference series:

Abstract

We present a static analysis that estimates reusable memory cells and a source-level transformation that adds explicit memory-reuse commands into the program text. For benchmark ML programs, our analysis and transformation achieves the memory reuse ratio from 5.2% to 91.3%. The small-ratio cases are for programs that have too prevalent sharings among memory cells. For other cases, our experimental results are encouraging in terms of accuracy and cost. Major features of our analysis are: (1) poly-variant analysis of functions by parameterization for the argument heap cells; (2) use of multiset formulas in expressing the sharings and partitionings of heap cells; (3) deallocations conditioned by dynamic flags that are passed as extra arguments to functions; (4) individual heap cell as the granularity of explicit memory-free. Our analysis and transformation is fully automatic.

This work is supported by Creative Research Initiatives of the Korean Ministry of Science and Technology.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. David Aspinall and Martin Hofmann. Another type system for in-place update. In Proceedings of the European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 36–52, April 2002.

    Google Scholar 

  2. Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579–612, 1995.

    MathSciNet  Google Scholar 

  3. Bruno Blanchet. Escape analysis: Correctness proof, implementation and experimental results. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 25–37, 1998.

    Google Scholar 

  4. Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 262–275, January 1999.

    Google Scholar 

  5. David Gay and Alex Aiken. Language support for regions. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages 70–80, June 2001.

    Google Scholar 

  6. Ovidiu Gheorghioiu, Alexandru Sălcianu, and Martin Rinard. Interprocedural compatibility analysis for static object preallocation. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 273–284, January 2003.

    Google Scholar 

  7. Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in Cyclone. In Proceedings of the ACM Conference on Programming Language Design and Implementation, June 2002.

    Google Scholar 

  8. Williams L. Harrison III. The interprocedural analysis and automatic parallelization of scheme programs. Lisp and Symbolic Computation, 2(3/4):179–396, 1989.

    Article  Google Scholar 

  9. Samin Ishtiaq and Peter O’Hearn. BI as an assertion language for mutable data structures. In Proceedings of the ACM Symposium on Principles of Programming Languages, January 2001.

    Google Scholar 

  10. Naoki Kobayashi. Quasi-linear types. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 29–42, 1999.

    Google Scholar 

  11. Oukseh Lee. A correctness proof on an algorithm to insert safe memory reuse commands. Tech. Memo. ROPAS-2003-19, Research On Program Analysis System, Korea Advanced Institute of Science and Technology, February 2003. http://ropas.kaist.ac.kr/memo.

    Google Scholar 

  12. Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system release 3.04. Institut National de Recherche en Informatique et en Automatique, December 2001. http://caml.inria.fr.

    Google Scholar 

  13. Yosuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 271–283, January 1996.

    Google Scholar 

  14. Markus Mohnen. Efficient compile-time garbage collection for arbitrary data structures. In Proceedings of Programming Languages: Implementations, Logics and Programs, volume 982 of Lecture Notes in Computer Science, pages 241–258. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  15. nML programming language system, version 0.92a. Research On Program Analysis System, Korea Advanced Institute of Science and Technology, March 2002. http://ropas.kaist.ac.kr/n.

    Google Scholar 

  16. Peter O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In The Proceedings of Computer Science and Logic, pages 1–19, 2001.

    Google Scholar 

  17. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, July 2002.

    Google Scholar 

  18. Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Proceedings of the European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366–382, March/April 2000.

    Google Scholar 

  19. The Standard ML of New Jersey, version 110.0.7. Bell Laboratories, Lucent Technologies, October 2000. http://cm.bell-labs.com/cm/cs/what/smlnj.

    Google Scholar 

  20. Mads Tofte and Lars Birkedal. A region inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):734–767, July 1998.

    Article  Google Scholar 

  21. Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld Olesen, and Peter Sestoft. Programming with regions in the ML Kit (for version 4). IT University of Copenhagen, April 2002. http://www.it-c.dk/research/mlkit.

    Google Scholar 

  22. Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 188–201, 1994.

    Google Scholar 

  23. Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  24. David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In International Conference on Functional Programming and Computer Architecture, pages 25–28, June 1995.

    Google Scholar 

  25. Philip Wadler. Linear types can change the world! In Programming Concepts and Methods. North Holland, April 1990.

    Google Scholar 

  26. David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, volume 2071 of Lecture Notes in Computer Science, pages 177–206, September 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science/ Research On Program Analysis System, Korea Advanced Institute of Science and Technology, Korea

    Oukseh Lee, Hongseok Yang & Kwangkeun Yi

Authors
  1. Oukseh Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hongseok Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kwangkeun Yi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. École Polytechnique, STIX, 91128, Palaiseau cedex, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lee, O., Yang, H., Yi, K. (2003). Inserting Safe Memory Reuse Commands into ML-Like Programs. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-44898-5_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40325-8

  • Online ISBN: 978-3-540-44898-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation