Adaptive Concretization for Parallel Program Synthesis
Adaptive Concretization for Parallel Program Synthesis
复制标题
并行程序综合的自适应具体化
DOI：
10.1007/978-3-319-21668-3_22
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
J. Foster
中科院分区：
文献类型：
--
作者：
Jinseong Jeon;Xiaokang Qiu;Armando Solar;J. Foster
程序综合工具通过搜索满足给定规范的实现来起作用。两种流行的搜索策略是符号搜索，它将合成降低到传递给SAT求解器的公式，并明确搜索，该搜索使用蛮力或随机搜索来找到解决方案。在本文中，我们提出了自适应混凝土化，这是一种新型的合成算法，结合了符号和明确搜索的最佳算法。我们的算法通过部分凝结一个随机选择但可能具有很高影响力的未知数子集的作用。自适应混凝土使用在线搜索过程，使用指数爬坡和二进制搜索的组合，使用统计测试来确定一种何时凝结何时比另一个更好。此外，我们的算法使自己具有高度平行的实现，从而进一步加快了搜索。我们对草图实施了自适应具体化，并根据一系列基准进行了评估。我们发现自适应混凝土在许多情况下非常有效，表现优于草图，有时显着，并且具有良好的并行可伸缩性。
在新窗口中打开图像
Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search. We implemented adaptive concretization for Sketch and evaluated it on a range of benchmarks. We found adaptive concretization is very effective, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability.
Open image in new window