Modeling synchronization and consistency for data race detection in remote memory access programs

Schwitanski, Simon; Müller, Matthias S.; Schulz, Martin

doi:44131

Modeling synchronization and consistency for data race detection in remote memory access programs

Schwitanski, Simon^RWTH*

2025

Verantwortlichkeitsangabevorgelegt von Simon Schwitanski, Master of Science

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Müller, Matthias S. (Thesis advisor)^RWTH* ; Schulz, Martin (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2025-02-05

Online
DOI: 10.18154/RWTH-2024-11180
URL: https://publications.rwth-aachen.de/record/998167/files/998167.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
HPC (frei) ; RMA (frei) ; correctness (frei) ; data races (frei) ; memory consistency (frei) ; synchronziation (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Der stetig wachsende Parallelismus in heutigen Supercomputern erfordert skalierbare, parallele Programmiermethoden mit effizienten Kommunikationsmodellen. Das traditionelle Kommunikationsmodell im wissenschaftlichen Rechnen ist der Nachrichtenaustausch: Sowohl der sendende als auch der empfangende Prozess ist aktiv am Datenaustausch über Nachrichten beteiligt. Remote-Memory-Access-Modelle (RMA) stellen eine alternative Kommunikationsmethode bereit, in der Prozesse direkt auf den Speicher von anderen Prozessen zugreifen. RMA-Modelle vermeiden unnötige Synchronisation zwischen Prozessen und erzielen in modernen Supercomputern eine bessere Leistung als der klassische Nachrichtenaustausch. Sie erfordern jedoch, dass der Nutzer explizit Synchronisation und Konsistenz der Speicherzugriffe durch entsprechende API-Aufrufe sicherstellt. Andernfalls führen gleichzeitige, im Konflikt stehende Speicherzugriffe zu Data Races mit undefiniertem Verhalten. Der Nichtdeterminismus von Data Races, bekannt von Shared-Memory-Programmierung, macht ihre manuelle Erkennung komplex. Diese Arbeit untersucht Data Races in RMA-Programmen und präsentiert neue skalierbare Methoden, um diese zur Laufzeit zu erkennen. Eine Klassifikation von Data Races in den RMA-Modellen MPI RMA, OpenSHMEM und GASPI zeigt, dass Synchronisation und Konsistenz die wesentlichen Eigenschaften zur Data-Race-Erkennung in RMA sind, die ein Korrektheitsanalysewerkzeug untersuchen muss. Diese Arbeit definiert formale Modelle, die die Analyse von beiden Eigenschaften in RMA-Programmen ermöglichen. Das Synchronisationsmodell analysiert die Happened-Before-Relation von Ereignissen mithilfe eines Vektoruhraustauschs. Dieser zeichnet den Synchronisationszustand von Prozessen zur Laufzeit auf. Das Konsistenzmodell formalisiert eine Relation, die definiert, wann ein RMA-Zugriff garantiert abgeschlossen ist. Beide Modelle werden in einem generalisierten Modell zur Laufzeiterkennung von Data Races in RMA-Programmen, unabhängig vom konkret genutzten RMA-Modell, kombiniert. Das entwickelte Modell zur Erkennung von Data Races ist im Werkzeug RMASanitizer implementiert. Es kombiniert ThreadSanitizer, ein Werkzeug zur Erkennung von Data Races in Shared-Memory-Programmen, mit dem Korrektheitsanalysewerkzeug MUST, um Data Races in MPI RMA, OpenSHMEM und GASPI zur Laufzeit zu erkennen. Zur Evaluation wird RMARaceBench entwickelt, ein Benchmark zur Analyse der Klassifikationsqualität, der die Erkennungsgenauigkeit von Werkzeugen zur Race-Erkennung in RMA quantifiziert. Die Evaluation mit RMARaceBench zeigt, dass RMASanitizer die höchste Erkennungsgenauigkeit verglichen mit anderen Werkzeugen hat. Eine Overheaduntersuchung mit RMA-Proxy-Applikationen, die mit mehr als 700 Prozessen ausgeführt werden, zeigt, dass RMASanitizer in hochskalierenden Anwendungen nutzbar ist.

The increasing parallelism in today's supercomputers requires scalable parallel programming methods with efficient communication models. The traditional communication model in scientific computing is message passing: Both the sending and the receiving processes participate actively in the data exchange via messages. Remote Memory Access (RMA) models provide an alternative communication method where processes can access the memory of other processes directly. RMA models avoid unnecessary synchronization between processes and outperform the traditional message-passing model in modern supercomputers. However, they require users to explicitly ensure the synchronization and consistency of memory accesses through corresponding API calls. Otherwise, concurrent conflicting memory accesses lead to data races with undefined behavior. The non-deterministic nature of data races, commonly known from shared-memory programming, makes their manual detection difficult.This thesis investigates data races in RMA programs and provides novel scalable methods to detect them at runtime. A classification of data races in the RMA models MPI RMA, OpenSHMEM, and GASPI shows that synchronization and consistency are the two key properties that a correctness tool must capture to identify RMA races. This thesis provides formal models that allow analyzing both properties in RMA programs. The synchronization model analyzes the happened-before relation of events using a vector clock exchange. It captures the synchronization state of processes at runtime. The consistency model formalizes a relation defining when a remote memory access is guaranteed to be completed. Both models are combined in a generalized on-the-fly race detection model that can detect RMA data races independent of the concrete RMA model used in an application.The developed race detection model is implemented in a tool named RMASanitizer. It combines the shared-memory race detector ThreadSanitizer with the correctness checking tool MUST to detect RMA data races in MPI RMA, OpenSHMEM, and GASPI at runtime. For the evaluation, this thesis provides RMARaceBench, a classification quality benchmark suite designed to quantify the detection accuracy of RMA race detection tools. The evaluation with RMARaceBench shows that RMASanitizer has the highest detection accuracy compared to other state-of-the-art RMA race detectors. An overhead study with RMA proxy applications running with more than 700 processes shows that RMASanitizer is applicable to large-scale workloads.

OpenAccess:
PDF
(additional files)