On the Correctness of the SIMT Execution Model of GPUs

Axel Habermaier, Alexander Knapp
Institut fur Informatik, Augsburg
Institut fur Informatik (Augsburg) Report, 2012


   title={On the Correctness of the SIMT Execution Model of GPUs$}$},

   author={Habermaier, A. and Knapp, A.},


   publisher={Universit{"a}tsbibliothek der Universit{"a}t Augsburg$}$}


Download Download (PDF)   View View   Source Source   



GPUs are becoming a primary resource of computing power. They use a single instruction, multiple threads (SIMT) execution model that executes batches of threads in lockstep. If the control flow of threads within the same batch diverges, the different execution paths are scheduled sequentially; once the control flows reconverge, all threads are executed in lockstep again. Several thread batching mechanisms have been proposed, albeit without establishing their semantic validity or their scheduling properties. To increase the level of confidence in the correctness of GPU-accelerated programs, we formalize the SIMT execution model for a stack-based reconvergence mechanism in an operational semantics and prove its correctness by constructing a simulation between the SIMT semantics and a standard interleaved thread semantics. We also demonstrate that the SIMT execution model produces unfair schedules in some cases. We discuss the problem of unfairness for different batching mechanisms like dynamic warp formation and a stack-less reconvergence strategy.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: