Computer Science

“Can Formal Methods (alone) Rescue HPC Debugging?”

Department of Computer Science

Distinguished Lecturer Series

Professor Ganesh L. Gopalakrishnan

School of Computing, University of Utah

When: Thursday, May 10th at 3:10pm

Where: 1131 Kemper Hall

Host: Cindy Rubio Gonzalez



High Performance Computing systems are extremely complex ensembles of CPUs and GPUs, powering supercomputers that help understand and manage the earth. The same compute power permeates autonomous systems that one day may drive all of us around. Due to the extreme degree of concurrency and heterogeneity, these systems are very difficult to design and debug. One somehow has to develop deep trust of the numbers these systems spew out. Abstraction is the key tenet to complexity reduction, the epitome of which is formal methods for debugging.  This talk will cover our formal methods inspired research covering multiple concurrency models, issues such as system resilience, floating-point error analysis and tuning, data race checking, and result-reproducibility of everyday tools such as compilers.

In HPC debugging, however, more than textbook formal methods are needed.  We recently developed an OpenMP data race checker based on collaborations with real users, but more importantly, a mix of many ideas: event tracing, data compression, data structure selection, trace abstraction — all in addition to a dose of operational semantics.  The resulting race checker has negligible memory overheads for any program size, while detecting the most races of any tool out there.  This race checker (joint work with Simone Atzeni and Zvonimir Rakamaric of Utah, and Ignacio Laguna, Greg Lee, and Dong H. Ahn of LLNL) will be the highlight of the talk.


Ganesh L. Gopalakrishnan (Senior Member of IEEE and ACM Distinguished Scientist) earned his B.Sc.(EE) degree from NIT Calicut in 1978, M.Tech (EE) from IIT Kanpur in 1980, and PhD in Computer Science from Stony Brook University in 1986, when he joined the University of Utah.

His external engagements include Visiting Assistant Professorship at the University of Calgary (1988-89) and sabbatical visits at Stanford University (1995-96), Intel (2002-03), and sabbatical projects with Microsoft on developing parallel computing curriculum (2009-10), and work on two textbooks using Jupyter notebooks in undergraduate Discrete Math and Automata Theory classes (2016-17; git-clone it from my homepage). He has published one textbook (Computation Engineering: Applied Automata Theory and Logic, Springer, 2006).

He has published over 180 refereed papers, and has graduated 21 PhD students. He is serving as the Director of the Center for Parallel Computing at Utah (“CPU”).  He was awarded one of the six “Beacons of Excellence” Awards for 2012 by the University of Utah for his work on mentoring undergraduates.

His currently active projects are: Verification Methods and Tool Frameworks for Parallel and Concurrent Systems, Formal Techniques to Enhance System Resilience, Floating-point precision tuning methods, Symbolic Data Race Checking Methods for GPUs, and Scalable OpenMP Data Race Checking Methods. His current  research grants and contracts are from NSF (CISE) and DOE (in collaboration with LLNL and PNNL).

1131 Kemper Hall

Loading Map....