Sciweavers

APLAS
2009
ACM

Fractional Ownerships for Safe Memory Deallocation

13 years 10 months ago
Fractional Ownerships for Safe Memory Deallocation
We propose a type system for a programming language with memory allocation/deallocation primitives, which prevents memory-related errors such as double-frees and memory leaks. The main idea is to augment pointer types with fractional ownerships, which express both capabilities and obligations to access or deallocate memory cells. By assigning an ownership to each pointer type constructor (rather than to a variable), our type system can properly reason about list/tree-manipulating programs. Furthermore, thanks to the use of fractions as ownerships, the type system admits a polynomial-time type inference algorithm, which serves as an algorithm for automatic verification of lack of memoryrelated errors. A prototype verifier has been implemented and tested for C programs.
Kohei Suenaga, Naoki Kobayashi
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where APLAS
Authors Kohei Suenaga, Naoki Kobayashi
Comments (0)