Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

邮发代号 80-970

2019 Impact Factor: 1.275

Frontiers of Computer Science  2018, Vol. 12 Issue (1): 86-100   https://doi.org/10.1007/s11704-016-5459-9
  本期目录
Tuning parallel symbolic execution engine for better performance
Anil Kumar KARNA1(), Jinbo DU2, Haihao SHEN3, Hao ZHONG1, Jiong GONG3, Haibo YU2, Xiangning MA3, Jianjun ZHAO4
1. Department of Computer Science, Shanghai Jiao Tong University, Shanghai 200240, China
2. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China
3. Intel Asia-Pacific Research and Development Ltd., Shanghai 200240, China
4. Department of Advanced Information Technology, Kyushu University, Fukuoka 819-0395, Japan
 全文: PDF(859 KB)  
Abstract

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 tun 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.

Key wordscode analysis    symbolic execution    parallelizing symbolic execution    KLEE    Cloud9
收稿日期: 2015-11-01      出版日期: 2018-01-12
Corresponding Author(s): Anil Kumar KARNA   
 引用本文:   
. [J]. Frontiers of Computer Science, 2018, 12(1): 86-100.
Anil Kumar KARNA, Jinbo DU, Haihao SHEN, Hao ZHONG, Jiong GONG, Haibo YU, Xiangning MA, Jianjun ZHAO. Tuning parallel symbolic execution engine for better performance. Front. Comput. Sci., 2018, 12(1): 86-100.
 链接本文:  
https://academic.hep.com.cn/fcs/CN/10.1007/s11704-016-5459-9
https://academic.hep.com.cn/fcs/CN/Y2018/V12/I1/86
1 Ciortea L, Zamfir C, Bucur S, Chipounov V, Candea G. Cloud9: a software testing service. ACM SIGOPS Operating Systems Review, 2010, 43(4): 5–10
https://doi.org/10.1145/1713254.1713257
2 Staats M, Pˇašareanu C S. Parallel symbolic execution for structural testgeneration. In: Proceedings of the 19th International Symposium on Software Testing and Analysis. 2010, 183–194
3 King A. Distributed parallel symbolic execution. Dissertation for the Doctoral Degree. Manhattan, KS: Kansas State University, 2009
4 Siddiqui J H, Khurshid S. ParSym: Parallel symbolic execution. In: Proceedings of the 2nd International Conference on Software Technology and Engineering. 2010, 405–409
https://doi.org/10.1109/ICSTE.2010.5608866
5 Sasnauskas R, Dustmann O S, Kaminski B L, Wehrle K, Weise C, Kowalewski S. Scalable symbolic execution of distributed systems. In: Proceedings of the 31st International Conference on Distributed Computing Systems. 2011, 333–342
https://doi.org/10.1109/ICDCS.2011.28
6 Griesmayer A, Aichernig B, Johnsen E B, Schlatte R. Dynamic symbolic execution of distributed concurrent objects. In: Lee D, Lopes A, Poetzsch-Heffter A, eds. Formal Techniques for Distributed Systems. Berlin: Springer, 2009, 225–230
https://doi.org/10.1007/978-3-642-02138-1_16
7 Aleb N, Kechid S. A new approach for distributed symbolic software testing. In: Proceedings of International Conference on Computational Science and Its Applications. 2013, 487–497
https://doi.org/10.1007/978-3-642-39643-4_35
8 Cadar C, Dunbar D, Engler D R. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceeding of OSDI. 2008, 209–224
9 Bucur S, Ureche V, Zamfir C, Candea G. Parallel symbolic execution for automated real-world software testing. In: Proceedings of the 6th ACM Conference on Computer Systems. 2011, 183–198
https://doi.org/10.1145/1966445.1966463
10 Candea G, Bucur S, Zamfir C. Automated software testing as a service. In: Proceedings of the 1st ACM Symposium on Cloud Computing. 2010, 155–160
https://doi.org/10.1145/1807128.1807153
11 Renshaw D, Kong S. Symbolic execution in difficult environments. Technical Report 15-745. 2011
12 Marinescu P D, Cadar C. Make test-zesti: A symbolic execution solution for improving regression testing. In: Proceedings of the 34th International Conference on Software Engineering. 2012, 716–726
https://doi.org/10.1109/ICSE.2012.6227146
13 Cui H M, Hu G, Wu J Y, Yang J. Verifying systems rules using ruledirected symbolic execution. ACM SIGPLAN Notices, 2013, 48(4): 329–342
https://doi.org/10.1145/2499368.2451152
14 Zhang D Z, Liu D G, Lei Y, Kung D, Csallner C, Wang W H. Detecting vulnerabilities in c programs using trace-based testing. In: Proceedings of IEEE/IFIP International Conference on Dependable Systems and Networks. 2010, 241–250
15 Zitser M, Lippmann R, Leek T. Testing static analysis tools using exploitable buffer overflows from open source code. ACM SIGSOFT Software Engineering Notes, 2004, 29(6): 97–106
https://doi.org/10.1145/1041685.1029911
16 Saxena P, Poosankam P, McCamant S, Song D. Loop-extended symbolic execution on binary programs. In: Proceedings of the 18th ACM International Symposium on Software Testing and Analysis. 2009, 225–236
https://doi.org/10.21236/ADA538843
17 Jaffar J, Murali V, Navas J A, Santosa A E. TRACER: a symbolic execution tool for verification. In: Proceedings of the 24th International Conference on Computer Aided Verification. 2012, 758–766
https://doi.org/10.1007/978-3-642-31424-7_61
18 Coward P D. Symbolic execution systems-a review. Software Engineering Journal, 1988, 3(6): 229–239
https://doi.org/10.1049/sej.1988.0029
19 King J C. Symbolic execution and program testing. Communications of the ACM, 1976, 19(7): 385–394
https://doi.org/10.1145/360248.360252
20 Sen K, Marinov D, Agha G. CUTE: a concolic unit testing engine for C. ACMSIGSOFT Software Engineering Notes, 2005, 30(5): 263–272
https://doi.org/10.1145/1095430.1081750
21 Zhang Y F, Chen Z B, Wang J. Speculative symbolic execution. In: Proceedings of the 23rd IEEE International Symposium on Software Reliability Engineering. 2012, 101–110
https://doi.org/10.1109/ISSRE.2012.8
22 Palikareva H, Cadar C. Multi-solver support in symbolic execution. In: Proceedings of International Conference on Computer Aided Verification. 2013, 53–68
https://doi.org/10.1007/978-3-642-39799-8_3
[1] Supplementary Material Download
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed