Graspan: A single-machine disk-based graph system for interprocedural static analyses of large-scale systems code

被引：63
作者：
Wang K. [1 ]
Hussain A. [1 ]
Zuo Z. [1 ]
Xu G. [1 ]
Amiri Sani A. [1 ]
机构：
[1] University of California, Irvine, CA
来源：
ACM SIGPLAN Notices | 2017年 / 52卷 / 04期
基金：
美国国家科学基金会;
关键词：
Disk-based systems; Graph processing; Static analysis;
D O I：
10.1145/3037697.3037744
中图分类号：
学科分类号：
摘要：
There is more than a decade-long history of using static analysis to find bugs in systems such as Linux. Most of the existing static analyses developed for these systems are simple checkers that find bugs based on pattern matching. Despite the presence of many sophisticated interprocedural analyses, few of them have been employed to improve checkers for systems code due to their complex implementations and poor scalability. In this paper, we revisit the scalability problem of interprocedural static analysis from a "Big Data" perspective. That is, we turn sophisticated code analysis into Big Data analytics and leverage novel data processing techniques to solve this traditional programming language problem. We develop Graspan, a disk-based parallel graph system that uses an edge-pair centric computation model to compute dynamic transitive closures on very large program graphs. We implement context-sensitive pointer/alias and dataflow analyses on Graspan. An evaluation of these analyses on large codebases such as Linux shows that their Graspan implementations scale to millions of lines of code and are much simpler than their original implementations. Moreover, we show that these analyses can be used to augment the existing checkers; these augmented checkers uncovered 132 new NULL pointer bugs and 1308 unnecessary NULL tests in Linux 4.4.0-rc5, PostgreSQL 8.3.9, and Apache httpd 2.2.18. © 2017 ACM.
引用
收藏
页码：389 / 404
页数：15
相关论文
共 102 条
[11]  
Alur R., Benedikt M., Etessami K., Godefroid P., Reps T., Yannakakis M., Analysis of recursive state machines, ACM Trans. Program. Lang. Syst., 27, 4, pp. 786-818, (2005)
[12]  
Alur R., Madhusudan P., Visibly pushdown languages, STOC, pp. 202-211, (2004)
[13]  
Atkinson M.D., Sack J.-R., Santoro N., Strothotte T., Min-max heaps and generalized priority queues, Commun ACM, 29, 10, pp. 996-1000, (1986)
[14]  
Ball T., Cook B., Levin V., Rajamani S.K., Slam and static driver verifier: Technology transfer of formal methods inside microsoft, IFM, pp. 1-20, (2004)
[15]  
Ball T., Majumdar R., Millstein T., Rajamani S.K., Automatic predicate abstraction of c programs, PLDI, pp. 203-213, (2001)
[16]  
Bastani O., Anand S., Aiken A., Specification inference using context-free language reachability, POPL, pp. 553-566, (2015)
[17]  
Bravenboer M., Smaragdakis Y., Strictly declarative specification of sophisticated points-to analyses, OOPSLA, pp. 243-262, (2009)
[18]  
Brown F., Notzli A., Engler D., How to build static checking systems using orders of magnitude less code, ASPLOS, pp. 143-157, (2016)
[19]  
Bugrara S., Aiken A., Verifying the safety of user pointer dereferences, IEEE S&P, pp. 325-338, (2008)
[20]  
Cadar C., Dunbar D., Engler D., Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs, OSDI, pp. 209-224, (2008)
12345678910