The rise of AI, and especially the use of large language models is creating a massive demand for computing power. This computing power is increasingly based on GPU computing, that is, the use of graphics processing units for general purpose computing tasks. GPUs have massively parallel computing capabilities and much improved energy efficiency compared to CPUs. One of the challenges of GPU computing is the lack of portable concurrency primitives to allow a program to run correctly on GPU hardware from any manufacturer. The problem is analogous to the porting of Linux kernel concurrency primitives to all the 30+ hardware architectures it supports. That problem was solved with the help of formal memory consistency models, which enable one to prove the correctness of concurrency primitives for each architecture. This project proposes developing methods and tools to create and verify portable concurrency primitives for GPUs based on formal memory consistency models for GPUs.

2025

2029