Synthesis of fixed-point programs
Synthesis of fixed-point programs
复制标题
定点程序的综合
DOI：
10.1109/emsoft.2013.6658600
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
I. Saha
中科院分区：
文献类型：
--
作者：
Eva Darulova;Viktor Kunčak;R. Majumdar;I. Saha
在控制系统、信号处理系统和科学计算系统的实现中，有几个问题归结为使用定点运算将实数上的多项式表达式编译成命令式程序。不动点算术只近似于真实的值，并且它的运算符不具有真实的算术的基本性质，例如结合性。因此，朴素编译过程可能产生显著偏离真实的多项式的程序，而不同的求值顺序可能导致程序在其域中的所有输入上接近真实的值。我们提出了一种将实值算术表达式编译为定点算术程序的编译方案。给定一个实值多项式t，我们找到一个表达式t'，它等价于实数上的t，但它的实现是一系列定点运算，使定点值和所有输入空间上的t值之间的误差最小化。我们表明，相应的决策问题，检查是否有一个实现t'的t，其误差小于给定的常数，是NP-困难的。然后，我们提出了一种基于遗传规划的解决方案。我们的技术使用基于仿射算法的静态分析来评估每个候选程序的适合度。我们表明，我们的工具可以显着减少在一组线性控制系统基准的定点实现的错误。例如，我们的工具发现实现的错误仅为原始定点表达式中错误的一半。
Several problems in the implementations of control systems, signal-processing systems, and scientific computing systems reduce to compiling a polynomial expression over the reals into an imperative program using fixed-point arithmetic. Fixed-point arithmetic only approximates real values, and its operators do not have the fundamental properties of real arithmetic, such as associativity. Consequently, a naive compilation process can yield a program that significantly deviates from the real polynomial, whereas a different order of evaluation can result in a program that is close to the real value on all inputs in its domain. We present a compilation scheme for real-valued arithmetic expressions to fixed-point arithmetic programs. Given a real-valued polynomial expression t, we find an expression t' that is equivalent to t over the reals, but whose implementation as a series of fixed-point operations minimizes the error between the fixed-point value and the value of t over the space of all inputs. We show that the corresponding decision problem, checking whether there is an implementation t' of t whose error is less than a given constant, is NP-hard. We then propose a solution technique based on genetic programming. Our technique evaluates the fitness of each candidate program using a static analysis based on affine arithmetic. We show that our tool can significantly reduce the error in the fixed-point implementation on a set of linear control system benchmarks. For example, our tool found implementations whose errors are only one half of the errors in the original fixed-point expressions.