On-the-fly data race detection for OpenSHMEM programs

Klotz, Sven; Müller, Matthias S.; Schwitanski, Simon; Katoen, Joost-Pieter

doi:10.18154/RWTH-2023-05644

On-the-fly data race detection for OpenSHMEM programs = Konzepte zur Laufzeiterkennung von kritischem Wettlauf für OpenSHMEM-Programme

Klotz, Sven^RWTH*

2023

VerantwortlichkeitsangabeSven Klotz

ImpressumAachen : RWTH Aachen University 2023

Umfang1 Online-Ressource : Diagramme

Bachelorarbeit, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Müller, Matthias S. (Thesis advisor)^RWTH* ; Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Schwitanski, Simon (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2023-06-06

Online
DOI: 10.18154/RWTH-2023-05644
URL: https://publications.rwth-aachen.de/record/959491/files/959491.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
HPC (frei) ; OpenSHMEM (frei) ; correctness checking (frei) ; data races (frei) ; one-sided communication (frei) ; remote memory access (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
OpenSHMEM is a distributed-memory programming model part of the Partitioned Global Address Space family of programming models. It provides vendors with a standard Application Programming Interface to implement SHMEM libraries and facilitates the portability and predictability of OpenSHMEM applications. The OpenSHMEM effort aims to imitate the success of the widely used Message Passing Interfacing programming model while focusing exclusively on one-sided communication. One-sided communication or Remote Memory Access enables a process to directly access and modify memory regions of a remote process without actively involving the remote process. Although OpenSHMEM’s one-sided communication has many significant desirable properties, it also has drawbacks. Specifically, the one-sidednature of this communication results in applications being prone to contain data races as the remote process is unaware of the remote memory accesses. To prevent this, a developer must ensure proper synchronization between all types of memory accesses, remote or local. This thesis discusses the semantics of OpenSHMEM communication and synchronization and classifies what constitutes a data race within an OpenSHMEM program. Based on this definition, a semantics-driven search for data races in this thesis results in 35 data race test cases that are classified and labeled as many share common properties. Additionally, this thesis uses the insights gained from semantics-driven search to formalize the notion of data races by adapting an existing semi-formal model of the MPI RMA semantics to OpenSHMEM. Based on this model, this thesis presents the concepts required for on-the-fly data race detection in OpenSHMEM programs and a prototype data race detection tool for OpenSHMEM based on this on-the-fly method. The approach performs happens-before analysis using vector clocks and uses memory consistency rules to determine the earliest and latest points in logical time when a memory access could occur. The prototype annotates these memory accesses in a shared-memory race detector that performs the actual race detection. A separate race detection covers only special cases. Lastly, this thesis evaluates the prototype using the data race test cases developed for this thesis. The results of this evaluation are promising for our prototype as it achieved an accuracy of 0.86. This shows that the on-the-fly data race detection approach works in practice for OpenSHMEM.

OpenAccess:
PDF
(zusätzliche Dateien)