By Atsushi Igarashi and Naoki Kobayashi. Information and Computation, 161:1-44, August 2000.
This material has been published in Information & Computation, 161:1-44, August 2000, the only definitive repository of the content that has been certified and accepted after peer review. Copyright and all rights therein are retained by Academic Press. This material may not be copied or reposted without explicit permission. Copyright © 2000 by Academic Press. You can also find it at International Digital Electronic Library (IDEAL).
A preliminary summary of the title ``Type-based Analysis of Communication for Concurrent Programming Languages,'' appeared in Proceedings of the Fourth International Static Analysis Symposium (SAS'97), Springer LNCS 1302, pages 187-201, September 1997.
Powerful concurrency primitives in recent concurrent languages and thread libraries provide 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 non-trivial code optimization, such as elimination of redundant communication. In order to overcome those problems, advanced type systems for input-only/output-only channels and linear (use-once) channels have been recently studied, but the type reconstruction problem for those type systems remained open, and therefore, their applications to concurrent programming languages have been limited. In this paper, we develop type reconstruction algorithms for variants of Kobayashi, Pierce, and Turner's linear channel type system with Pierce and Sangiorgi's subtyping based on input-only/output-only channel types, and prove correctness of the algorithms. To our knowledge, no complete type reconstruction algorithm has been previously known for those type systems. We have implemented one of the algorithms and incorporated it into the compiler of the concurrent language HACL. This paper also shows some experimental results on the algorithm and its application to compile-time optimizations.
$Date: 2005-12-24 00:37:08 +0900 (Sat, 24 Dec 2005) $