基于类型注解的认证编译器设计与实现

基于类型注解的认证编译器是安全策略系统的核心部件，它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intel x86／linux汇编语言程序，而且还可以根据类型安全策略的要求产生带注解的汇编程序．实验结果表明，新设计的认证编译器可实现：①类型安全的C语言子集的编译；②许多标准的局部优化；③可以对数组运行时越界操作进行检查．由于安全策略系统的证明是建立在含注解的代码基础之上的，因此，该认证编译器在移动代码安全检查中非常有用。     

一种出具证明编译器中的汇编级断言和证明生成的方法

携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.     

基于提示的移动代码安全检查

基于语言内部安全机制能够有效地保证移动代码的安全执行，其思想是要在移动代码中附加详细且足够的满足安全策略检查的注解信息．基于提示的移动代码的安全检查，克服了目前PCC存在的验证条件必须回送和证明长度过于庞大等缺陷，从而获得了更佳的代码安全检查性能．     

并行编译中对维内通信的通信优化

代码生成作为并行编译器的后端,其生成代码的优劣直接影响着并行程序的执行效率。并行分解的维内存在偏移会产生维内通信,传统算法生成的维内通信代码不够精确,会产生冗余通信。提出了通过合并数组变量生成通信链,并按照通信链生成通信代码的维内通信优化算法来消除此类冗余,对传统算法进行了改进和优化。测试结果表明该算法对维内通信的优化效果明显。     

程序自动并行化中的数组终写关系分析

在程序自动并行化中过程中,数据收集阶段可能产生冗余通信,该文利用数组终写关系分析的方法来消除冗余通信,实现嵌套循环中数组数据最后写关系的快速求解,并将结果提供给编译器后端,生成精确数据收集代码。描述数组终写关系的研究目的和内容,将所处理的嵌套循环根据其结构特征进行分类,给出实现算法的过程。测试结果证明了该算法的正确性和高效性,所产生的精确数据收集代码能够有效地消除部分冗余通信,从而优化和提高了并行化程序的性能。     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

编译原理——C教学编译器设计

该文根据目前编译原理的教学现状,设计了一个C教学编译器。它是一个基于Windows平台的编译器,不但能全面体现编译器的设计和实现过程而且还采用了教学上新的算法和结构设计思想。如基于需要给标识符分配空间、半缓冲区的应用,分离哈希链表的设计。同时,编译器在生成目标代码时,先生成虚拟机代码,再对虚拟机代码进行解释执行得出最终运行结果。这样就便于在不同目标机器上移植了。此技术在Java上已经广泛应用,但在C语言上还是尝试。     

基于重排序变换和循环分布的通信优化算法

针对现有通信优化算法无法使MPI自动并行化编译器生成加速比理想的消息传递程序问题,提出了一种基于重排序变换和循环分布的通信优化算法。该算法根据给出的过程间副作用集合和基于mpi_wait/mpi_irecv移动的重排序变换规则,有序地采用重排序变换和循环分布,尽可能安全地扩大点到点非阻塞通信中通信与计算的重叠窗口,使MPI自动并行化编译器生成具有更多计算重叠通信的消息传递代码。实验结果表明,该算法能够隐藏更多的点到点非阻塞通信开销,并且明显提升消息传递程序的加速比。     

基于Itanium处理器的密码算法实现

使用ItaniumCompiler7.0编译器对现有分组密码算法的C语言实现进行编译得到汇编代码,在对这些汇编代码进行分析时可以发现编译器并没有充分利用Itanium处理器提供的资源。针对这一问题,该文提出了在Itanium处理器上有效实现常用密码算法的方法,主要是利用Itanium处理器指令集中提供的SIMD指令提高处理的并行性,并探讨了Itanium处理器SIMD指令的使用方法。     

MPI通信代码自动生成算法

对于高性能并行计算机而言，如何由给出的计算、数据划分信息及精确数组数据流分析信息自动生成并行化代码是实现串行程序并行化的一个重要问题。根据Saman P.Amarasinghe和Lam的定理，实现了一种并行化识别工具中MPI（Message Passing Interface）并行化代码自动生成技术的算法，并对该算法的性能进行分析。     

Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certificate that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both fast and verifiably safe. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.     

A pointer logic and certifying compiler

Proof-Carrying Code brings two big challenges to the research field of programming languages. One is to seek more expressive logics or type systems to specify or reason about the properties of low-level or high-level programs. The other is to study the technology of certifying compilation in which the compiler generates proofs for programs with annotations. This paper presents our progress in the above two aspects. A pointer logic was designed for PointerC (a C-like programming language) in our research. As an extension of Hoare logic, our pointer logic expresses the change of pointer information for each statement in its inference rules to support program verification. Meanwhile, based on the ideas from CAP (Certified Assembly Programming) and SCAP (Stack-based Certified Assembly Programming), a reasoning framework was built to verify the properties of object code in a Hoare style. And a certifying compiler prototype for PointerC was implemented based on this framework. The main contribution of this paper is the design of the pointer logic and the implementation of the certifying compiler prototype. In our certifying compiler, the source language contains rich pointer types and operations and also supports dynamic storage allocation and deallocation.     

A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.     

Automatic generation of self-scheduling programs

Techniques are described for the automatic generation of self-scheduling parallel programs. Both scheduling algorithms and the concurrent components of applications are expressed in a high-level concurrent language. Partitioning and data dependency information are expressed by simple control statements, which may be generated either automatically or manually. A self-scheduling compiler, implemented as a source-to-source transformation, takes application code, control statements, and scheduling routines and generates a new program that can schedule its own execution on a parallel computer. The approach has several advantages compared to previous proposals. It generates programs that are portable over a wide range of parallel computers. There is no need to embed special control structures in application programs. The use of a high-level language to express applications and scheduling algorithms facilitates the development, modification, and reuse of parallel programs     

一种用于Java程序验证编译的标签类型

在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的Java程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现Java程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的Java字节码即时编译器中.     

A constraint-weaving approach to points-to analysis for AspectJ

Points-to analysis is a static code analysis technique that establishes the relationships between variables of references and allocated objects. A number of points-to analysis algorithms have been proposed for procedural and object-oriented languages like C and Java, while few of them can be used for AspectJ as we know so far. One main reason is that AspectJ is an aspect-oriented language which implements the separation of crosscutting concerns by advices, pointcuts, and inter-type declarations, while a points-to analysis of AspectJ programs may be imprecise because any aspect woven into the base code may change the points-to relations in the program and thus a conservative analysis has to be taken in order to handle the aspects. In this paper, we propose a context-sensitive points-to analysis technique called AJPoints for AspectJ. Similar to the weaving mechanism for AspectJ, AJPoints obtains the constraints and templates on the points-to relations for the base code and the aspects, respectively, but weaves and solves them in an iterative manner in order to cross the boundary between the base code and the aspects. We have implemented AJPoints on abc AspectJ compiler and evaluated it by using twelve AspectJ benchmark programs. The experimental results show that our technique can achieve a high precision about points-to relations in AspectJ programs.     

Optimizing OpenMP Programs on Software Distributed Shared Memory Systems

This paper describes compiler techniques that can translate standard OpenMP applications into code for distributed computer systems. OpenMP has emerged as an important model and language extension for shared-memory parallel programming. However, despite OpenMP's success on these platforms, it is not currently being used on distributed system. The long-term goal of our project is to quantify the degree to which such a use is possible and develop supporting compiler techniques. Our present compiler techniques translate OpenMP programs into a form suitable for execution on a Software DSM system. We have implemented a compiler that performs this basic translation, and we have studied a number of hand optimizations that improve the baseline performance. Our approach complements related efforts that have proposed language extensions for efficient execution of OpenMP programs on distributed systems. Our results show that, while kernel benchmarks can show high efficiency of OpenMP programs on distributed systems, full applications need careful consideration of shared data access patterns. A naive translation (similar to OpenMP compilers for SMPs) leads to acceptable performance in very few applications only. However, additional optimizations, including access privatization, selective touch, and dynamic scheduling, resulting in 31% average improvement on our benchmarks.     

基于确认式编译技术的移动代码安全性研究

应用确认式编译技术解决移动代码的安全性问题是国际上新近开始研究的方法，其最大特点是把确保满足安全策略的主要任务由代码消费方转移到代码生产方，可以有效解决代码消费方运行时负担过重的问题；此外，它是对代码本身进行验证，而不是对代码产生方的身份进行验证，因而可信度更高并可以支持匿名代码。本文对该研究技术进行了分析，从中可了解到：支持更高级别的安全性是这种技术获得更广泛应用的焦点；并针对这种需求，在该文中穿插介绍了我们的工作设想，以期与同行分享。