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.
|Title of host publication||Formal methods and software engineering|
|Publication status||Published - 2008|
|Event||International Conference on Formal Methods and Software Engineering - Kitakyushu-City, Japan|
Duration: 27 Oct 2008 → 31 Oct 2008
Conference number: 10
|Conference||International Conference on Formal Methods and Software Engineering|
|Period||27/10/08 → 31/10/08|
Bibliographical noteAuthor can archive post-print (ie final draft post-refereeing).
Craciun, F., Qin, S., & Chin, W-N. (2008). A formal soundness proof of region-based memory management for object-oriented paradigm. In Formal methods and software engineering (pp. 126-146). Springer Verlag. https://doi.org/10.1007/978-3-540-88194-0-10