Applications of Strong Moding in Concurrent Logic Programming

GHC(Guarded Horn子句)等并发逻辑编程语言的突出特点是其通信和同步机制极其简单，并且在描述并发性方面具有灵活性。然而，为了使语言真正实用，静态分析需要在编程和优化中发挥关键作用。首席研究员对GHC静态模式系统(强建模)的理论方面进行了研究，并设计了模式分析的算法。在这个项目中，我们致力于强建模的实践方面，并从以下几个方面论证了它的有效性：1.模式分析器的实现--我们使用并发逻辑语言KL1本身作为实现语言来实现模式分析器KLINT。该系统经过了多次修改，直到它能够处理大型的、真实的程序。强模式化下的描述能力--通过对各种实际ELI程序的分析，我们证明了具有强模式化的并发逻辑语言与没有强模式化的并发逻辑语言一样具有实用性和表现力。基于强修改-强修改的程序诊断对于程序错误的静态检测是非常有用的。我们设计并实现了一套算法来高效地分析非良好模式程序的错误。此外，我们还提出了一种自动纠错的方法，并证明了该方法对小程序错误有很好的效果。基于强修改的优化-我们演示了，除了模式信息之外，通过使用类型和线性信息，可以消除许多运行时操作，如标记检查，从而使性能与过程程序获得的性能差别不大。

The outstanding features of concurrent logic programming languages such as GHC (Guarded Horn Clauses) are the extreme simplicity of its communication and synchronization mechanisms and its flexibility in describing concurrency. To make the languages really practical, however, static analysis needs to play key roles both in programming and optimization.The head investigator had worked on the theoretical aspects of the static mode system (strong moding) for GHC and designed the algorithms for mode analysis. In this project, we worked on the practical aspects of strong moding and demonstrated its effectiveness from the following respects :1. Implementation of a mode analyzer - We implemented the mode analyzer klint for the concurrent logic language KL1 using KL1 itself as an implementation language. The system was revised several times until it could process large, real-life programs.2. Descriptive power under strong moding - We demonstrated, through the analysis of various real-life Eli programs, that concurrent logic languages with strong moding are as practical and expressive as those without strong moding.3. Program diagnosis based on strong moding - Strong moding turned out to be extremely useful for the static detection of program errors. We designed and implemented a set of algorithms for analyzing the errors of non-well-moded programs efficiently. Furthermore, we proposed a method of automated error correction and showed that it worked quite well for small program errors.4. Optimization based on strong moding - We demonstrated that, by using type and linearity information in addition to mode information, many of runtime operations such as tag checking could be eliminated, leading to performance not too different from that obtained by procedural programs.