On the Correctness of the SIMT Execution Model of GPUs