Speaker Dr Tiago Cogumbeiro
Abstract 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 formalize a novel compositional analysis for DRF, based on access memory protocols. These protocols are behavioural types that codify the way threads interact over shared memory. Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in Faial, a tool that outperforms the state-of-the-art. Notably, it can correctly verify at least 1.41× more real-world kernels, and it exhibits a linear growth, while others grow exponentially.
Bio Tiago is an assistant professor at UMass Boston. Tiago’s research helps programmers write software with fewer bugs. Tiago develops tools that localize errors, proves the correctness of algorithms, and mines how we write code to identify anomalies.
