Data race reported on CAS-lock implementation

[teppanyakii]

Hello, The following is a simple implementation of a CAS-lock using opencl-1.2 (in this outdated version, the CAS returns the old value).

 __kernel void mutex_test(global uint* l, global int* x, global int* A) {
     int a;
     if (atom_cmpxchg(l, 0, 1) == 0) {
       a = *x;
       *x = a + 1;
       atom_xchg(l, 0);
     }
 }

Usually, the CAS would be in a loop. I created this version with an if since if the kernel contains loops there is a high chance that they may be false positives arising due to limitations of the tool invariant inference procedures. The lock is only released if it was acquired (otherwise this could cause problems with more than 2 threads). Unfortunately, gpu-verify still reports a race. Is this still a false alarm?

> gpuverify --local_size=2 --num_groups=1 --findbugs [caslock.cl](http://caslock.cl/)
caslock.opt.bc: warning: Assuming the arguments 'l', 'x', 'A' of 'mutex_test' on line 1 of [caslock.cl](http://caslock.cl/) to be non-aliased; please consider adding a restrict qualifier to these arguments
[caslock.cl](http://caslock.cl/): error: possible read-write race on x[0]:
Write by work item 1 in work group 0, caslock.cl:5:7:
  *x = a + 1;
Read by work item 0 in work group 0, caslock.cl:4:7:
  a = *x;
GPUVerify kernel analyser finished with 0 verified, 1 error

[afd]

This false alarm is expected, because GPUVerify only supports barrier-based synchronisation. Limited support for atomics is provided, as described in this paper:

https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/NFM.pdf

However, from what I recall this only supports simple use cases where atomic counters are used to access disjoint memory locations. In your case, the lock is being used to protect a particular location in shared memory, and that is beyond the scope of the tool.

[afd]

While I closed the issue, happy to discuss more if you have questions (in which case just reopen it).