Main Contents
Kobayashi's group moved in October, 2004 from Tokyo Institute of Technology to Tohoku University.
This Web page is obsolete. See the new laboratory's page instead.
Research Topics
Type sytems, program analysis, and implementation of programming languages
Introduction
The general goal of our research group is to design and implement programming languages based on solid theoretical foundations. Our particular interests are currently in concurrent/parallel programming languages: in spite of the difficulty of writing and debugging concurrent/parallel programs, little support for them has been provided by concurrent programming languages. Following many successes of theoretical foundations in sequential programming languages (such as lambda-calculus in functional languages), we are trying to establish good principles for design and implementation of concurrent programming languages. We have so far designed and implemented a concurrent programming language HACL and a parallel constraint logic programming language PARCS, and studied several type systems, program analyses, and compilation techniques for those languages. We have also studied a variety of type-based program analysis/transformation techniques, and implented program analysis tools, including a lock usage analyzer and an information flow analyzer for Java bytecode, and a type-based analyzer for the pi-calculus (TyPiCal).
Recent Research Topics (papers)
Linear Types for Concurrent Programming Languages
While communication is one of the most basic features in concurrent programming languages, it is also one of the major sources of bugs and inefficiency of concurrent programs. Our linear type system can improve the safety and efficiency of concurrent programs, by ensuring that certain channels (called linear channels) are used just once. A linear channel can be reclaimed as soon as the communication takes place, reducing memory management overhead particularly in distributed environments. Furthermore, the linearity enables aggressive compiler optimizations (e.g., forwarder elimination, which is a parallel analogue of tail call elimination). A process equivalence theory based on the linear type system has been developed to show the validity of the compiler optimizations. A type inference algorithm has also been developed.
A Type System for Deadlock-freedom
Deadlock and non-determinism are major sources for the difficulty of writing and debugging concurrent programs. They also make static decision of control flows difficult, disabling efficient implementation. We developed a novel static type system that can ensure partial deadlock-freedom and determinacy. In that type system, channels are classified into reliable and unreliable channels: it is statically ensured that reliable channels never cause deadlock and that certain reliable channels never cause non-determinism. Parallel function primitives can be, for example, implemented in the deadlock and deterministic fragment, and many concurrent objects are ensured to be deadlock-free by the type system.
Type Systems for Java Bytecode
A Java program is usually compiled into Java bytecode and then the bytecode is interpreted by the Java Virtual Machine. However, bytecode downloaded through Internet cannot be always trusted and source programs for the bytecode are not always available. Therefore, JVM verifier checks that bytecode does not cause any fatal error before executing bytecode. The present version of the verifier, however, checks only basic properties: It checks that the operands of each instruction are valid, that branch must be within the bounds of the code array for the method, and that the operand stack is always the same size at any program point. We have developed type systems for verifying more sophisticated properties of Java bytecode, and implemented Java bytecode verifiers:
A bytecode verifier for checking usage of Java bytecode lock primitives The Java virtual machine language has primitives to acquire and release a lock on an object. If these primitives are used in a wrong manner, fatal errors (e.g. deadlock) may occur. We have constructed a type system for checking sage usage of lock primitives and implemented a Java bytecode verifier. Our type system can guarantee that when a method terminates it has released all the locks it has acquired and that a method releases a lock only if it has acquired the lock previously. More information is available in this paper.
A bytecode verifier for information flow analysis for Java bytecode.Some bytecode may manipulate secret data like passwords. We have designed a type system for checking that bytecode does not leak information about secret data, and implemented a Java bytecode verifier based on the type system.More information is available in this paper.
Type-based Static Memory Management
We are currently studying two schemes for static memory management (or, compile-time garbage collection): linear types and region inference. Linear type systems guarantee that certain values are used just once at run-time; so, such values can be deallocated immediately after being used, without help of conventional garbage collection. Actually, however, not so many values are judged to be linear by traditional linear type systems, hence their applications have been rather limited. In order to overcome this limitation, we developed a new variant of linear type system, called a quasi-linear type system. More information is available here. In parallel to the development of the quasi-linear type system, we have been working on integration of region-based memory management with conventional garbage collection. The main difficulty was that the region-based memory management may create dangling pointers. We overcame it by using region/type information at garbage collection time. On this topic, only a paper written in Japanese is available right now.
Computation Model Based on Linear Logic
Basic computation models are important for good design and implementation of programming languages. We have proposed a concurrent linear logic programming framework called HACL, based on the view ``computation = controlled deduction in linear logic.'' HACL is a rather low level model for concurrent computation, but it has been shown that it can also serve as a basis for higher-level computation models like concurrent object-oriented computation; therefore, HACL can be used as a common basis for studying types systems, program analyses, and implementation techniques of concurrent programming languages. A concurrent programming language HACL was designed and implemented based on the framework. It can be considered an ML extended with primitives for parallel execution, dynamic creation of first-class communication channels, and asynchronous communication over those channels.
Type-Directed Compilation for Concurrent Programming Languages
Types have been playing a great role in many advanced compilation techniques for modern sequential programming languages. We have shown that types are also very useful for implementation of concurrent programming languages, particularly for optimizations of communication. The proposed technique enables (almost) tag-free communication of high-level data in distributed environments. It has been incorporated in the distributed implementation of HACL.