一句话:提出乐观混合分析,用不可靠静态分析与运行时不变量验证加速动态分析,同时保持精度与可靠性。
动态分析可检测数据竞争、内存安全和信息流,但速度慢;传统混合分析依赖可靠静态分析减少动态工作。本文指出,保持动态分析可靠并不要求静态分析可靠:对静态分析所考虑状态内的执行仍可可靠分析。据此提出乐观混合分析:先剖析少量执行生成大概率不变量,再用更精确但不可靠的静态分析假设其成立,随后推测运行动态分析并验证该执行中不变量,失败则回退传统混合分析重新执行。结果与动态分析同样精确可靠,但通常更快,因为不可靠静态分析加速更大且验证很少失败。用于竞争检测和切片,分别比 FastTrack 快 1.8 倍、比 Giri 快 8.3 倍。
Dynamic analysis tools, such as those that detect data-races, verify memory safety, and identify information flow, have become a vital part of testing and debugging complex software systems. While these tools are powerful, their slow speed often limits how effectively they can be deployed in practice. Hybrid analysis speeds up these tools by using static analysis to decrease the work performed during dynamic analysis. In this paper we argue that current hybrid analysis is needlessly hampered by an incorrect assumption that preserving the soundness of dynamic analysis requires an underlying sound static analysis. We observe that, even with unsound static analysis, it is possible to achieve sound dynamic analysis for the executions which fall within the set of states statically considered. This leads us to a new approach, called optimistic hybrid analysis. We first profile a small set of executions and generate a set of likely invariants that hold true during most, but not necessarily all, executions. Next, we apply a much more precise, but unsound, static analysis that assumes these invariants hold true. Finally, we run the resulting dynamic analysis speculatively while verifying whether the assumed invariants hold true during that particular execution; if not, the program is reexecuted with a traditional hybrid analysis. Optimistic hybrid analysis is as precise and sound as traditional dynamic analysis, but is typically much faster because (1) unsound static analysis can speed up dynamic analysis much more than sound static analysis can and (2) verifications rarely fail. We apply optimistic hybrid analysis to race detection and program slicing and achieve 1.8x over a state-of-the-art race detector (FastTrack) optimized with traditional hybrid analysis and 8.3x over a hybrid backward slicer (Giri).
DOI 原文 ·
@inproceedings{paperbot4297,
title = {Optimistic Hybrid Analysis},
author = {David Devecsery and Peter M. Chen and Jason Flinn and Satish Narayanasamy},
booktitle = {ASPLOS},
year = {2018},
doi = {10.1145/3173162.3177153}
}