Type-Based Safe Resource Deallocation for Shared-Memory Concurrency

By Kohei Suenaga, Ryota Fukuda and Atsushi Igarashi. To appear in Proceedings of the ACM International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2012), Tucson, AZ, October, 2012.


We propose a type system to guarantee safe resource deallocation for shared-memory concurrent programs by extending the previous type system (Suenaga and Kobayashi 2009) based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are not left allocated when a program terminates. Our framework supports (1) fork/join parallelism, (2) synchronization with spinlocks, and (3) dynamically allocated memory cells and locks. The type system is proved to be sound. We also provide a type inference algorithm for the type system and a prototype implementation of the algorithm.