by Anton Wijs (Eindhoven University of Technology), Jan Heemstra (Technical University of Eindhoven)

→ Europe/Zurich
593/R-010 - Salle 11 (CERN)

593/R-010 - Salle 11

CERN

50
Show room on map
Description

Abstract

Since 2007, graphics processing units (GPUs) have been used to accelerate scientific computations other than image processing, with tremendous success. In many fields, they revolutionised the state-of-the-art. This has happened for computational biology, statistics, and physics, among others. With deep learning, GPUs have made an enormous impact in Artificial Intelligence.

GPUs offer an increasingly important alternative to the more traditional computing with Central Processing Units (CPUs). Science published an article by Leiserson et al. in 2020 [66] in which it was concluded that the computational growth of new CPUs has stagnated, and that therefore major computational advances will have to come more and more from the use of massively parallel algorithms, such as the ones running on GPUs.

GPUs have an enormous computational power, but a very restricting computational paradigm, called Single Instruction Multiple Threads (SIMT). This essentially means that computations ideally consist of instructions that can be simultaneously performed by thousands of threads, every thread applying those instructions on different data.

A good example of a computation fitting this paradigm is matrix-vector multiplication: it can be performed in parallel by assigning one thread to each matrix row. Given a row i, a thread computes the i-th entry of the resulting vector. An alternative is to assign one thread to each matrix entry; although more complicated, this is also very much in line with SIMT.

Computations for which it is less clear whether they can be accelerated effectively with GPUs are those that highly depend on the input data. Graph processing, for instance, tends to highly depend on the structure of the input graph (representing, for instance, a social network or a road map). Still, impressive acceleration has been achieved by researchers over the years.

In this course, we will take a close look at GPU programming, from the basic principles to very involved low-level optimisations. Furthermore, we will take an in-depth look at various real-world applications in which GPU-acceleration has been effectively applied, and discuss the algorithms that have enabled these successes, which are in some cases vastly different from the state-of-the-art algorithms for CPU computing. Graph search, symbolic reasoning with Binary Decision Diagrams, and formal verification are some of the applications that will be presented. In a number of lab sessions, the course participants will get hands-on experience accelerating some of these algorithms, such as parallel reduction, matrix operations, and graph search.

Lecturers biographies

Anton Wijs is an associate professor at Eindhoven University of Technology (TU/e), where he is leading the Parallel Software Development group in the Department of Mathematics and Computer Science. In 2007, he obtained his PhD in Computer Science at VU Amsterdam based on his research done at the Centre for Mathematics and Computer Science (CWI). After having conducted postdoctoral research at INRIA Rhône-Alpes from 2007 to 2009, at TU/e from 2009 to 2014, and RWTH Aachen University in 2014, he started working as an assistant professor at TU/e in 2015, and was promoted to associate professor in 2023. Since 2010, he has been pioneering in using GPUs to accelerate formal verification of hard- and software systems, addressing techniques such as model checking, term rewriting, system equivalence checking, SAT solving and SAT-solving based symbolic model checking, and various graph algorithms. His work has been supported by a number of grants from the Dutch Research Council (NWO), such as NWO TOP grants for the GEARS (2016) and AVVA (2017) projects, an NWO OTP grant for the ChEOPS project (2019), and NWO Open Competition grants for the GAP (2022) and GUESS (2025) projects. Internationally, Wijs acts as president of the European Association for Programming Languages and Systems (EAPLS), steering committee chair of the SPIN symposia, and steering committee member of the ETAPS & FACS conferences, all well-known in the formal verification field, in which peer-reviewed conferences form the primary venues for publication. Furthermore, he has co-chaired various well-known Computer Science conferences. In 2022, he received an Amazon Research Award for his work on GPU-accelerated model checking.

Jan Heemstra is a PhD candidate at Eindhoven University of Technology. He obtained his Master's degree from Radboud University in 2023, with a Master's Thesis on GPU-accelerated first-order theorem proving under supervision of Josef Urban at the CTU in Prague. During his PhD he continued with hardware accelerating for formal methods by extending GPUexplore with probabilistic model checking functionality. Currently, he works on GPUdecide: a GPU acceleration library for binary decision diagrams.