Abstract
Region-based memory management has been proposed as a viable alternative to garbage collection for real-time applications and embedded software. In our previous work we have developed a region type inference algorithm that provides an automatic compile-time region-based memory management for object-oriented paradigm. In this work we present a formal soundness proof of the region type system that is the target of our region inference. More precisely, we prove that the object-oriented programs accepted by our region type system achieve region-based memory management in a safe way. That means, the regions follow a stack-of-regions discipline and regions deallocation never create dangling references in the store and on the program stack. Our contribution is to provide a simple syntactic proof that is based on induction and follows the standard steps of a type safety proof. In contrast the previous safety proofs provided for other region type systems employ quite elaborate techniques.
The work is supported in part by the EPSRC project EP/E021948/1.
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.
Similar content being viewed by others
References
Bacon, D.F., Cheng, P., Rajan, V.T.: A real-time garbage collector with low overhead and consistent utilization. In: POPL, pp. 285–298 (2003)
Birkedal, L., Tofte, M.: A constraint-based region inference algorithm. Theoretical Computer Science 258(1–2), 299–392 (2001)
Bollella, G., Brosgol, B., Dibble, P., Furr, S., Gosling, J., Hardin, D., Turnbull, M.: The Real-Time Specification for Java. Addison-Wesley, Reading (2000)
Boudol, G.: Typing safe deallocation. In: European Symposium on Programming (ESOP), pp. 116–130 (2008)
Boyapati, C., Salcianu, A., Beebee, W., Rinard, M.: Ownership Types for Safe Region-Based Memory Management in Real-Time Java. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 324–337 (2003)
Calcagno, C.: Stratified operational semantics for safety and correctness of the region calculus. In: ACM Symposium on Principles of Programming Languages (POPL), 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)
Chin, W.-N., Craciun, F., Qin, S., Rinard, M.C.: Region inference for an object-oriented language. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 243–254 (2004)
Christiansen, M.V., Velschow, P.: Region-Based Memory Management in Java. Master’s Thesis, Department of Computer Science (DIKU), University of Copenhagen (1998)
Craciun, F., Goh, H.Y., Chin, W.-N.: A framework for object-oriented program analyses via Core-Java. In: IEEE International Conference on Intelligent Computer Communication and Processing (ICCP), Cluj-Napoca, Romania, pp. 197–205 (2006)
Craciun, F., Qin, S., Chin, W.-N.: A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm. Technical report, Department of Computer Science, Durham University, UK (April 2008), http://www.durham.ac.uk/shengchao.qin/papers/reg_cal_proof.pdf
Elsman, M.: Garbage collection safety for region-based memory management. In: ACM Workshop on Types in Language Design and Implementation (TLDI), pp. 123–134 (2003)
Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-Based Memory Management in Cyclone. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 282–293 (2002)
Helsen, S.: Region-Based Program Specialization. PhD thesis, Universität Freiburg (2002)
Helsen, S., Thiemann, P.: Syntactic type soundness for the region calculus. Electronic Notes in Theoretical Computer Science 41(3) (2000)
Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 132–146 (1999)
Morrisett, G.: Compiling with Types. PhD thesis, Carnegie Mellon University (1995)
Morrisett, J.G., Felleisen, M., Harper, R.: Abstract Models of Memory Management. In: ACM Conference Conference on Functional Programming Languages and Computer Architecture (FPCA), pp. 66–77 (1995)
Niss, H.: Regions are imperative. Unscoped regions and control-sensitive memory management. PhD thesis, University of Copenhagen (2002)
Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)
Tofte, M., Birkedal, L.: A region inference algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS) 20(4), 734–767 (1998)
Tofte, M., Talpin, J.: Implementing the Call-By-Value λ-calculus Using a Stack of Regions. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 188–201 (1994)
Tofte, M., Talpin, J.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Wilson, P.R.: Uniprocessor garbage collection techniques. In: International Workshop on Memory Management (IWMM), pp. 1–42 (1992)
Wright, A.K., Felleisen, M.: A Syntactic Approach to Type Soundness. Information Computation 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Craciun, F., Qin, S., Chin, WN. (2008). A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm. In: Liu, S., Maibaum, T., Araki, K. (eds) Formal Methods and Software Engineering. ICFEM 2008. Lecture Notes in Computer Science, vol 5256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88194-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-88194-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88193-3
Online ISBN: 978-3-540-88194-0
eBook Packages: Computer ScienceComputer Science (R0)