A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm

Craciun, F.; Qin, S.; Chin, W.N.; Liu, S.; Maibaum, T.; Araki., K.

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.

Citation

Craciun, F., Qin, S., Chin, W., Liu, S., Maibaum, T., & Araki., K. (2008, October). A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm. Presented at 10th International Conference on Formal Engineering Methods (ICFEM 2008), Kitakyushu, Japan

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 10th International Conference on Formal Engineering Methods (ICFEM 2008)
• Start Date: Oct 27, 2008
• End Date: Oct 31, 2008
• Publication Date: Oct 1, 2008
• Deposit Date: Nov 23, 2009
• Publicly Available Date: Dec 10, 2009
• Print ISSN: 0302-9743
• Pages: 126-146
• Series Title: Lecture notes in computer science
• Series Number: 5256
• Series ISSN: 0302-9743,1611-3349
• Book Title: Formal methods and software engineering : 10th International Conference on Formal Engineering Methods, ICFEM 2008, 27-31 October 2008, Kitakyushu-City, Japan ; proceedings.
• ISBN: 9783540881933
• DOI: https://doi.org/10.1007/978-3-540-88194-0_10
• Public URL: https://durham-repository.worktribe.com/output/1160898