BBB
9 October 2025 - 14h00
Verifying GPU programs with Memory Access Protocols
by Tiago Cogumbreiro from University of Massachusetts, Boston
invited by David MONNIAUX
9 October 2025 - 14h00
Verifying GPU programs with Memory Access Protocols
by Tiago Cogumbreiro from University of Massachusetts, Boston
invited by David MONNIAUX
Abstract: *** Tiago is likely to applying to DR CNRS ***
GPUs offer parallelism as a commodity, but they are difficult to program correctly.Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels).However, existing approaches produce too many false alarms and struggle to handle larger programs.
To address these limitations we introduce a novel analysis for DRF and bug finding, based on access memory protocols. These protocols are behavioral types that codify the way threads interact over shared memory. The crux of our approach is an approximation analysis that can correctly identify true alarms, and pinpoint the conditions that make an alarm imprecise. Our approximation analysis detects when the reported locations are reachable (control independence, or CI), and when the reported locations are precise (data independence, or DI), as well identify inexact values in an alarm. In addition to a True Positive result for programs that are CI and DI, we establish the root causes of spurious alarms depending on whetherCI or DI are present.
BIO
Tiago Cogumbreiro's research helps programmers write software with fewer bugs.
He is interested in formal methods applied to High-Performance Computing,
developing tools and techniques that localize errors.
Tiago Cogumbreiro is an associate professor, and joined the Department of
Computer Science at the University of Massachusetts Boston in fall of 2018.
Prior to that, Tiago was a postdoctoral researcher at the Georgia Institute of
Technology and Rice University, a research assistant at Imperial College London.
Tiago obtained a PhD from the University of Lisbon, Portugal.
