Tuning parallel symbolic execution engine for better performance

Anil Kumar Karna, Jinbo Du, Haihao Shen, Hao Zhong, Jiong Gong, Haibo Yu, Xiangning Ma, Jianjun Zhao

Research output: Contribution to journalArticle

1 Citation (Scopus)

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

Original languageEnglish
Pages (from-to)86-100
Number of pages15
JournalFrontiers of Computer Science
Volume12
Issue number1
DOIs
Publication statusPublished - Feb 1 2018

Fingerprint

Symbolic Execution
Tuning
Engine
Engines
Benchmark
Cache
Field Study
Communication
Evaluation
Execution Time
Testing
Path

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tuning parallel symbolic execution engine for better performance. / Karna, Anil Kumar; Du, Jinbo; Shen, Haihao; Zhong, Hao; Gong, Jiong; Yu, Haibo; Ma, Xiangning; Zhao, Jianjun.

In: Frontiers of Computer Science, Vol. 12, No. 1, 01.02.2018, p. 86-100.

Research output: Contribution to journalArticle

Karna, AK, Du, J, Shen, H, Zhong, H, Gong, J, Yu, H, Ma, X & Zhao, J 2018, 'Tuning parallel symbolic execution engine for better performance', Frontiers of Computer Science, vol. 12, no. 1, pp. 86-100. https://doi.org/10.1007/s11704-016-5459-9
Karna, Anil Kumar ; Du, Jinbo ; Shen, Haihao ; Zhong, Hao ; Gong, Jiong ; Yu, Haibo ; Ma, Xiangning ; Zhao, Jianjun. / Tuning parallel symbolic execution engine for better performance. In: Frontiers of Computer Science. 2018 ; Vol. 12, No. 1. pp. 86-100.
@article{921d59f9b712402ca655460a29886443,
title = "Tuning parallel symbolic execution engine for better performance",
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 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.",
author = "Karna, {Anil Kumar} and Jinbo Du and Haihao Shen and Hao Zhong and Jiong Gong and Haibo Yu and Xiangning Ma and Jianjun Zhao",
year = "2018",
month = "2",
day = "1",
doi = "10.1007/s11704-016-5459-9",
language = "English",
volume = "12",
pages = "86--100",
journal = "Frontiers of Computer Science",
issn = "2095-2228",
publisher = "Springer Science + Business Media",
number = "1",

}

TY - JOUR

T1 - Tuning parallel symbolic execution engine for better performance

AU - Karna, Anil Kumar

AU - Du, Jinbo

AU - Shen, Haihao

AU - Zhong, Hao

AU - Gong, Jiong

AU - Yu, Haibo

AU - Ma, Xiangning

AU - Zhao, Jianjun

PY - 2018/2/1

Y1 - 2018/2/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=85029497781&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85029497781&partnerID=8YFLogxK

U2 - 10.1007/s11704-016-5459-9

DO - 10.1007/s11704-016-5459-9

M3 - Article

AN - SCOPUS:85029497781

VL - 12

SP - 86

EP - 100

JO - Frontiers of Computer Science

JF - Frontiers of Computer Science

SN - 2095-2228

IS - 1

ER -