ACM通信

研究突出了

技术视角:使用随机技术的程序综合

由苏米特Gulwani
ACM通信，2016年2月，第59卷第2期，第113页
10.1145 / 2863699
评论

程序综合涉及使用某种搜索技术从满足给定规范的底层程序空间中发现一个程序。^3.它有很多应用，包括算法发现、优化实现、编程辅助、⁵以及合成小脚本，为最终用户自动化重复任务。⁴它的成功在很大程度上依赖于高效的搜索算法来导航程序底层巨大的状态空间。本文的作者开发了一种随机搜索技术，并将其应用于程序优化。他们在硬程序优化基准上实现STOKE的令人印象深刻的结果说明了随机搜索在硬程序综合问题中的潜力。

程序综合的规范可以采用输入和输出之间的逻辑声明关系的形式。示例或演示跟踪是终端用户编程的流行规范选择。⁴在程序优化中，当被视为一个综合问题时，规范由低效的程序组成，这些程序需要转换为功能等效但更高效的程序。

多个解可以满足规范中的布尔约束。在这种情况下，可以使用优化函数指定首选项。在按例编程中，解决方案的数量可能是10的几次方，根据程序特性对函数进行排序，以猜测预期的程序。⁴在程序优化中，目标是选择运行时更小的程序。STOKE使用相关指令的平均延迟之和作为预期度量的一个很好的静态近似。

程序综合中的搜索空间需要权衡:既要有足够的表达能力来描述感兴趣的程序，又要有足够的限制来实现高效的综合。各种特定于领域的语言都是为合成目的而设计的^1，3.满足这种取舍。在程序优化中，常用的选择是有界长度的无环指令序列。以前的技术将空间限制在10-15个操作码或要求为给定的问题实例指定一小组相关操作码，而STOKE允许近400个x86-64操作码，极大地提高了技术水平。

回到顶部

搜索技术

一种简单的搜索策略是在底层空间中按大小增加的顺序枚举程序。然而，这并不能扩展到STOKE所考虑的那种巨大的搜索空间。另一种策略是将(二阶)搜索问题简化为(一阶)约束求解^3.利用现成的SAT/SMT求解器，如Z3。²这允许构建在SAT/SMT求解中取得的巨大工程进步，但不允许有效地整合优化约束。Version-space algebra-based技术⁴通过在第一个阶段计算所有/多个解决方案集，然后在第二个阶段选择排名最高的解决方案，来合并首选项。斯托克还采用了两阶段的方法。它的第一阶段寻找算法上不同的解决方案，而第二阶段寻找第一阶段发现的代码序列的有效实现。

随机搜索。斯托克使用随机搜索的每两个阶段。这包括一个适当定义的成本度量，以及选择下一个候选的MCMC抽样。第一阶段的成本度量基于与目标输入序列的功能等价(一个布尔约束)。第二阶段成本度量结合了功能等价度量和性能度量(优化约束)。为了在布尔程序等价约束上定义一个平滑的成本度量，STOKE使用了两个聪明的启发式:使用汉明距离来度量生成的位值与代表性测试输入集上目标的接近度，以及奖励在不正确的位置上(几乎)正确的值的生成。

跨学科的灵感。STOKE结合了软件工程、编程语言和数值优化的技术。它使用测试输入生成(英特尔的PinTool)来生成具有代表性的测试输入，以评估MCMC采样期间的等价成本度量。它使用自动定理证明(微软的Z3)在后处理步骤中验证合成序列的等价性。最近的扩展在循环程序空间中搜索利用不变推理技术来验证等价性。斯托克是一个伟大的实践，在跨学科启发的高效搜索算法的困难综合问题。这是及时和重要的，考虑到最近在不同社区的规划综合领域重新产生的兴趣和有前途的发展。

回到顶部

回到顶部

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2016 ACM, Inc.

---

没有发现记录