The VLISP verified PreScheme compiler

This paper describes a verified compiler for PreScheme, the implementation language for thevlisp run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that translates the core language into a combinator-based tree-manipulation language, and a linearizer that translates combinator code into code for an abstract stored-program machine with linear memory for both data and code. This factorization enabled different proof techniques to be used for the different phases of the compiler, and also allowed the generation of good code. Finally, the whole process was made possible by carefully defining the semantics ofvlisp PreScheme rather than just adopting Scheme's. We believe that the architecture of the compiler and its correctness proof can easily be applied to compilers for languages other than PreScheme.This work was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001, through the MITRE Corporation, and by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603. Author's current address: Department of Computer Science and Engineering, Oregon Graduate Institute, P.O. Box 91000, Portland, OR 97291-1000.The work reported here was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation.This work was supported by Rome Laboratory of the United States Air Force, contract No. F19628-89-C-0001, through the MITRE Corporation, and by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603.     

Action semantics-directed prototyping

We present a methodology for compiler synthesis based on Mosses-Watt's action semantics. Each action in action semantics notation is assigned specific “analysis functions”, such as a typing function and a binding-time function. When a language is given an action semantics, the typing and binding-time functions for the individual actions compose into typing and binding-time analyses for the language; these are implemented as the type checker and static semantics processor, respectively, in the synthesized compiler. Other analyses can be similarly formalized and implemented. We show a sample language semantics and its synthesized compiler, and we describe the compiler synthesizer that we have developed.     

EFFECTIVE PARALLELIZATION TECHNIQUES FOR LOOP NESTS WITH NON-UNIFORM DEPENDENCES

The parallelism of loop nests with non-uniform dependences is difficult to extract and ineffectively explored by the existing parallelization schemes. In this paper, we propose new efficient techniques in extracting parallelism of loop nests with non-uniform dependences using their irregularity. By this way, current highly parallel multiprocessor systems such as multithreaded and clustering multiprocessor systems can be fully utilized. These four mechanisms are (a) parallelization part splitting, (b) partial parallelization decomposition, (c) irregular loop interchange and (d) growing pattern detection. They explore parallelisms of special parallel patterns for nested loops with non-uniform dependences. The loop transformations used in uniform loops are also applied in non-uniform dependence loops after legality tests. We apply the results of classical convex theory and detect special parallel patterns of dependence vectors. We also proposed an algorithm that combines above mechanisms to enhance parallelism. We demonstrate that our technique gives much better speedup and extracts more parallelism than the existing techniques. Thus, we are encouraged by these apparent enhancements to pursue further development.     

基于MYGCC的编程规则检查算法研究

MYGCC是一个编程规则检查工具,其目前的检查算法存在局限性,不能完整地展示违反编程规则的程序路径。本文提出并实现了一种改进的编程规则检查算法,可以弥补上述的局限性。实验表明改进算法是有效的,此改进有助于用户更准确地定位错误位置,方便对编程错误的修正。     

编译原理中项目集规范族的分析与研究

LR分析法是一种应用较广泛的语法分析方法,项目集规范族是构造LR分析表的基础.本文将词法分析方法与语法分析方法联系起来,以有限自动机知识为基础,给出了一种基于自动机的构造项目集规范族的方法,然后,给出了一种更简洁的方法,并比较了两种方法的异同.     

即时编译器中的代码消极生成机制

提出一种应用于即时编译器中的代码生成优化技术——代码消极生成机制,结合Intel微处理器研究院的XORP虚拟机对该项技术进行了阐述。介绍了XORP中实现的其他轻量级优化算法,并采用EEMBC对不同虚拟机和不同优化进行了科学评估。采用该项技术的XORP虚拟机的运行速度为KVM的15倍以上,超过其他商用高性能虚拟机。     

基于开放编译的面向对象程序静态分析器*

采用反射和开放编译技术,设计并实现了一个面向对象程序静态分析器,对开放编译器OpenC++进行了扩展与改进。通过实验研究表明,该程序静态分析器可以得到全面的系统依赖信息,可以有效地辅助程序理解。     

用JavaCC和JJTree构造扩展模式文档解析器

XML正成为互联网中数据表示和数据交换的标准。扩展DTD支持面向XML的查询,但结构复杂,现有工具无法解析扩展DID,获取元素之间的面向对象信息。利用JavaCC和JJTree设计解析器,包括构造语法和语义分析器,设计扩展DTD的语法规则和解析器的类结构,从而解析扩展DTD,利用解析后的扩展DTD的语法树获取面向对象信息,方便高效,不仅支持XML存储建立,而且支持面向对象XML查询方式,使得查询方式更为灵活多样。     

Loop headers in λ-calculus or CPS

The introduction of a loop header block facilitates the hoisting of loop-invariant code from a loop. In a -calculus intermediate representation, which has a notion of scope, this transformation is particularly useful. Loop headers with scope also solve a problem with in-line expansion of recursive functions or loops: if done naively, only the first iteration is inlined. A loop header can encapsulate the loop or recursion for better in-line expansion. This optimization improves performance by about 5% in Standard ML of New Jersey.