Speeding up machine-code synthesis
Speeding up machine-code synthesis
复制标题
加速机器代码合成
DOI：
10.1145/2983990.2984006
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
T. Reps
中科院分区：
文献类型：
--
作者：
Venkatesh Srinivasan;Tushar Sharma;T. Reps
机器码合成是搜索实现语义规范的指令序列的问题，该语义规范以无量化器位向量逻辑（QFBV）中的公式给出。像英特尔的IA-32这样的指令集有大约43，000个唯一的指令模式;这个巨大的指令池，沿着枚举合成中固有的指数成本，导致机器代码合成器的巨大搜索空间：即使是相对较小的规范，合成器也可能需要几个小时或几天才能找到实现。在本文中，我们提出了几个改进的算法中使用的一个国家的最先进的机器代码合成器McSynth。除了一个新的修剪启发式，我们的改进纳入了一些已知的想法，从文献中，我们适应以新的方式加快机器代码合成的目的。我们对英特尔IA-32指令集的实验表明，我们的改进能够合成McSynth超时的14个公式中的12个公式的代码，将合成时间加快至少1981倍，对于其余公式，将合成速度加快3倍。
Machine-code synthesis is the problem of searching for an instruction sequence that implements a semantic specification, given as a formula in quantifier-free bit-vector logic (QFBV). Instruction sets like Intel's IA-32 have around 43,000 unique instruction schemas; this huge instruction pool, along with the exponential cost inherent in enumerative synthesis, results in an enormous search space for a machine-code synthesizer: even for relatively small specifications, the synthesizer might take several hours or days to find an implementation. In this paper, we present several improvements to the algorithms used in a state-of-the-art machine-code synthesizer McSynth. In addition to a novel pruning heuristic, our improvements incorporate a number of ideas known from the literature, which we adapt in novel ways for the purpose of speeding up machine-code synthesis. Our experiments for Intel's IA-32 instruction set show that our improvements enable synthesis of code for 12 out of 14 formulas on which McSynth times out, speeding up the synthesis time by at least 1981X, and for the remaining formulas, speeds up synthesis by 3X.