A region inference algorithm

ABSTRACT

Region Inference is a program analysis which infers lifetimes of values. It is targeted at a runtime model in which the store consists of a stack of regions and memory management predominantly consists of pushing and popping regions, rather than performing garbage collection. Region Inference has previously been specified by a set of inference rules which formalize when regions may be allocated and deallocated. This article presents an algorithm which implements the specification. We prove that the algorithm is sound with respect to the region inference rules and that it always terminates even though the region inference rules permit polymorphic recursion in regions. The algorithm is the result of several years of experiments with region inference algorithms in the ML Kit, a compiler from Standard ML to assembly language. We report on practical experience with the algorithm and give hints on how to implement it.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Raph Levien, Better static memory management: improving region-based analysis of higher-order languages, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.174-185, June 18-21, 1995, La Jolla, California, United States
• 2: Maria Virginia Aponte, Extending record typing to type parametric modules with sharing, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.465-478, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158704]
• 3: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 4: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 5: DIJKSTRA, E. W. 1960. Recursive programming. Numerische Math 2, 312-318. Also in Rosen: "Programming Systems and Languages", McGraw-Hill, 1967.
• 6: HALLENBERG, N. 1997. ML Kit test report. (Automatically generated test report; available at http:////www, diku. dk//reseat ch-gr o ups//to p ps//act ivi ties//ki t 2//test. ps).
• 7: R. Harper , R. Milner , M. Tofte, A type discipline for Program modules, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.308-319, March 1987, Pisa, Italy
• 8: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 9: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 10: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.468-476, May 13-17, 1990, Baltimore, Maryland, United States [doi>10.1145/100216.100279]
• 11: LEROY, X. 1992. Typage polymophe d'un language Mgorithmique. Ph.D. thesis, University Paris VII. English version: Polymorphic Typing of an Algorithmic Language, INRIA Research Report no. 1778, October 1992.
• 12: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 13: MILNER, R. 1978. A theory of type polymorphism in programming. J. Computer and System Sciences 17, 348-375.
• 14: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 15: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 16: J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger , P. Naur, Revised report on the algorithm language ALGOL 60, Communications of the ACM, v.6 n.1, p.1-17, Jan. 1963 [doi>10.1145/366193.366201]
• 17: NIELSON, F., NIELSON, H. R., AND AMTOFT, T. 1996. Polymorphic subtyping for effect analysis: the algorithm. Tech. Rep. LOMAPS-DAIMI-16, Department of Computer Science, University of Aarhus (DAIMI). April.
• 18: Hanne Riis Nielson , Flemming Nielson, Higher-order concurrent programs with finite communication topology (extended abstract), Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.84-97, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174538]
• 19: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 20: TALPIN, J.-P. 1993. Theoretical and practical aspects of type and effect inference. Doctoral Dissertation. Also available as Research Report EMP//CRI//A-236, Ecole des Mines de Paris.
• 21: TALPIN, J.-P. AND JOUVELOT, P. 1992a. Polymorphic type, region and effect inference. Journal of Functional Programming 2, 3.
• 22: TALPIN, J.-P. AND JOUVELOT, P. 1992b. The type and effect discipline. In Proceedings of the seventh IEEE Conference on Logic in Computer Science. 162-173. Also, (extended version) technical report EMP//CRI//A-206, Ecole des Mines de Paris, April 1992.
• 23: TOFTE, M. 1988. Operational semantics and polymorphic type inference. Ph.D. thesis, Edinburgh University, Department of Computer Science, Edinburgh University, Mayfield Rd., EH9 3JZ Edinburgh. Available as Technical Report CST-52-88.
• 24: TOFTE, M. AND BIRKEDAL, L. 1996. Unification and polymorphism in region inference. Submitted to the Milner Festschrift. http ://www. diku. dk/users/tofte/publ/milner, ps.
• 25: TOFTE, M., BIRKEDAL, L., ELSMAN, M.,, HALLENBERG, N., OLESEN, T. H., SESTOFT, P., AND BERTELSEN, P. 1997. Programming with regions in the ML Kit. Tech. Rep. DIKU-TR-97/12, Dept. of Computer Science, University of Copenhagen. (http://www.diku.dk/research-groups/ topps / activities/kit 2).
• 26: TOFTE, M. AND TALPIN, J.-P. 1992. Data region inference for polymorphic functional languages (technical summary). Tech. Rep. EMP/CRI/A-229, Ecole des Mines de Paris.
• 27: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 28: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 29: Paul R. Wilson, Uniprocessor Garbage Collection Techniques, Proceedings of the International Workshop on Memory Management, p.1-42, September 17-19, 1992

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Dynamic storage management

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure; Functional constructs

General Terms:
Algorithms, Reliability, Theory

Keywords:
regions, standard ML