Craciun, F. and Qin, S. and Chin, W.-N. (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. Berlin: Springer, pp. 126-146. Lecture notes in computer science. (5256).
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.
|Item Type:||Book chapter|
|Full text:||(AM) Accepted Manuscript|
Download PDF (159Kb)
|Publisher Web site:||http://dx.doi.org/10.1007/978-3-540-88194-0_10|
|Publisher statement:||The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-88194-0_10|
|Record Created:||23 Nov 2009 13:05|
|Last Modified:||31 Mar 2015 12:53|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|