Loading…
Higher-Order Nested Data Parallelism: Semantics and Implementation
Leshchinskiy, Roman
Das veschachtelt datenparallele Programmiermodell ist ein attraktiver Ansatz zur Entwicklung von Software für massiv parallele Systeme. Das Modell erlaubt es, komplexes paralleles Verhalten durch verschachtelte kollektive Operationen zu spezifizieren, ohne maschinennahe Details wie Synchronisation oder Kommunikation betrachten zu müssen. Dieses hohe Abstraktionsniveau wird erreicht, indem die Aufgabe leicht parallelisierbare Repräsentationen von Datenstrukturen abzuleiten und Berechnungen entsprechend zu transformieren, vom Programmierer auf den Compiler übertragen wird. Dies wird durch die Flattening-Transformation ermöglicht, die verschachtelten Parallelismus eliminiert und flache datenparallele Programme erzeugt. Letztere können mit Hilfe von einer Reihe bekannter Techniken optimiert und schließlich effizient auf modernen parallelen Rechnern ausgeführt werden. Die Korrektheit von Flattening hängt entscheidend von der referenziellen Transparenz der Quellsprache ab. Allerdings war die Benutzbarkeit der Transformation in einem rein funktionalen Ansatz stark eingeschränkt, da sie Funktionen höherer Ordnung nicht behandeln konnte. Die vorliegende Dissertation führt diese Einschränkung auf das in der Standardsemantik der Lambda-Kalküls inhärente Vermischen von Berechnungen und Daten zurück und zeigt auf, wie diese Problem durch eine Kombination von Flattening mit Closure Conversion gelöst werden kann. Closure Conversion ist eine bekannte Programmtransformation, die genau die erforderlich Trennung zwischen Code und Daten vornimmt. Zur Validierung des Ansatzes wird eine repräsentative Menge von parallelen Operationen betrachtet und aufgezeigt, wird diese erweitern werden können, um Funktionen höherer Ordnung in durch Closure Conversion transformierten Programmen zu unterstützen. Ferner enthält die Dissertation eine detaillierte Untersuchung der Interaktionen zwischen Flattening und nicht-strikter Auswertung. Diese sind recht komplex, da die durch die Transformation erzeugten Datenstrukturen auf strikten Vektoren basieren. Durch eine im Vergleich zu früheren Arbeiten modifizierte Definition der Flattening-Transformation können nicht-strikte Programme trotzdem korrekt übersetzt werden. Schließlich wird die Korrektheit von Flattening für eine nicht-strikte Sprache mit Funktionen höherer Ordnung beweisen. Für den Beweis wird eine neue Form des Lambda-Kalküls eingeführt, in der die Trennung zwischen Berechnungen und Daten syntaktisch sichergestellt wird. Diese Ergebnisse erlauben es, Flattening und somit verschachtelten Datenparallelismus transparent in eine vollständige funktionale Programmiersprache wie Haskell zu intergrieren. Wir glauben, daß dies sowohl der Akzeptanz des Programmiermodells als auch der Entwicklung von paralleler Software zugute kommen wird.
Nested data-parallel programming is an attractive approach to implementing applications for massively parallel systems. It allows complex parallel behaviour to be specified by combining and nesting operations on parallel collections and liberates the programmer from low-level concerns such as synchronisation and communication. The high degree of abstraction is achieved by transferring to the compiler the problem of finding easily parallelisable representations for data structures and transforming the computations accordingly. This task is carried out by the flattening transformation which eliminates nested uses of parallelism, generating flat data-parallel code which is amenable to a wide range of optimisations and can be executed efficiently on modern parallel architectures. The correctness of flattening crucially depends on referential transparency of the source language; but until now, the usefulness of this transformation in a purely functional setting has been severely restricted as it could not handle higher-order functions. The present dissertation shows that this shortcoming is due to the intertwining of computation and data inherent in the standard semantics of the lambda calculus and proposes to combine flattening with closure conversion as a solution to this problem. Closure conversion is a well-established program transformation which provides precisely the required degree of separation between code and data. The viability of this approach is validated by investigating a representative range of parallel operations and demonstrating how they can be naturally extended to support higher-order functions in closure-converted programs. Moreover, the dissertation provides a detailed discussion of the interactions between flattening and lazy evaluation. These interactions are quite intricate, as the flat data structures derived by the transformation a based on strict, unboxed arrays. Nevertheless, it is shown that lazy programs can be correctly flattened by suitably modifying the transformation as compared to previous accounts. Finally, the correctness of the flattening transformation in a higher-order, non-strict setting is proved. The proof relies on a novel form of the lambda calculus which syntactically enforces the separation of computation and data achieved by closure conversion. These results allow flattening and, hence, nested data parallelism to be seamlessly integrated into a full-fledged functional language, such as Haskell. We believe that this will have a beneficial impact on the acceptance of this programming model and on the delevopment of parallel software applications.
