Add global fence example

sakehl · Mar 27, 2024 · 7aa1f4e · 7aa1f4e
1 parent 7baa7f9
commit 7aa1f4e
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 0 deletions.
diff --git a/examples/concepts/gpgpu/global_fence_opencl.cl b/examples/concepts/gpgpu/global_fence_opencl.cl
@@ -0,0 +1,47 @@
+//:: cases DynamicSharedOpenCl
+//:: tool silicon
+//:: verdict Pass
+
+#include <opencl.h>
+
+/*@
+  context get_local_size(0) == 32 && get_local_size(1) == 1 && get_local_size(2) == 1;
+  context get_num_groups(0) == 4 && get_num_groups(1) == 1 && get_num_groups(2) == 1;
+
+  context in != NULL && out != NULL;
+  context \pointer_length(in) == 1;
+  context \pointer_length(out) == n;
+  context n > 0;
+  context get_local_size(0) * get_num_groups(0) >= n;
+  context Perm(&in[0], write \ (get_local_size(0) * get_num_groups(0)));
+  context \gtid<n ==> Perm(&out[\gtid], write);
+
+  context s != NULL && \pointer_length(s) == get_num_groups(0);
+  requires \ltid == 0 ==> Perm(&s[get_group_id(0)], write);
+
+  ensures \gtid<n ==> out[\gtid] == \old(out[\gtid]) + in[0];
+@*/
+__kernel void blur_x(global int* in, global int* out, int n, global int* s) {
+  int tid = get_group_id(0) * get_local_size(0) + get_local_id(0);
+  if(get_local_id(0) == 0) {
+    s[get_group_id(0)] = in[0];
+  }
+
+  /*@
+    context Perm(&in[0], write \ (get_local_size(0) * get_num_groups(0)));
+    context get_group_id(0) * get_local_size(0) + get_local_id(0)<n ==> Perm(&out[get_group_id(0) * get_local_size(0) + get_local_id(0)], write);
+    context get_group_id(0) * get_local_size(0) + get_local_id(0)<n ==> \old(out[get_group_id(0) * get_local_size(0) + get_local_id(0)]) == out[get_group_id(0) * get_local_size(0) + get_local_id(0)];
+
+    requires get_local_id(0) == 0 ==> Perm(&s[get_group_id(0)], write);
+    requires get_local_id(0) == 0 ==> s[get_group_id(0)] == in[0];
+
+    ensures Perm(&s[get_group_id(0)], write \ get_local_size(0));
+
+    ensures s[get_group_id(0)] == in[0];
+  @*/
+  barrier(CLK_GLOBAL_MEM_FENCE);
+
+  if(tid < n) {
+    out[tid] += s[get_group_id(0)];
+  }
+}
diff --git a/test/main/vct/test/integration/examples/GpgpuSpec.scala b/test/main/vct/test/integration/examples/GpgpuSpec.scala
@@ -5,10 +5,13 @@ import vct.test.integration.helper.VercorsSpec
 class GpgpuSpec extends VercorsSpec {
   vercors should verify using silicon example "concepts/gpgpu/cuda.cu"
   vercors should verify using silicon example "concepts/gpgpu/cuda_blur.cu"
+
   vercors should verify using silicon example "concepts/gpgpu/dynamic_shared_cuda.cu"
   vercors should verify using silicon example "concepts/gpgpu/dynamic_shared_opencl.cl"
   vercors should verify using silicon example "concepts/gpgpu/static_shared_cuda.cu"
   vercors should verify using silicon example "concepts/gpgpu/static_shared_opencl.cl"
+
+  vercors should verify using silicon example "concepts/gpgpu/global_fence_opencl.cl"
   // https://github.com/utwente-fmt/vercors/issues/852
   // vercors should verify using silicon example "concepts/gpgpu/GPGPU-Example-updates.cu"
   // https://github.com/utwente-fmt/vercors/issues/856