Verification of Producer-Consumer Synchronization in GPU Programs