Abstract
Safe is a first-order eager language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time. The language is aimed at inferring and certifying upper bounds for memory consumption in a Proof Carrying Code environment. Some of its analyses have been presented elsewhere [7,8]. In this paper we present an inference algorithm for annotating programs with regions which is both simpler to understand and more efficient than other related algorithms. Programmers are assumed to write programs and to declare datatypes without any reference to regions. The algorithm decides the regions needed by every function. It also allows polymorphic recursion with respect to regions. We show convincing examples of programs before and after region annotation, prove the correctness and optimality of the algorithm, and give its asymptotic cost.
Work supported by the Ministry of Science grants AP2006-02154, TIN2008-06622-C03-01/TIN (STAMP), and the Madrid Government grant S-0505/TIC/0407 (PROMESAS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aiken, A., Fähndrich, M., Levien, R.: Better static memory management: improving region-based analysis of higher-order languages. In: ACM SIGPLAN Conference on Programming Languages Design and Implementation, PLDI 1995, pp. 174–185. ACM Press, New York (1995)
Birkedal, L., Tofte, M., Vejlstrup, M.: From region inference to von Neumann machines via region representation inference. In: 23rd ACM Symposium on Principles of Programming Languages, POPL 1996, pp. 171–183. ACM Press, New York (1996)
Fluet, M., Morrisett, G., Ahmed, A.: Linear regions are all you need. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 7–21. Springer, Heidelberg (2006)
Henglein, F., Makholm, H., Niss, H.: A direct approach to control-flow sensitive region-based memory management. In: 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP 2001, pp. 175–186. ACM Press, New York (2001)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: 30th ACM Symposium on Principles of Programming Languages, POPL 2003, pp. 185–197. ACM Press, New York (2003)
Makholm, H.: A language-independent framework for region inference. Ph.D thesis, Univ. of Copenhagen, Dep. of Computer Science, Denmark (2003)
Montenegro, M., Peña, R., Segura, C.: A type system for safe memory management and its proof of correctness. In: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2008, pp. 152–162 (2008)
Montenegro, M., Peña, R., Segura, C.: An inference algorithm for guaranteeing safe destruction. In: Hanus, M. (ed.) Logic-Based Program Synthesis and Transformation. LNCS, vol. 5438, pp. 135–151. Springer, Heidelberg (2009)
Montenegro, M., Peña, R., Segura, C.: A simple region inference algorithm for a first-order functional language (extended version). Technical report, SIC-5-09. Dpto. de Sist. Informáticos y Computación. UCM (2009), http://federwin.sip.ucm.es/sic/investigacion/publicaciones/informes-tecnicos
Tofte, M., Birkedal, L.: A region inference algorithm. ACM Transactions on Programming Languages and Systems 20(4), 724–767 (1998)
Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N., Olesen, T.H., Sestoft, P.: Programming with regions in the MLKit (revised for version 4.3.0). Technical report, IT University of Copenhagen, Denmark (2006)
Tofte, M., Hallenberg, N.: Region-Based Memory Management in Perspective. In: Invited talk Space 2001 Work, London, January 2001, pp. 1–8. Imperial College (2001)
Tofte, M., Talpin, J.-P.: Implementing the call-by-value lambda-calculus using a stack of regions. In: 21st ACM Symposium on Principles of Programming Languages, POPL 1994, January 1994, pp. 188–201 (1994)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Montenegro, M., Peña, R., Segura, C. (2010). A Simple Region Inference Algorithm for a First-Order Functional Language. In: Escobar, S. (eds) Functional and Constraint Logic Programming. WFLP 2009. Lecture Notes in Computer Science, vol 5979. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11999-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-11999-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11998-9
Online ISBN: 978-3-642-11999-6
eBook Packages: Computer ScienceComputer Science (R0)