Translation and Run-Time Validation of Loop Transformations

This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validationperforms a validation check after every run of the compiler, producing a formal proof that the produced target code is a correct implementation of the source code. As part of an active and ongoing research project on translation validation, we have previously described approaches for validating optimizations that preserve the loop structure of the code and have presented a simulation-based general technique for validating such optimizations. In this paper, for more aggressive optimizations that alter the loop structure of the code—such as distribution, fusion, tiling, and interchange—we present a set of permutation ruleswhich establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation. We describe the extensions to our tool voc-64 which are required to validate these structure-modifying optimizations. This paper also discusses preliminary work on run-time validation of speculative loop optimizations. This involves using run-time tests to ensure the correctness of loop optimizations whose correctness cannot be guaranteed at compile time. Unlike compiler validation, run-time validation must not only determine when an optimization has generated incorrect code, but also recover from the optimization without aborting the program or producing an incorrect result. This technique has been applied to several loop optimizations, including loop interchange and loop tiling, and appears to be quite promising. This research was supported in part by NSF grant CCR-0098299, ONR grant N00014-99-1-0131, and the John von Neumann Minerva Center for Verification of Reactive Systems.     

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.     

Run-Time Validation of Speculative Optimizations using CVC.

Translation validation is an approach for validating the output of optimizing compilers. Rather than verifying the compiler itself, translation validation mandates that every run of the compiler generate a formal proof that the produced target code is a correct implementation of the source code. Speculative loop optimizations are aggressive optimizations which are only correct under certain conditions which cannot be validated at compile time. We propose using an automatic theorem prover together with the translation validation framework to automatically generate run-time tests for such speculative optimizations. This run-time validation approach must not only detect the conditions under which an optimization generates incorrect code, but also provide a way to recover from the optimization without aborting the program or producing an incorrect result. In this paper, we apply the run-time validation technique to a class of speculative reordering transformations and give some initial results of run-time tests generated by the theorem prover CVC.     

DSP汇编程序优化方案

对于复杂的算法和功能模块用汇编代码编写并对其进行优化,往往能够起到事半功倍的效果。DSP汇编指令多采取并行的方式,使其优化的潜力很大,复杂程度也很高。一个计算或一次存储器访问往往有多种实现方式及相应的指令,应选择最有效的指令。但几条最有效的指令放在一行内或几行内就不一定能得到最快的执行速度,甚至得不到正确的结果。这涉及到指令间的资源冲突、流水引起的数据相关性问题。本文从这两方面出发,以ADI公司的TS101程序为实例,归纳概括出对DSP汇编代码进行优化的一般方法。     

基于DSP的数字波束形成算法优化实现

在DSP上移植算法，代码优化程度成为提高系统性能、缩短开发周期的瓶颈。同时针对复杂算法在DSP上的实现，也产生很多优化策略、方法。本文介绍水声信号处理中广泛使用的数字式波束形成（DBF）算法，简述DBF的基本原理以及目标处理器（TMS320C6201）的处理能力；介绍C6000软件编程及优化步骤，并提出一些具体的优化策略和技巧。     

基于模型的嵌入式C代码的实现与验证

以51芯片为例,讲述了模型的建立、调试与验证,以及基于模型的嵌入式C代码的自动生成及软硬件在环测试。实践表明,该基于模型的设计方法可显著提高工作效率、缩短研发周期、降低开发成本,并且增加了代码的安全性与鲁棒性,有效降低了产品软件开发的风险。     

Run-Time Checking of Dynamic Properties

We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for replication of properties for dynamically created and destroyed objects in the system. The other kind, called attribute quantifiers, is used to check dynamically changing values within the same object. We show that expressions in this language can be efficiently checked over an execution trace of a system.     

使用动态二进制翻译防止代码植入攻击

论文主要介绍了代码植入攻击的原理及其防范，并讨论了如何将动态二进制翻译应用于代码植入攻击的防范．介绍了两种方法：带外返回地址验证和系统调用沙盒。     

二进制翻译中的标志位优化技术

在二进制翻译技术中,如何有效降低对源指令集体系结构标志位的模拟开销是一个值得研究的课题．分别针对二进制翻译中的解释执行和动态翻译,提出了相应的标志位模拟优化算法,能够有效地减少翻译生成的目标代码数量,提高目标代码性能．经过大量测试验证,在应用该标志位模拟优化算法后,Digital Bridge系统翻译生成的目标代码量是源体系结构目标代码量的120％,而没有应用该优化算法时该比例是250％,作为对比系统UQDBT系统的比例是150％．     

动态二进制翻译中的代码Cache管理策略

就代码cache的管理抽出了CPB（cache-piece-block)策略,它具有全清空,FIFO和LRU策略的优点,并且考虑到程序的时间空间局部性和cache替换开销,从而实现了对代码cache的高效管理。     

基于位图汉字验证码的Web认证系统及其应用

介绍了在Web系统中通过采用窗体身份验证和附加码技术来增强Web认证系统的安全性.附加码显示的是系统随机产生的GB2312码的一级汉字的图像,并给出了ASP.NET实现的关键程序代码.     

The Utilization of Matrix Structure to Generate Optimized Code from MATLAB Programs

The FALCON development environment was designed around three basic data representations: scalars, vectors, and dense matrices. Utilizing the FALCON interactive restructuring system, the environment has been enhanced to allow the identification of structures within sparse matrices, such as diagonal matrices or symmetric matrices, and the use of this information for improving performance of the generated code. In addition, the environment supports the modification of the representation of the data. Such modifications have been shown to provide significant performance improvements.     

The Implementation of Run-Time Diagnostics in Pascal

This paper considers the role of run-time diagnostic checking in enforcing the rules of the Pascal programming language. Run-time diagnostic checks must be both complete (covering all language requirements) and efficient. Further, such checks should be implemented so that the cost of enforcing the correct use of a given construct is borne by users of that construct. This paper descxibes simple and efficient mechanisms currently in use with a diagnostic Pascal compiler that monitor the run-time behavior of such sensitive Pascal constructs as pointers, variant records, reference (i.e., var) parameters, and with statements. The use of these mechanisms with related constructs in other languages is considered. Language modifications that simplify run-time checking ate also noted.     

同步变长码码字和码序号的互换算法

基于同步变长码（SVLC）的构造原理,先根据码长的不同将码表分成不同的码组,再根据前n位的不同将码组细分为不同的子码组,然后给出了一种计算SVLC子码组的码长分布的迭代算法。基于码表中码字首先按码长从小到大排列,码长相同时按码字对应的二进制值从小到大排列的准则,并利用码组和子码组的码长分布,给出了一种SVLC的码字和序号互换的算法。     

Effective and Efficient Compilation of Run-Time Generics in Java

After several years from Sun Microsystems' call-for-proposals for adding generics to the Java Programming Language, JDK 1.5 will be finally shipped with a compile-time support for generics. However, differently e.g. from the current implementation of .NET Common Language Runtime, run-time support to generics — also commonly referred to as reification of type parameters — is not provided, leading to a number of well-known inadequacies which might potentially be critical. In this paper we present the EGO compiler (Exact Generics on Demand). This is the result of a project developed in collaboration with Sun Microsystems as an effort to provide run-time generics in a smooth way, without requiring any change on the JVM or on any other run-time support. The core solution is a sophisticated translation of code based on the type-passing style, where run-time type information is automatically created on a by-need basis, limiting as most as possible run-time overhead while retaining interoperability with legacy Java code.We present the main aspects of this development, from basic design to implementation and deployment issues. Many relevant aspects that typical raise when implementing advanced type systems over a mainstream programming language are discussed, shading light to some effective implementation techniques.     

Highly Optimized Code Generation for Stencil Codes with Computation Reuse for GPUs

Computation reuse is known as an effective optimization technique. However, due to the complexity of modern GPU architectures, there is yet not enough understanding regarding the intriguing implications of the interplay of computation reuse and hardware specifics on application performance. In this paper, we propose an automatic code generator for a class of stencil codes with inherent computation reuse on GPUs. For such applications, the proper reuse of intermediate results, combined with careful register and on-chip local memory usage, has profound implications on performance. Current state of the art does not address this problem in depth, partially due to the lack of a good program representation that can expose all potential computation reuse. In this paper, we leverage the computation overlap graph (COG), a simple representation of data dependence and data reuse with “element view”, to expose potential reuse opportunities. Using COG, we propose a portable code generation and tuning framework for GPUs. Compared with current state-of-the-art code generators, our experimental results show up to 56.7 % performance improvement on modern GPUs such as NVIDIA C2050.