An empirical study of adaptive concretization for parallel program synthesis
An empirical study of adaptive concretization for parallel program synthesis
复制标题
并行程序综合自适应具体化的实证研究
DOI：
10.1007/s10703-017-0269-8
复制
发表时间：
2017
影响因子：
0.8
通讯作者：
J. Foster
中科院分区：
文献类型：
--
作者：
Jinseong Jeon;Xiaokang Qiu;Armando Solar;J. Foster
自适应具体化是一种程序合成技术，可以有效地平行挑战的合成问题。自适应具体化背后的关键观察是，在充满挑战的综合问题中，有些未知数最适合于明确的搜索，有些最适合通过约束解决的象征性搜索。在很高的水平上，自适应具体化背后的主要思想是动态确定哪些未知数最适合哪种搜索，并在那些未知的搜索方面并行化明确的搜索。我们首先在较早的论文中引入了自适应混凝土[Jeon等。在计算机辅助验证中，施普林格，柏林2015]。我们的原始算法涉及一些任意设计决策，留下了一个问题，即不同选择是否可以实现更好的性能。在本文中，我们系统地评估了设计空间的几个维度，以更好地了解权衡。我们表明，通常沿这些维度稳健，我们的最初选择是合理的。
Adaptive concretization is a program synthesis technique that enables efficient parallelization of challenging synthesis problems. The key observation behind adaptive concretization is that in a challenging synthesis problem, there are some unknowns that are best suited for explicit search and some that are best suited for symbolic search through constraint solving. At a high level, the main idea behind adaptive concretization is to dynamically identify which unknowns are best suited to which kind of search, and to parallelize the explicit search on those unknowns for which that style of search is more suitable. We first introduced adaptive concretization in an earlier paper [Jeon et al. in Computer aided verification, Springer, Berlin 2015]. Our original algorithm involved a few arbitrary design decisions, leaving open the question of whether different choices could achieve better performance. In this paper, we systematically evaluate several dimensions of the design space to better understand the tradeoffs. We show that, in general, adaptive concretization is robust along those dimensions, and our initial choices were reasonable.