Abstract
In this work we address the problem of proving, by static analysis means, that allocating and deallocating regions in the store provides a safe way to achieve memory management. That is, the goal is to provably ensure that a program does not use pointers into a deallocated region. A well-known approach to this problem is the one of Tofte and Talpin. Our first contribution is to provide a simple proof, by means of a subject reduction property, of type safety for their region calculus. Our second, main contribution is that we actually do this for an extension of Tofte-Talpin’s calculus, featuring a primitive construct for deallocating regions, similar to C’s free, that allows one to circumvent the strict stack-of-regions discipline enforced in Tofte-Talpin’s calculus. Our static analysis consists in a novel type and effect system, extending the one of Tofte and Talpin, where we record deallocation effects.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Aiken, A., Fähndrich, M., Levien, R.: Better static memory management: improving region-based analysis of higher-order languages. In: PLDl 1995, pp. 174–185 (1995)
Banerjee, A., Heintze, N., Riecke, J.: Region analysis and the polymorphic lambda-calculus. In: LICS 1999, pp. 88–97 (1999)
Birkedal, L., Tofte, M., Vejlstrup, M.: From region inference to von Neumann machines via region representation inference. In: POPL 1996, pp. 171–183 (1996)
Calcagno, C.: Stratified operational semantics for safety and correctness of the region calculus. In: POPL 2001, pp. 155–165 (2001)
Calcagno, C., Helsen, S., Thiemann, P.: Syntactic type soundness results for the region calculus. Information and Computation 173(2), 199–221 (2002)
Dal Zilio, S., Gordon, A.: Region analysis and a π-calculus with groups. J. of Functional Programming 12(3), 229–292 (2002)
Fähndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI 2002, pp. 13–24 (2002)
Fluet, M., Morrisett, G., Ahmed, A.: Linear regions are all you need. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)
Gay, D., Aiken, A.: Memory management with explicit regions. In: PLDI 1998, pp. 313–323 (1998)
Gay, D., Aiken, A.: Language support for regions. In: PLDI 2001, pp. 70–80 (2001)
Helsen, S., Thiemann, P.: Syntactic type soundness for the region calculus. HOOTS 2000, ENTCS 41(3), 1–19 (2001)
Henglein, F., Makholm, H., Niss, F.: A direct approach to control-flow sensitive region-based memory management. In: PPDP 2001, pp. 175–186 (2001)
Henglein, F., Makholm, H., Niss, F.: Effect Types and Region-Based Memory Management. In: Pierce, B.C. (ed.) Chap. 3 of Advanced Topics in Types and Programming Languages, pp. 87–135. MIT Press, Cambridge (2005)
Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL 1988, pp. 47–57 (1988)
Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value λ-calculus using a stack of regions. In: POPL 1994, pp. 188–201 (1994)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N.: A retrospective on region-based memory management. HOSC 17(2), 245–265 (2004)
Walker, D., Crary, K., Morrisett, G.: Typed memory management via static capabilities. TOPLAS 22(4), 701–771 (2000)
Walker, D., Watkins, K.: On regions and linear types. In: ICFP 2001, pp. 181–192 (2001)
Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boudol, G. (2008). Typing Safe Deallocation. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)