Type-based Analysis of Communication for Concurrent Programming Languages

Powerful concurrency primitives in recent concurrent languages and thread libraries provide the great flexibility about implementation of high-level features like concurrent objects. However, they are so low-level that they often make it difficult to check global correctness of programs or to perform aggressive code optimization. We propose a static analysis method for inferring how many times each communication channel is used during execution of concurrent programs: a type system that is sensitive to usage information is constructed for this purpose and a type reconstruction algorithm is developed. Our analysis can, in particular, automatically detect linear channels (communication channels used just once): as studied by Kobayashi, Pierce, and Turner, they are very useful for reasoning about program behavior and aggressive code optimization. Our analysis has already been implemented and applied to the compiler of a concurrent language HACL; we present the results of simple benchmarks..