Type-Based Safe Resource Deallocation for Shared-Memory Concurrency

We propose a type system to guarantee safe resource deal-location for shared-memory concurrent programs by extend-ing the previous type system based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are not left allocated when a program ter-minates. Our framework supports (1) fork/join parallelism, (2) synchronization with locks, and (3) dynamically allo-cated 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 algo-rithm