Gklee Tutorial

Wednesday, November 11, 2015

Professor Ganesh Gopalakrishnan with assistance from Geof Sawaya

GPGPU (General Purpose Graphics Processing Unit) accelerators put 1,000s of parallel (shared memory) computational units at developers' disposal, allowing advances in medical imaging, scientific computing, security, Bitcoin mining and climate modeling (just to name a few).

But this high degree of parallelism comes at a price. How does the CUDA programmer verify her program is free from data races?

For this class, we will present Gklee: a concolic (concrete + symbolic) verification tool for CUDA programs. After a brief introduction to CUDA and GPGPU programming, we will walk through details of Gklee's program analysis, such as errors it can locate and how it can cover the entire program space and still manage to scale well.

Following the discussion, we'll give a demonstration of Gklee's capabilities by running it on two CUDA programs. These will show race detection and provide output illuminating the concept of Gklee flows (they key to scalable race checking). We will also provide a pre-configured facility for you to experiment with Gklee on your own programs.