代数库规范下的程序合成( 四 ) 1引用BenjaminMariano,JoshReese,Siyu

对于测试工具，我们将测试套件用于每个基准测试。回忆一下这些测试工具是我们的规格；也就是说，保证任何合成程序相对于测试套件都是正确的。一些示例包含不完整的测试套件或缺少测试套件，因此我们添加了其他工具来涵盖更多的方法和功能。在实践中，我们发现其他工具是对现有测试的简单扩展。
由于我们与代数规范和模拟共同开发了 JLibSketch ，因此无法直接比较每种方法所需的工作量。但是，我们确实观察到大小上的显着差异。表 1 的最后三列给出了每个程序所需的规范和模拟的 LoC 以及它们的比率。从表中可以看出，每个示例的代数规格要求的 LoC 较少。所有示例的中位数差异超过 80 行。在最坏的情况下（比较器），代数规范仅缩短 20％，而在最坏的情况下（HashMap），则缩短 70％。对于 Comparator ，差异较小是由于难以使用重写规则对 ArrayList 进行编码排序；这是重写规则不是自然规范时的情况。相反， HashMap 的 LoC 差异很大是由于复杂的模拟 ArrayList 方法，代数规范不需要这种实现选择。
为了制定基准，我们通过应用预定的规则将表 1 中的程序系统地转化为合成问题。此过程的目的是产生具有挑战性的合成问题，这些问题并非针对特定的库建模方法而量身定制的。规则如下：
（1）为每种局部变量类型创建一个数组。使用数组可使合成器轻松分配给这些变量。
（2）创建一个函数合成器 stmts ，它表示对局部变量的可能分配以及对副作用的 void 函数的调用。我们使用类型信息来确定可能的分配。
（3）创建一个保护合成器，返回局部布尔值，调用布尔值函数的结果，比较以及此类术语的合取，析取和否定。
（4）用对 stmts 合成器的调用替换每个非控制、非返回语句的块，并用对保护合成器的调用替换每个条件保护。
（5）将每个非无效的 return 语句替换为适当类型的合成器的返回值。
为了使问题易于处理，我们根据需要进行了简化以减少搜索空间。我们的简化主要包括删除递归合成器调用。
表 2 中的第二组列显示成功合成所需的语句（#S）和防护（#G）的数量以及近似的搜索空间大小。更准确地说，（＃G）是警惕的调用次数，而（#S）至少是对 stmts 的调用次数，因为对后者的每次调用都可能合成多个语句。搜索空间的大小是近似值，因为在运行时通过启发式确定 Sketch 中合成器的内联。
表 2 合成问题和实验结果的描述
文章插图
Sketch 性能注意事项。在运行基准测试时，我们发现一些 Sketch 命令行标志具有显着的性能影响。特别是，循环展开边界（U）和函数调用内联边界（I）会影响所有九个基准。此外，整数范围（R），控制位范围（C）和自适应具体化的使用（A）影响了某些基准的性能。当前，没有确定这些范围的自动机制，因此我们从将每个设置为 1 开始，禁用自适应具体化，并且没有控制位或整数范围。然后，我们增加界限，直到合成成功。对于每个基准，模拟和代数规范的结果界限都是相同的。
运行时性能。表 2 中的最后一组列显示了模拟和代数规格的合成运行时间（以秒为单位）。所有测试均使用运行于 2.2 GHz ， 128 GB RAM 的 10 核 Intel Xeon v4 CPU 进行。我们使用模拟程序对每个合成问题运行 31 次，使用代数规范运行 31 次。该表给出了中值时间，并以小字体给出了半四分位间距（SIQR）。对于所有问题，我们都将超时设置为 4 小时（14400 秒）。我们手动验证了每种合成的正确性。我们观察到，三个基准测试因模拟而超时，但成功完成了代数指定。为了比较其余六个基准的性能，我们使用了非参数的 Mann-Whitney U 检验来比较模拟和代数规范的结果分布。我们发现，对于余下的六个程序中的四个（以粗体表示），具有代数规范的合成在统计学上比在模拟上的合成显着快得多，而在其他两个程序中则相同。尽管很难理解实验中性能差异的原因，但我们确实确定了几种趋势。在加密示例中，模拟中的实现选择可能会产生显着的性能影响。我们还注意到，限制整数范围可以显着提高性能。
总体而言，在我们的实验中，对于 9 个基准中的 7 个，使用代数规范的合成比使用模拟的合成要快，而对于其他两个基准，合成的性能相同。此外，中位性能提升范围从 2 倍到超过 81 倍，并且在三个示例中，代数规范在模拟超时的情况下结束。因此，我们的结果表明，对于一系列程序，代数规范可以提供比模拟更好的合成性能优势。