add C11 vs OpenCL race tests

hernanponcedeleon · Oct 14, 2024 · e321b06 · e321b06
1 parent 41d755c
commit e321b06
Show file tree

Hide file tree

Showing 9 changed files with 43 additions and 16 deletions.
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/comparison/C11AndOpenCLRaceTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/comparison/C11AndOpenCLRaceTest.java
@@ -0,0 +1,27 @@
+package com.dat3m.dartagnan.comparison;
+
+import com.dat3m.dartagnan.configuration.Property;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.IOException;
+import java.util.EnumSet;
+
+@RunWith(Parameterized.class)
+public class C11AndOpenCLRaceTest extends C11AndOpenCLTest {
+
+    @Parameterized.Parameters(name = "{index}: {0}")
+    public static Iterable<Object[]> data() throws IOException {
+        return buildLitmusTests("litmus/OPENCL/portedFromC11/");
+    }
+
+    public C11AndOpenCLRaceTest(String path) {
+        super(path);
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.CAT_SPEC));
+    }
+}
diff --git a/litmus/OPENCL/portedFromC11/auto/c.litmus b/litmus/OPENCL/portedFromC11/auto/c.litmus
@@ -1,7 +1,7 @@
 OPENCL c
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int t = *p;
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_p.litmus b/litmus/OPENCL/portedFromC11/auto/c_p.litmus
@@ -1,7 +1,7 @@
 OPENCL c_p
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int t = atomic_compare_exchange_strong_explicit(p, one, 2, memory_order_acquire, memory_order_relaxed);
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_p_reorder.litmus b/litmus/OPENCL/portedFromC11/auto/c_p_reorder.litmus
@@ -1,7 +1,7 @@
 OPENCL c_p_reorder
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     *q = 1;
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_pq.litmus b/litmus/OPENCL/portedFromC11/auto/c_pq.litmus
@@ -1,7 +1,7 @@
 OPENCL c_pq
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int t = atomic_compare_exchange_strong_explicit(p, one, 2, memory_order_acquire, memory_order_relaxed);
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_pq_reorder.litmus b/litmus/OPENCL/portedFromC11/auto/c_pq_reorder.litmus
@@ -1,7 +1,7 @@
 OPENCL c_pq_reorder
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int u = atomic_compare_exchange_strong_explicit(q, zero, 1, memory_order_acquire, memory_order_relaxed);
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_q.litmus b/litmus/OPENCL/portedFromC11/auto/c_q.litmus
@@ -1,7 +1,7 @@
 OPENCL c_q
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int t = *p;
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_q_reorder.litmus b/litmus/OPENCL/portedFromC11/auto/c_q_reorder.litmus
@@ -1,7 +1,7 @@
 OPENCL c_q_reorder
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; [zero] = 0; [one] = 1; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q, global atomic_int* zero, global atomic_int* one) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     int u = atomic_compare_exchange_strong_explicit(q, zero, 1, memory_order_acquire, memory_order_relaxed);
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;

diff --git a/litmus/OPENCL/portedFromC11/auto/c_reorder.litmus b/litmus/OPENCL/portedFromC11/auto/c_reorder.litmus
@@ -1,7 +1,7 @@
 OPENCL c_reorder
 { [x] = 0; [y] = 0; [p] = 0; [q] = 0; }
 
-P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P0@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r0 = atomic_load_explicit(x, memory_order_relaxed);
   if (r0) {
     *q = 1;
@@ -12,7 +12,7 @@ P0@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile g
   }
 }
 
-P1@wg 0, dev 0 (atomic_int *x, atomic_int *y, volatile global int* p, volatile global int* q) {
+P1@wg 0, dev 0 (global atomic_int* x, global atomic_int* y, volatile global int* p, volatile global int* q) {
   int r1 = atomic_load_explicit(y, memory_order_relaxed);
   if (r1) {
     int r2 = *q;