Tuning parallel symbolic execution engine for better performance
Tuning parallel symbolic execution engine for better performance
复制标题
调整并行符号执行引擎以获得更好的性能
DOI：
10.1007/s11704-016-5459-9
复制
发表时间：
2018-01
影响因子：
4.2
通讯作者：
Zhao Jianjun
中科院分区：
文献类型：
--
作者：
Karna Anil Kumar;du Jinbo;Shen Haihao;Zhong Hao;Gong Jiong;Yu Haibo;Ma Xiangning;Zhao Jianjun
符号执行广泛用于许多代码分析、测试和验证工具。由于符号执行会穷尽地探索所有可行的路径，因此非常耗时。为了解决这个问题，研究人员已经改进了现有的符号执行工具（例如，KLEE）。特别是，Cloud9是一种广泛使用的符号执行工具，研究人员已经使用该工具分析了真实的代码。然而，研究人员批评说，像Cloud9这样的工具仍然无法分析大规模代码。本文对Cloud 9进行了实地研究，使用KLEE和Cloud 9对C中的基准测试进行了分析。我们的结果证实了批评。基于结果，我们确定了阻碍Cloud9性能的三个瓶颈：通信时间间隔、作业传输策略和已解决约束的该高速缓存管理。为了解决这些问题，我们调整通信时间间隔更好的参数，修改作业传输策略，并实现了解决约束的缓存管理方法。我们对我们的基准和一个真实的应用程序进行两次评估，以了解我们的改进。我们的结果表明，我们调优的Cloud9显着减少了执行时间，无论是在我们的基准测试和真实的应用程序。此外，我们的评估结果表明，我们的调整技术提高了所有设备上的有效性，并且可以实现高达五倍的改善，这取决于我们的方法的调整值和测试下的程序的行为。
Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execution exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have paralleled existing symbolic execution tools (e.g., KLEE). In particular, Cloud9 is a widely used paralleled symbolic execution tool, and researchers have used the tool to analyze real code. However, researchers criticize that tools such as Cloud9 still cannot analyze large scale code. In this paper, we conduct a field study on Cloud9, in which we use KLEE and Cloud9 to analyze benchmarks in C. Our results confirm the criticism. Based on the results, we identify three bottlenecks that hinder the performance of Cloud9: the communication time gap, the job transfer policy, and the cache management of the solved constraints. To handle these problems, we tune the communication time gap with better parameters, modify the job transfer policy, and implement an approach for cache management of solved constraints. We conduct two evaluations on our benchmarks and a real application to understand our improvements. Our results show that our tuned Cloud9 reduces the execution time significantly, both on our benchmarks and the real application. Furthermore, our evaluation results show that our tuning techniques improve the effectiveness on all the devices, and the improvement can be achieved upto five times, depending upon a tuning value of our approach and the behaviour of program under test.
登录
查看更多内容
DOI：
10.1145/1831708.1831732
发表时间：
2010-07
期刊：
--
影响因子：
--
作者：
Matthew Staats;C. Păsăreanu
通讯作者：
Matthew Staats;C. Păsăreanu
DOI：
10.1145/1029894.1029911
发表时间：
2004-10
期刊：
--
影响因子：
--
作者：
Misha Zitser;R. Lippmann;T. Leek
通讯作者：
Misha Zitser;R. Lippmann;T. Leek
DOI：
10.1145/2451116.2451152
发表时间：
2013-03
期刊：
--
影响因子：
--
作者：
Heming Cui;Gang Hu;Jingyue Wu;Junfeng Yang
通讯作者：
Heming Cui;Gang Hu;Jingyue Wu;Junfeng Yang
DOI：
10.1109/issre.2012.8
发表时间：
2012-05
期刊：
2012 IEEE 23rd International Symposium on Software Reliability Engineering
影响因子：
--
作者：
Yufeng Zhang;Zhenbang Chen;Ji Wang
通讯作者：
Yufeng Zhang;Zhenbang Chen;Ji Wang
DOI：
10.1109/icdcs.2011.28
发表时间：
2011-06
期刊：
2011 31st International Conference on Distributed Computing Systems
影响因子：
--
作者：
Raimondas Sasnauskas;Oscar Soria Dustmann;Benjamin Lucien Kaminski;Klaus Wehrle;Carsten Weise;S. Kowalewski
通讯作者：
Raimondas Sasnauskas;Oscar Soria Dustmann;Benjamin Lucien Kaminski;Klaus Wehrle;Carsten Weise;S. Kowalewski