guest ::
A modular LLVM-based contract framework for parallel programming models = Ein modulares LLVM-basiertes Vertragssystem für parallele Programmiermodelle
2025
Masterarbeit, RWTH Aachen University, 2025
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
; ; ; ; ;
Tag der mündlichen Prüfung/Habilitation
2025-03-05
Online
URL: https://publications.rwth-aachen.de/record/1014244/files/1014244.pdf
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Parallel programming models such as the Message Passing Interface (MPI) and OpenSHMEM facilitate the use of distributed-memory computers. While powerful, these models are error-prone: Users may forget the MPI initialization, do not initialize a datatype, or leak a request handle. Thus, a lot of work has gone into dynamic correctness checking tools such as MUST, PARCOACH and ITAC, which, while possessing great accuracy, cause significant runtime overhead. Static tools, which perform analysis at compile time, avoid this overhead but trade it for lower accuracy. Additionally, most correctness checkers are inflexible, supporting only one parallel programming model of many, where adding support for another is generally nontrivial. This thesis proposes the use of contracts to verify the correct usage of parallel programming models. Contracts are a way to annotate user-defined rules in code for the compiler to check. The analyses that run to verify the contracts apply to any contract defined, and thus are not bound to a set of known programming models. By introducing a suitably powerful contract syntax the API requirements of the parallel programming model can be embedded directly into the code, and analysis can be performed regardless of the model used. This thesis aims to perform contract verification for parallel programs at compile-time using LLVM, enabling fast checking and debugging of some error classes such as local data races, handle lifecycle errors and more. The contracts embed the API specifications of each programming model using MPI and OpenSHMEM as examples. We use contracts for extensibility: New checks and support for other models can be easily implemented using additional contract annotations. By performing analysis using the LLVM IR future development may allow additional programming languages to be used with the same analysis framework. The analyses are implemented using efficient data flow analysis, with each analysis relying on the same generic worklist algorithm. Additionally, we evaluate our tool against other static checkers on known correctness benchmarks RMARaceBench and MPI-BugBench, as well as discuss compilation overhead using the proxy applications LULESH, miniVite and the PRK Stencil Kernel. In our testing, our approach improves accuracy through wider error coverage with a compile-time overhead of around 2-3x, comparable to or improving upon the other tools tested.
Restricted: 
PDF
(additional files)
Dokumenttyp
Master Thesis
Herkunft
Public Reference
Sprache
English
Interne Identnummern
RWTH-2025-05969
Datensatz-ID: 1014244
Beteiligte Länder
Germany
|
The record appears in these collections: |