LCT：分布式concolic测试与DPOR和睡眠集算法在多线程Java程序上的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）253-259www.elsevier.com/locate/entcsLCT：一个面向多线程Java程序的KariKahkonen、OlliSaarikivi和KeijoHeljanko理学院信息与计算机科学系阿尔托大学PO Box 15400，FI-00076 AALTO，Finland{Kari.Kahkonen，Olli.Saarikivi，Keijo.Heljanko} @ aalto.fi摘要LIME Concolic Tester（LCT）是一个开源的自动化测试工具，允许测试两个顺序多线程Java程序该工具使用concolic测试来处理输入值，并结合睡眠集使用动态偏序约简（DPOR）来避免探索不必要的线程交织。LCT工具是为分布式使用而设计的，其中SMT约束求解和测试执行可以分布到工作站网络上的多个进程。 在本文中，我们描述了该工具背后的架构，以及它如何允许分布式concolic测试与DPOR和睡眠集算法。 这允许并行测试给定程序的不同执行路径。 我们评估该工具的体系结构和分布式算法在几个Java基准测试程序上的应用。关键词：Concolic测试，分布式测试，符号执行1引言与手工编写的测试用例相比，自动化测试有可能提高可靠性并降低成本。自动化测试的一种技术是使用concolic测试结合具体和符号执行来探索给定顺序程序的不同执行路径。Concolic测试可以与动态偏序约简（DPOR）和睡眠集算法相结合，使该方法也可以用于测试多线程程序。基于这些算法，我们已经开发了一个开源的工具LCT（LIME Concolic Tester），可以自动测试顺序和多线程的Java程序。该工具已被设计为分布式使用的计算机网络可以利用，使测试方法的规模比在非分布式的情况下更大的程序。我们之前已经通过测试[7]中的单线程程序评估了我们工具的分布式特性，从那时起，我们已经扩展了我们的工具，以支持使用[8]中描述的DPOR算法的多线程程序主要1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.002254K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）253本文的贡献是：（i）一个面向工具的描述，我们的系统的分布式体系结构和修改所需的DPOR和睡眠集算法，使他们在这种体系结构中可用，和（ii）一个新的实验评估的分布式性质，我们的工具多线程程序。特别是，新的实验集中在大多数测试执行的情况下，由于不同的时间我们表明，即使在这种情况下，测试可以分布作为有效的单线程程序。本文其余部分的结构如下。第2节简要介绍concolic测试和动态偏序约简算法，第3节给出了LCT的概述以及我们对所用算法的修改，第4节涵盖了相关工作，第5节提供了多线程程序背景下的分布式体系结构2 Concolic测试和动态偏序约简Concolic测试[6，9，4]（也称为动态符号执行）是一种方法，其中一个给定的程序同时被具体地和符号地执行这种方法背后的主要思想是，在运行时，在每个分支点收集符号约束，这些约束指定导致程序采取特定分支的输入值作为一个例子，一个程序x = x +1;if（x>0）;将在if语句中生成约束input1+ 1>0和input1+ 1≤0，假设符号值input1最初被分配给x。路径约束是与给定执行中做出的每个分支决策相对应的符号约束的结合。要强制测试执行遵循未探索的执行路径，请使用先前探索的路径约束的前缀被选中，并且其中的最后一个符号约束被否定。为了获得具体的输入值，通常使用SMT求解器来求解路径约束。符号约束形成了一个符号执行树，每个测试都在这个树中探索一条路径。由于符号执行树的任何两个不同的子树可以独立地进行探索，因此可以有效地并行化测试过程。有关concolic测试的更多详细信息，请参见例如，[9]的文件。对于多线程程序，调度也会选择执行路径。在concolic测试中，可以通过控制调度器并将调度视为系统的输入来处理由线程交织引起的不确定性为了限制需要探索的线程交织的数量，可以将卷积测试与动态偏序约简算法结合起来[5]。这些算法背后的基本思想是找到当前执行中处于竞争中的转换，然后将回溯点引入执行树，以便最终探索竞争中转换的不同交织K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）2532553工具详情Fig. 1. LCT的架构LCT的架构遵循客户端-服务器模型，如图1所示。LCT由三个主要部分组成：仪器，服务器（测试选择器）和客户端（测试执行器）。为了测试一个给定的Java程序，首先在代码中标记输入位置。例如，intx =LCT. getString（）表示将为变量x生成一个int类型的输入。在此之后，程序被交给仪器，仪器通过向程序添加新代码来修改程序，使其能够符号执行。对于这一步，LCT使用了一个名为Soot的程序转换框架[10]，并为大多数语句添加了符号对应物，这些符号对应物以符号方式执行相同的操作。为了使Java程序的插装更容易，给定的程序首先被翻译成一种名为Jimple的中间语言，它在插装之后，程序被翻译回字节码。生成的程序称为测试执行器，其工作方式为一个客户当客户端运行时，它发送信息（例如，约束）发送到服务器，服务器又基于该信息构造符号执行树。当客户端完成测试执行时，它会向服务器请求新的输入值。然后，服务器选择接下来探索符号执行树中的哪条路径，并将相应的线程调度和路径约束发送给客户端，客户端然后对其进行求解以获得具体的输入值。通过这种方式，约束求解被分发到客户端，并防止约束求解成为测试过程并行化的瓶颈。服务器和客户端之间的通信是使用TCP套接字实现的，这使得很容易将测试分布到多个工作站。在测试执行过程中生成的约束以位向量理论表示，布尔向量[2]用作约束求解器。为了避免在测试多线程程序时探索不必要的交织，该工具使用了动态偏序约简和睡眠集算法。为了将这些算法应用于我们的dis.256K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）253我们将对它们进行一些修改，这些修改将在下面描述3.1分布式环境中的动态偏序约简和睡眠集DPOR是无状态的，在这个意义上，以前访问过的国家不需要识别种族。然而，对于回溯，确实需要一种方法来到达以前的状态。有几种方法可以做到这一点[5]。LCT使用程序的重新执行，因为它是与concolic测试相结合的自然选择。 这这是因为concolic测试中的路径约束对具体状态集进行了编码，即使新的路径约束与旧的路径约束共享一个前缀，从新约束求解的输入可能不会将程序驱动到任何先前访问过的具体状态。重新执行是达到满足新路径约束的具体状态的一种方便方法在每个测试执行的开始，客户端从服务器获取一系列要重新执行的调度决策。在重新执行过程中不需要添加回溯点，因为任何识别的回溯点都已经由先前的测试执行添加。否则，DPOR在重新执行期间正常运行，这意味着维护用于标识回溯点的向量时钟和其他簿记数据为了能够重新执行，客户端将每个调度决策发送到服务器，服务器将它们添加到执行树中并记住客户端在其中的当前位置。然后将回溯点DPOR标识作为索引发送到服务器，沿着客户端的路径以及一组从该状态开始探索的备用操作。在随后的测试执行中，通过向客户端提供所收集的调度决策来探索这些备用操作，直到将备用操作附加到序列的回溯状态。在模型检验中，由偏序约简算法探索的约简状态空间通常必须满足循环条件，这防止了在状态图中的循环的所有状态中忽略操作在并行环境中实施循环限制条款具有挑战性，尽管已经提出了一些解决方案[1]。但是，由于DPOR是具有非循环状态空间的无状态方法，我们可以避免循环限制条件，允许更容易的并行化。使用多个并发客户端以及DPOR执行的回溯搜索是简单的：当一个客户端发现一个回溯点时，另一个客户端可以在第一个客户端完成之前开始执行测试来探索它。 虽然没有 需要客户端修改才能启用此功能，服务器必须正确同步。睡眠集可以与DPOR组合，以在DPOR无法从回溯状态识别要探索的准确操作集时提供额外的减少。睡眠集算法是基于这样的观察：在从某个状态s探索了操作t之后，然后在从s探索了与t无关的其他操作之后，没有必要再次探索t。为此，我们将每个到达的状态与睡眠集相关联，这是一组不在该状态下执行的操作K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）253257为了计算睡眠集合，当从s探索状态sJ时，sJ的候选睡眠集合是s的睡眠集合和已经从s探索的操作集合的并集。然后过滤该候选睡眠集合以仅包括与被执行以到达sJ的操作无关的操作。初始状态的睡眠集为空。我们的设置提出了实现睡眠集的两个复杂性：（i）只有服务器知道从给定状态探索了哪些操作;（ii）只有客户端知道操作之间的依赖关系。因此，我们在服务器和客户端之间划分实现如下。在执行开始时，服务器发送候选睡眠集，用于客户端重新执行服务器发送的操作序列后将达到的状态。当客户端到达序列末尾的状态以及之后的每个状态时，它收到的睡眠集将被过滤掉相关操作。以这种方式获得的每个新的睡眠集都被发送到服务器。客户端和服务器在执行操作和选择回溯点进行探索时都分别遵守睡眠集。对DPOR和睡眠集算法的修改的详细描述可以在[8]中找到，这些修改允许它们在客户端-服务器设置中使用4相关工作分布式concolic测试的另一种方法是以这样一种方式划分符号执行树，即单个工作进程探索树的独立分区。分区可以静态地或动态地完成。由于符号执行树的形状事先不知道，静态分区很少导致工作者之间的最佳负载平衡。动态分区解决了这个问题，并为大量工作者提供了出色的可伸缩性。然而，与LCT中使用的同步服务器方法相比，动态分区需要更复杂的实现。参见[3]，了解一种基于动态分区的方法。在[11]中，提出了一种使用分区来分配DPOR的方法。这种方法为工作者的数量提供了很好的可伸缩性，但在某些情况下会导致多次探索同一个调度。同步服务器方法没有这个问题。5实验为了评估LCT（版本2.2.1）的分布式体系结构，我们使用了使用不同数量的测试执行器客户端测试多个多线程Java程序，这些客户端同时运行。我们以前已经表明，分布式体系结构的单线程程序工作得很好。然而，DPOR的使用是否能足够快地生成足够多的开放分支以保持大量客户端忙碌，这一点并不直接明显。因此，这些实验集中在大多数测试运行的情况下，由于回溯请求的DPOR算法生成258K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）253基准Avg. 路径平均值时间1客户端2客户端5Avg.客户加速比10个客户端20 客户机1索引器（13）671285s1.894.688.9416.97文件系统（18）13847步枪1.924.558.8814.91并行Pi（5）1252250s1.954.739.1418.06合成1（3）1020176s1.994.919.7418.13合成2（3）4496783s2.004.869.6118.17表1LCT分布式体系结构的实验评估结果索引器和文件系统程序来自[5]，用于评估DPOR算法。Parallel Pi程序实现了计算π值的并行算法。合成程序是一些简单的例子，其中许多线程执行随机生成的共享变量访问序列在实验中，服务器运行在2.93GHz四核Linux工作站上，内存为4GB。客户端主要在3.30GHz双核Linux工作站1上运行，每个工作站有两个客户端。实验结果示于表1中。由于探索不同线程交织的顺序会影响DPOR的性能，因此我们的工具的不同运行会导致相同基准测试的不同测试运行次数为了考虑DPOR的这个属性，每个基准测试都使用随机的初始线程调度运行了五次。该表显示了在只使用一个客户端的情况下，探索的执行路径的平均数量以及测试它们所需的秒数。对于多个客户端同时运行的情况，该表显示了与单个客户端情况相比获得的平均加速比。结果表明，该架构至少可扩展到20个客户端。这是因为运行单个测试执行的时间，包括重新启动JVM以初始化全局状态，解决路径约束以及具体和象征性地运行程序，比服务器需要以同步方式执行此外，在大多数情况下，符号执行树中的开放路径数量足够大，因此每个客户端都有工作要做。6结论本 文 介 绍 了 LCT 工 具 ， 该 工 具 与 源 代 码 一 起 可 从 ：http://www.tcs.hut.fi/Software/lime/作为石灰接口测试台。我们已经描述了该工具的分布式架构以及我们对该架构所需的DPOR和睡眠集算法的修改。我们已经评估了几个Java程序的工具的分布式性质，并表明它提高了多线程程序的concolic测试的可扩展性1在20个客户端的情况下，另外10个客户端在不同的Linux工作站上运行，这些工作站比其余实验中使用的工作站稍快或稍慢。 性能差异小到单个运行时。K. Kähkönen et al. /Electronic Notes in Theoretical Computer Science 296（2013）253259特别是，我们已经表明，使用DPOR并不限制搜索新的执行路径进行测试，在这样一种方式，大量的并行工人不能有效地利用。确认这项工作得到了Tekes-芬兰技术和创新机构，Conformiq Software，Elektrobit，诺基亚，Space Systems Finland和芬兰科学院（项目126860，128050和139402）的财政支持，以及Artemis-JU资助的项目RECOMP（使用可信多核平台降低认证成本）。引用[1] Barnat，J.，L. Brim和P.Rockai，并行偏序减少与拓扑排序但书，在：J. L. Fiadeiro，S.Gnesi和A.Maggiolo-Schettini，editors，SEFM（2010），pp.222-231[2] 布鲁迈尔河和A. Biere，Boolector：An efficient SMT solver for bit-vectors and arrays，in：Proceedingsof the 15th International Conference on Tools and Algorithms for the Construction and Analysis ofSystems（TACAS 2009），Lecture Notes in Computer Science5505（2009），pp.174比177[3] Bucur，S.，V. Ureche，C. Zam fir和G. Candea，用于自动化真实世界软件测试，在：C。M. Kirsch和G.Heiser，editors，EuroSys（2011），pp.183-198.[4] 卡达尔角，V. Ganesh，P. M. Pawlowski，D. L. Dill和D. R. Engler，EXE：Automatically GeneratingInput of Death ， in ： Proceedings of the 13th ACM Conference on Computer and CommunicationsSecurity（CCS 2006）（2006），pp. 322-335[5] 弗拉纳根角，澳-地和P. Godefroid，Dynamic partial-order reduction for model checking software，在：J. Palsberg和M.Abadi，editors，POPL（2005），pp.110-121[6] Godefroid，P.，N. Klarlund和K. Sen，DART：Directed Automated Random Testing，in：Proceedingsof the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation（PLDI2005），pp. 213-223[7] K ahkonen，K.，T. 劳尼艾宁岛Saarikivi，J. Kauttio，K. 赫尔扬·科和我。Niemel，LCT：Ano pensourceconcolic testing tool for Java programs ， in ： Proceedings of the 6th Workshop on BytecodeSemantics，Verification，Analysis and Transformation（BYTECODE'2011），2011，pp. 75比80[8] Saarikivi， O.，K. Küahküonen 和K.Heljan ko， Imp roving dynamicpartialorderreductionsforconcolictesting， in ： Proceedings of the 12th International Conference on Application of Concurrency toSystem Design（ACSD '2012）（2012）。URLhttp://users.ics.aalto.fi/osaariki/lct-improving-dpor.pdf[9] Sen，K.，“Scalable automated methods for dynamic program analysis,” Doctoral thesis, Universityof Illinois[10] 瓦 尔 利 雷 河 ，P. Co ， E. 加 尼 翁 湖J. 亨 德 尔 山 口Lam 和 V. Sundaresan ， S oot-aJavabytecodeoptimization framework，in：Proceedings of the 1999 conference of the Centre for AdvancedStudies on Collaborative Research（CASCON 1999）（1999），p. 13.[11] 杨，Y.，X. Chen，G. Gopalakrishnan和R. M. Kirby，基于分布式动态偏序约简的线程软件验证，在：D。Bosnacki和S. Edelkamp，editors，SPIN，Lecture Notes in Computer Science4595（2007），pp.58比75