Optimizing Synthesis with Metasketches
Optimizing Synthesis with Metasketches
复制标题
DOI：
10.1145/2914770.2837666
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Ceze, Luis
中科院分区：
文献类型：
--
作者：
Bornholt, James;Torlak, Emina;Ceze, Luis
许多用于最终用户和专家开发人员的高级编程工具都依靠程序合成来自动从高级规格中生成实现。这些工具通常需要采用棘手，定制的合成算法，因为它们要求合成程序不仅正确，而且在所需的成本度量（例如程序尺寸）方面也是最佳的。有效地找到这些最佳解决方案需要特定于域的搜索策略，但是现有的合成器对策略进行了硬编码，使其难以重复使用。本文提出了Metasketches，这是指定和解决最佳合成问题的一般框架。 Metasschethes将搜索策略作为问题定义的一部分，通过将搜索空间的碎片定义为一组经典草图集。我们提供两种合作的搜索算法，以有效求解Metasschethes。全球优化搜索协调当地搜索活动的活动，向他们告知他们在探索候选人空间不同区域的潜在解决方案的成本。本地搜索执行反例引导的归纳合成的增量形式，以合并从全局搜索发送的信息。我们提出突触，这是这些算法的实现，并表明它有效地解决了各种不同成本函数的最佳合成问题。此外，MetassCethes可以通过明确控制搜索策略来使用MetassChete来加速经典（非最佳）合成，我们表明Synapse解决了最新工具无法使用的经典合成问题。
Many advanced programming tools for both end-users and expert developers rely on program synthesis to automatically generate implementations from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms because they require synthesized programs to be not only correct, but also optimal with respect to a desired cost metric, such as program size. Finding these optimal solutions efficiently requires domain-specific search strategies, but existing synthesizers hard-code the strategy, making them difficult to reuse.This paper presents metasketches, a general framework for specifying and solving optimal synthesis problems. Metasketches make the search strategy a part of the problem definition by specifying a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. A global optimizing search coordinates the activities of local searches, informing them of the costs of potentially-optimal solutions as they explore different regions of the candidate space in parallel. The local searches execute an incremental form of counterexample-guided inductive synthesis to incorporate information sent from the global search. We present SYNAPSE, an implementation of these algorithms, and show that it effectively solves optimal synthesis problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly controlling the search strategy, and we show that SYNAPSE solves classic synthesis problems that state-of-the-art tools cannot.