SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Fri 22 Oct 2021 14:20 - 14:35 at Zurich B - Test and Verification Chair(s): Mike Dodds
Fri 22 Oct 2021 22:20 - 22:35 at Zurich B - Test and Verification - mirror Chair(s): Shigeru Chiba

As GPU availability has increased and programming support has matured, a wider variety of applications are being ported to these platforms. Many parallel applications contain fine-grained synchronization idioms; as such, their correct execution depends on a degree of relative forward progress between threads (or thread groups). Unfortunately, many GPU programming specifications (e.g. Vulkan and Metal) say almost nothing about relative forward progress guarantees between workgroups.
Although prior work has proposed a spectrum of plausible progress models for GPUs, cross-vendor specifications have yet to commit to any model.

This work is a collection of tools and experimental data to aid specification designers when considering forward progress guarantees in programming frameworks. As a foundation, we formalize a small parallel programming language that captures the essence of fine-grained synchronization. We then provide a means of formally specifying a progress model, and develop a termination oracle that decides whether a given program is guaranteed to eventually terminate with respect to a given progress model. Next, we formalize a set of constraints that describe concurrent programs that require forward progress to terminate. This allows us to synthesize a large set of 483 progress litmus tests. Combined with the termination oracle, we can determine the expected status of each litmus test – i.e. whether it is guaranteed to eventually terminate – under various progress models. We present a large experimental campaign running the litmus tests across 8 GPUs from 5 different vendors. Our results highlight that GPUs have significantly different termination behaviors under our test suite. Most notably, we find that Apple and ARM GPUs do not support the linear occupancy-bound model, as was hypothesized by prior work.

Fri 22 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Test and VerificationOOPSLA at Zurich B +8h
Chair(s): Mike Dodds Galois, Inc.
13:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation LevelsDistinguished PaperVirtual
OOPSLA
Ranadeep Biswas Informal Systems, Diptanshu Kakwani Microsoft, India, Jyothi Vedurada IIT Hyderabad, Constantin Enea University of Paris / IRIF / CNRS, Akash Lal Microsoft Research
DOI
14:05
15m
Talk
Formal Verification of High-Level SynthesisVirtual
OOPSLA
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
DOI Pre-print File Attached
14:20
15m
Talk
Specifying and Testing GPU Workgroup Progress ModelsIn-Person
OOPSLA
Tyler Sorensen University of California at Santa Cruz, Lucas Fernan Salvador Princeton University, Harmit Raval Princeton University, Hugues Evrard Google, John Wickerson Imperial College London, Margaret Martonosi Princeton University, Alastair F. Donaldson Imperial College London
DOI
14:35
35m
Live Q&A
Discussion, Questions and Answers
OOPSLA

21:50 - 23:10
Test and Verification - mirrorOOPSLA at Zurich B
Chair(s): Shigeru Chiba The University of Tokyo
21:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation LevelsDistinguished PaperVirtual
OOPSLA
Ranadeep Biswas Informal Systems, Diptanshu Kakwani Microsoft, India, Jyothi Vedurada IIT Hyderabad, Constantin Enea University of Paris / IRIF / CNRS, Akash Lal Microsoft Research
DOI
22:05
15m
Talk
Formal Verification of High-Level SynthesisVirtual
OOPSLA
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
DOI Pre-print File Attached
22:20
15m
Talk
Specifying and Testing GPU Workgroup Progress ModelsIn-Person
OOPSLA
Tyler Sorensen University of California at Santa Cruz, Lucas Fernan Salvador Princeton University, Harmit Raval Princeton University, Hugues Evrard Google, John Wickerson Imperial College London, Margaret Martonosi Princeton University, Alastair F. Donaldson Imperial College London
DOI
22:35
35m
Live Q&A
Discussion, Questions and Answers
OOPSLA