mc-imperial / gpuverify

GPUVerify: a Verifier for GPU Kernels
http://multicore.doc.ic.ac.uk/tools/GPUVerify/
Other
58 stars 15 forks source link

Fix the handling on refined atomics acting on local memory #12

Closed jeroenk closed 6 years ago

jeroenk commented 6 years ago

We apply the same trick as for normal local arrays, and add an extra bv1 dimension to the relevant _USED map that is always indexed as 1 by thread 1, and is index by a same group check by thread 2.

afd commented 6 years ago

The changes look good.

A few lines were changed only in formatting - was this part of the StyleCop integration? Ideally we should separate functional changes from style changes so that diffs are as easy to read as possible in the former case (but this was a very minor issue here).

jeroenk commented 6 years ago

A few lines were changed only in formatting

That's me noticing some more inconsistencies not caught by StyleCop and fixing them on-the-fly. And, yes, I should know better and separate them out in a separate commit.