-
Auto-Tuning High-Performance Programs Using Model Checking in Promela
Authors:
Natalia Garanina,
Sergey Staroletov,
Sergei Gorlatch
Abstract:
The paper combines research approaches that traditionally have been disjoint: 1) model checking as used in formal verification of programs, and 2) auto-tuning as often used in high-performance computing. Auto-tuning frameworks optimize parallel programs by finding the optimal values of the performance-critical parameters -- so-called tuning parameters -- for a particular high-performance architect…
▽ More
The paper combines research approaches that traditionally have been disjoint: 1) model checking as used in formal verification of programs, and 2) auto-tuning as often used in high-performance computing. Auto-tuning frameworks optimize parallel programs by finding the optimal values of the performance-critical parameters -- so-called tuning parameters -- for a particular high-performance architecture and input data size. As there are many parameters influencing program's performance, finding the optimal parameter configuration is a hardly manageable task even for experts. Auto-tuning automates this process, but it is often time-consuming. We apply model checking for accelerating auto-tuning by using a counterexample constructed during the verification of the optimality property of the program. We describe in detail an implementation of our approach for programs written in OpenCL -- the standard for programming modern high-performance architectures -- using the model representation language Promela and the popular SPIN verification tool, and we report experimental results for an application use case.
△ Less
Submitted 15 May, 2023;
originally announced May 2023.
-
Descend: A Safe GPU Systems Programming Language
Authors:
Bastian Köpcke,
Sergei Gorlatch,
Michel Steuwer
Abstract:
Graphics Processing Units (GPU) offer tremendous computational power by following a throughput oriented computing paradigm where many thousand computational units operate in parallel. Programming this massively parallel hardware is challenging. Programmers must correctly and efficiently coordinate thousands of threads and their accesses to various shared memory spaces. Existing mainstream GPU prog…
▽ More
Graphics Processing Units (GPU) offer tremendous computational power by following a throughput oriented computing paradigm where many thousand computational units operate in parallel. Programming this massively parallel hardware is challenging. Programmers must correctly and efficiently coordinate thousands of threads and their accesses to various shared memory spaces. Existing mainstream GPU programming languages, such as CUDA and OpenCL, are based on C/C++ inheriting their fundamentally unsafe ways to access memory via raw pointers. This facilitates easy to make, but hard to detect bugs such as data races and deadlocks.
In this paper, we present Descend: a safe GPU systems programming language. In the spirit of Rust, Descend's type system enforces safe CPU and GPU memory management by tracking Ownership and Lifetimes. Descend introduces a new holistic GPU programming model where computations are hierarchically scheduled over the GPU's execution resources: grid, blocks, and threads. Descend's extended Borrow checking ensures that execution resources safely access memory regions without introducing data races. For this, we introduced views describing safe parallel access patterns of memory regions.
We discuss the memory safety guarantees offered by Descend's type system and evaluate our implementation of Descend using a number of benchmarks, showing that no significant runtime overhead is introduced compared to manually written CUDA programs lacking Descend's safety guarantees.
△ Less
Submitted 5 May, 2023;
originally announced May 2023.
-
A Language for Describing Optimization Strategies
Authors:
Bastian Hagedorn,
Johannes Lenfers,
Thomas Koehler,
Sergei Gorlatch,
Michel Steuwer
Abstract:
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a nightmare for portability which is particularly problematic given the accelerating trend towards specialized hardware d…
▽ More
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a nightmare for portability which is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning, automatic differentiation, or image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this paper, we present Elevate: a functional language for describing optimization strategies. Elevate follows a tradition of prior systems used in different contexts that express optimization strategies as composition of rewrites. In contrast to systems with scheduling APIs, in Elevate programmers are not restricted to a set of built-in optimizations but define their own optimization strategies freely in a composable way. We show how user-defined optimization strategies in Elevate enable the effective optimization of programs expressed in a functional data-parallel language demonstrating competitive performance with Halide and TVM.
△ Less
Submitted 6 February, 2020;
originally announced February 2020.
