By Atsushi Igarashi. Master's Thesis, Dept. of Information Science, University of Tokyo, February 1997.
We propose a type-based technique to analyze how many times each value, including communication channels, is used during execution of concurrent programs. This work is closely related with the recent work by Kobayashi, Pierce, and Turner on a linear channel system on a process calculus. They introduced a type system that ensures certain channels (called linear channels) to be used just once, and showed that how linear channels help reasoning about program behaviors. However, they only deal with a pure message passing calculus, and more importantly, the type reconstruction problem is left open. This thesis develops a type reconstruction algorithm of a variant of a linear channel type system for a concurrent language with data constructors such as records, and let-polymorphism. We can detect not only linear channels but also other used-once values (closures, records, etc.) by the type reconstruction algorithm. Computational cost of our analysis (excluding cost of ordinary type reconstruction -- which is known exponential in the worst case --) is polynomial in the size of a program. Moreover, several experiments show that our analysis is enough efficient in practice. We also incorporate the proposed analysis into a compiler of a concurrent language HACL and present results of several benchmarks.
$Date: 2005-12-24 00:37:08 +0900 (Sat, 24 Dec 2005) $