Mads Tofte
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.
- AIKEN, A., FAHNDRICH, iV{., AND LEVIEN, R. 1995. Better static memory management: Improving region-based analysis of higher-order languages. In Proc. of the A CM SIGPLAN '95 Conference on Programming Languages and Implementation (PLDI). ACM Press, La Jolla, CA, 174-185. Google Scholar
Digital Library
- APONTE, iV{. V. 1993. Extending record typing to type parametric modules with sharing. In Proc. of the 20th Annual A CM SIGPLAN-SIGA CT Symposium on Principles of Programming Languages (POPL). ACM Press, 465-478. Google ScholarDigital Library
- BIRKEDAL, L., TOFTE, ~/{., AND VEJLSTRUP, ~/{. 1996. From region inference to yon Neumann machines via region representation inference. In Proceedings of the 23rd ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages. ACM Press, 171-183. Google ScholarDigital Library
- DAMAS, L. AND iV{ILNER, R. 1982. Principal type schemes for functional programs. In Proc. 9th Annual A CM Syrup. on Principles of Programming Languages. 207-212. Google ScholarDigital Library
- DIJKSTRA, E. W. 1960. Recursive programming. Numerische Math 2, 312-318. Also in Rosen: "Programming Systems and Languages", McGraw-Hill, 1967.Google ScholarDigital Library
- 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).Google Scholar
- HARPER, R., iV{ILNER, R., AND TOFTE, iV{. 1987. A type discipline for program modules. In Proc. Int'l Joint Conf. on Theory and Practice of Software Development (TAPSOFT). Springer- Verlag, 308-319. Lecture Notes in Computer Science, Vol. 250. Google ScholarDigital Library
- HENGLEIN, F. 1993. Type inference with polymorphic recursion. ACM Transactions on Programruing Languages and Systems 15, 2 (April), 253. Google ScholarDigital Library
- JOUVELOT, P. AND GIFFORD, D. 1991. Algebraic reconstruction of types and effects. In Proceedings of the 18th A CM Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- KFOURY, A., TIURYN, J., AND URZYCZYN, P. 1990. The undecidability of the semi-unification problem. In Proc. 22nd Annual A CM Syrup. on Theory of Computation (STOC), Baltimore, Maryland. 468-476. Google ScholarDigital Library
- 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.Google Scholar
- LUCASSEN, J. AND GIFFORD, D. 1988. Polymorphic effect systems. In Proceedings of the 1988 A CM Conference on Principles of Programming Languages. Google ScholarDigital Library
- MILNER, R. 1978. A theory of type polymorphism in programming. J. Computer and System Sciences 17, 348-375.Google ScholarCross Ref
- MILNER, R., TOFTE, iV{., HARPER, R., AND iV{ACQUEEN, D. 1997. The Definition of Standard ML (Revised). MIT Press. Google ScholarDigital Library
- MYCROFT, A. 1984. Polymorphic type schemes and recursive definitions. In Proc. 6th Int. Conf. on Programming, LNCS 167. Google ScholarDigital Library
- NAUR, P. 1963. Revised report on the algorithmic language Algol 60. Comm. ACM 1, 1-17. Google ScholarDigital Library
- 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.Google Scholar
- NIELSON, H. R. AND NIELSON, F. 1994. Higher-order concurrent programs with finite communication topology. In Conference Record of POPL'94: 21st A CM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 84-97. Google ScholarDigital Library
- RI~MY, D. 1989. Typechecking records and variants in a natural extension of ML. In Proc. 16th Annual A CM Syrup. on Principles of Programming Languages. ACM, 77-88. Google ScholarDigital Library
- 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.Google Scholar
- TALPIN, J.-P. AND JOUVELOT, P. 1992a. Polymorphic type, region and effect inference. Journal of Functional Programming 2, 3.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google Scholar
- 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.Google Scholar
- 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).Google Scholar
- 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.Google Scholar
- TOFTE, M. AND TALPIN, J.-P. 1994. Implementing the call-by-value lambda-calculus using a stack of regions. In Proceedings of the 21st A CM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 188-201. Google ScholarDigital Library
- TOFTE, M. AND TALPIN, J.-P. 1997. Region-based memory management. Information and Computation 132, 2, 109-176. Google ScholarDigital Library
- WILSON, P. R. 1992. Uniprocessor garbage collection techniques. In Memory Management, Proceedings, International Workshop IWMM92, Y. Bekkers and J. Cohen, Eds. Springer-Verlag, Berlin, 1-42. Google ScholarDigital Library
Index Terms
- A region inference algorithm
Recommendations
From region inference to von Neumann machines via region representation inference
POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesRegion Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference uses a stack of regions, each of which can contain an ...
Combining region inference and garbage collection
This paper describes a memory discipline that combines region-based memory management and copying garbage collection by extending Cheney's copying garbage collection algorithm to work with regions. The paper presents empirical evidence that region ...
Combining region inference and garbage collection
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementationThis paper describes a memory discipline that combines region-based memory management and copying garbage collection by extending Cheney's copying garbage collection algorithm to work with regions. The paper presents empirical evidence that region ...
Comments