Automatic loop invariant generation for data dependence analysis

• Main Authors: Tabar, Asmae Heydari, Bubel, Richard, Hähnle, Reiner
• Format: Conference Proceeding
• Language: English
• Subjects: Abstraction; Invariants; Automation; Behavioral sciences; Codes; Computing methodologies > Parallel computing methodologies > Parallel algorithms > Massively parallel algorithms; Computing methodologies→Massively parallel algorithms; Formal software verification; Java; Parallel algorithms; Software; Software and its engineering > Software creation and management > Software verification and validation > Formal software verification; Software and its engineering > Software organization and properties > Software functional properties > Formal methods > Software verification; Software and its engineering→Software verification; Static analysis; Theory of computation > Logic > Programming logic; Theory of computation > Semantics and reasoning > Program reasoning > Abstraction; Theory of computation > Semantics and reasoning > Program reasoning > Invariants; Theory of computation→Programming logic
• ISSN: 2575-5099
• DOI: 10.1145/3524482.3527649

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.