Heydari Tabar, Asmae (2024)
Automatic Data Dependence Analysis by Deductive Verification.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00026722
Ph.D. Thesis, Primary publication, Publisher's Version
Text
PhDThesis-AHT-Final.pdf Copyright Information: CC BY 4.0 International - Creative Commons, Attribution. Download (2MB) |
Item Type: | Ph.D. Thesis | ||||
---|---|---|---|---|---|
Type of entry: | Primary publication | ||||
Title: | Automatic Data Dependence Analysis by Deductive Verification | ||||
Language: | English | ||||
Referees: | Hähnle, Prof. Dr. Reiner ; Rümmer, Prof. Dr. Philipp | ||||
Date: | 6 August 2024 | ||||
Place of Publication: | Darmstadt | ||||
Collation: | xxv, 164 Seiten | ||||
Date of oral examination: | 24 April 2024 | ||||
DOI: | 10.26083/tuprints-00026722 | ||||
Abstract: | In the realm of High-Performance Computing (HPC), the parallelization of programs holds significant importance. However, the correctness of parallelization hinges on the reliable exclusion of certain data dependences, such as read-after-write dependences, where a read access follows a write access on a given memory location. It is imperative that data dependence analyses are not only correct but also as precise as possible to seize every opportunity for parallelization. While various static, dynamic, and hybrid analysis approaches have been proposed within the HPC community, none have been based on program logic and deductive verification, despite the significant advantages this approach offers, including soundness, precision, and modularity. In this thesis, we present an automatic, sound, and highly precise approach to generate data dependences based on deductive verification. We define a program logic based on precise semantics for data dependences. As loops are usually the main source of parallelization in HPC applications, we equip our approach with an automatic loop invariant generation technique in the same program logic. To achieve full automation, we incorporate predicate abstraction tailored to the needs of data dependence analysis. To retain as much precision as possible, we generalize logic-based symbolic execution to compute abstract data dependence predicates. We provide a prototype demonstrating that fully automatic data dependence analysis based on deductive verification is feasible and is a promising alternative to the dependence analyses commonly used in HPC. Implementing our approach for Java atop a deductive verification tool, we conducted evaluations demonstrating its ability to analyze data dependences highly precisely for representative code extracted from HPC applications. |
||||
Alternative Abstract: |
|
||||
Status: | Publisher's Version | ||||
URN: | urn:nbn:de:tuda-tuprints-267225 | ||||
Classification DDC: | 000 Generalities, computers, information > 004 Computer science | ||||
Divisions: | 20 Department of Computer Science > Software Engineering | ||||
Date Deposited: | 06 Aug 2024 12:16 | ||||
Last Modified: | 08 Aug 2024 07:33 | ||||
URI: | https://tuprints.ulb.tu-darmstadt.de/id/eprint/26722 | ||||
PPN: | 520395255 | ||||
Export: |
View Item |