Applications of Strong Moding in Concurrent Logic Programming

并发逻辑程序设计语言GHC（GuardedHornClauses）的突出特点是其通信和同步机制的极端简单性以及在描述并发性方面的灵活性。然而，为了使语言真正实用，静态分析需要在编程和优化中发挥关键作用。首席研究员致力于GHC静态模式系统（强建模）的理论方面，并设计了模式分析的算法。在这个项目中，我们对强建模的实际方面进行了研究，并从以下几个方面证明了它的有效性：1。模式分析器的实现-我们使用KL 1本身作为实现语言，为并发逻辑语言KL 1实现了模式分析器klint。该系统经过多次修改，直到它可以处理大型，现实生活中的程序。强moding下的描述能力-我们通过对各种现实生活中的Eli程序的分析证明，具有强moding的并发逻辑语言与没有强moding的并发逻辑语言一样实用和表达能力。基于强模的程序诊断-强模被证明对于程序错误的静态检测非常有用。我们设计并实现了一套有效的非良模程序错误分析算法。此外，我们提出了一种自动纠错方法，并表明它对于小程序错误非常有效。4.基于强建模的优化-我们证明，通过使用类型和线性信息以及模式信息，可以消除许多运行时操作，如标记检查，从而使性能与过程式程序所获得的性能没有太大差异。

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.