Source-to-Source Conversion Based on Formal Definition

This paper proposes the idea of source-to-source conversion between two heterogeneous high-level programming languages.The conversion is based on formal definition and oriented to multi-pairs of languages.The issues in conversion from PASCAL to C are also discussed.     

面向CPU-GPU源到源编译系统的渐近拟合优化方法

针对CPU-GPU异构并行系统应用开发移植后优化不充分问题,提出了一种渐近拟合优化与源到源编译相结合的方法,该方法能够对插入了制导语句的C语言程序转换为CUDA语言后的程序进行多次剖分,根据源程序特性和硬件信息自动完成源到源编译与优化,并基于该方法实现了原型系统。通过在不同环境中的该原型系统在功能和性能方面进行的测试表明,由系统生成的CUDA目标程序与C源程序在功能上一致,性能上却有了大幅度提高,通过与CUDA基准测试程序相比表明,该目标程序在性能上明显优于其他源到源编译转换生成的程序。     

Implementing a Domain-Specific Language Using Stratego/XT: An Experience Paper

We describe the experience of implementing a Domain-Specific Language using transformation to a General Purpose Language. The domain of application is image processing and low-level computer vision. The transformation is accomplished using the Stratego/XT language transformation toolset. The implementation presented here is contrasted with the original implementation carried out many years ago using standard compiler implementation tools of the day. We highlight some of the unexpected advantages afforded to us, as language designers and implementers, by the source-to-source transformation technique. We also present some of the practical challenges faced in the implementation and show how these issues were addressed.     

针对C语言的自动微分系统及其应用*

采用切线性模式和代码转换策略,开发了C语言自动微分转换系统（DTC）,用于牛顿法求解非线性方程中Jacobi矩阵—向量乘积计算。介绍系统计算模型、功能、特色,并讨论系统的设计与实现技术,包括编译技术、微分代码转换及输入/输出（I/O）相关分析。最后给出了几个具有说服力的测试与应用。     

Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.     

A Transformational Derivation of a Parsing Algorithm in a High-Level Language

This paper presents a detailed algorithm derivation scenario, using correctness preserving source-to-source transfonnations. The algorithm derived is the Cocke-Younger nodal spans parsing algorithm. We describe a high-level SETL-like specification language, and give a partial correctness formalism and a set of transformation rules which enable the combination of algorithms whose partial correctness has already been established.     

基于DSP的KLT特征点跟踪算法优化实现

针对C6000系列定点DSP下KLT特征点跟踪算法的快速实现问题,通过结合DSP体系结构特点以及软件流水技术,提出了一种该类型DSP下的算法优化实现方案.基于算法流程的模块化分析,完成了该算法的定点化设计与实现工作;针对算法中计算密集型模块,提出了具体的改善软件流水,减少存储器访问,任务级并行设计等优化实现方法.在DSP软仿真平台CCS下进行实验测试,该优化实现方案下的运行效率和资源利用率均有较大的提升,且所使用的算法优化方法适用于所有C6000系列DSP.     

A new Mixed Radix Conversion algorithm MRC-II

In this paper, we present an efficient and simplified algorithm for the Residue Number System (RNS) conversion to weighted number system which in turn will simplify the implementation of RNS sign detection, magnitude comparison, and overflow detection. The algorithm is based on the Mixed Radix Conversion (MRC). The new algorithm simplifies the hardware implementation and improves the speed of conversion by replacing a number of multiplication operations with small look-up tables. The algorithm requires less ROM size compared to those required by existing algorithms. For a moduli set consisting of eight moduli, the new algorithm requires seven tables to do the conversion with a total table size of 519 bits, while Szabo and Tanaka MRC algorithm [N.S. Szabo, R.I. Tanaka, Residue Arithmetic and its Application to Computer Technology, McGraw-Hill, New York, 1967; C.H. Huang, A fully parallel mixed-radix conversion algorithm for residue number applications, IEEE Transactions on Computers c-32 (4) (1983)] requires 28 tables with a total table size of 8960 bits; and Huang MRC algorithm (Huang, 1983) requires 36 tables with a total table size of 5760 bits.     

Boolean and Cartesian abstraction for model checking C programs

We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a Boolean C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.     

Optimum RNS sign detection algorithm using MRC-II with special moduli set

In this paper, we present a generic sign detection algorithm based on mixed radix conversion algorithm, MRC-II [M. Akkal, P. Siy, A new mixed radix conversion algorithm MRC-II, Journal of System Architecture (2006)] and also we present an optimum algorithm for sign detection based on a special moduli set where m_n is even. The described algorithm requires only one comparison for sign detection. A new moduli set will also be presented which simplifies MRC-II conversion algorithm by eliminating the need for table lookup normally used in MRC hardware implementation. The algorithm does not require ROM table like other algorithms. For a moduli set of four moduli that satisfies the special moduli set conditions, 0 tables are needed to do the conversion, while Szabo and Tanaka MRC algorithm [N.S. Szabo, R.I. Tanaka, Residue Arithmetic and Its Application to Computer Technology, McGraw-Hill, New York, 1967] requires 6 tables with a total table size of 4608 bits; and Huang MRC algorithm [C.H. Huang, A fully ParallelMixed-radix conversion algorithm for residue number applications, IEEE Transactions on Computers c-32 (4) (1983)] requires 10 tables with a total table size of 3840 bits.