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.

doi:10.1007/978-3-540-88194-0_10

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.

Authors

F. Craciun

S. Qin

W.N. Chin

S. Liu

T. Maibaum

K. Araki.

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). A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm. In Formal methods and software engineering : 10th International Conference on Formal Engineering Methods, ICFEM 2008, 27-31 October 2008, Kitakyushu-City, Japan ; proceedings (126-146). https://doi.org/10.1007/978-3-540-88194-0_10

Conference Name	10th International Conference on Formal Engineering Methods (ICFEM 2008)
Conference Location	Kitakyushu, Japan
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
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