Automatic Loop Invariant Generation for Data Dependence Analysis
2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)(2022)
摘要
Parallelization of programs relies on sound and precise analysis of data dependences in the code, specifically, when dealing with loops. State-of-art tools are based on dynamic profiling and static analysis. They tend to over- and, occasionally, to under-approximate dependences. The former misses parallelization opportunities, the latter can change the behavior of the parallelized program. In this paper we present a sound and highly precise approach to generate data dependences based on deductive verification. The central technique is to infer a specific form of loop invariant tailored to express dependences. To achieve full automation, we adapt predicate abstraction in a suitable manner. To retain as much precision as possible, we generalized logic-based symbolic execution to compute abstract dependence predicates. We implemented our approach for Java on top of a deductive verification tool. The evaluation shows that our approach can generate highly precise data dependences for representative code taken from HPC applications.
更多查看译文
关键词
• Computing methodologies→Massively parallel algorithms,• Software and its engineering→Software verification, Formal software verification,• Theory of computation→Programming logic, Abstraction, Invariants
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要