Merge branch 'development' into opencl

benchmarks/opencl/loop/barrier-loop-1.cl

@@ -0,0 +1,11 @@
+// clspv barrier-loop-1.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-1.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    x[tid] = tid;
+    for (uint i = 1; i <= 3; i++) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+        x[tid] += i;
+    }
+}

benchmarks/opencl/loop/barrier-loop-2.cl

@@ -0,0 +1,13 @@
+// clspv barrier-loop-2.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-2.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    uint gid = get_group_id(0);
+    for (uint i = 0; i < 2; i++) {
+        if (i % 2 == gid) {
+            barrier(CLK_GLOBAL_MEM_FENCE);
+            x[tid] = tid + i;
+        }
+    }
+}

benchmarks/opencl/loop/barrier-loop-3.cl

@@ -0,0 +1,15 @@
+// clspv barrier-loop-3.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-3.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    x[tid] = tid;
+    for (uint i = 1; i <= 2; i++) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+        x[tid] += i;
+        for (uint j = 2; j <= 3; j++) {
+            barrier(CLK_GLOBAL_MEM_FENCE);
+            x[tid] *= j;
+        }
+    }
+}

benchmarks/opencl/loop/barrier-loop-4.cl

@@ -0,0 +1,11 @@
+// clspv barrier-loop-4.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-4.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+    for (uint i = 0; i < 2; i++) {
+        atomic_store_explicit(&(x[i * 2 + tid]), 1, memory_order_release);
+        barrier(CLK_GLOBAL_MEM_FENCE);
+        r0[i * 2 + tid] = atomic_load_explicit(&(x[i * 2 + 1 - tid]), memory_order_acquire);
+    }
+}

benchmarks/opencl/loop/barrier-loop-5.cl

@@ -0,0 +1,13 @@
+// clspv barrier-loop-5.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-5.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+    for (uint i = 0; i < 2; i++) {
+        atomic_store_explicit(&(x[i * 2 + tid]), 1, memory_order_release);
+        if (i == 0 || tid >= 2) {
+            barrier(CLK_GLOBAL_MEM_FENCE);
+        }
+        r0[i * 2 + tid] = atomic_load_explicit(&(x[i * 2 + 1 - tid]), memory_order_acquire);
+    }
+}

benchmarks/opencl/loop/barrier-loop-6.cl

@@ -0,0 +1,13 @@
+// clspv barrier-loop-6.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-loop-6.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+    for (uint i = 0; i < 2; i++) {
+        atomic_store_explicit(&(x[i * 2 + tid]), 1, memory_order_release);
+        if (i == 1 || tid >= 2) {
+            barrier(CLK_GLOBAL_MEM_FENCE);
+        }
+        r0[i * 2 + tid] = atomic_load_explicit(&(x[i * 2 + 1 - tid]), memory_order_acquire);
+    }
+}

benchmarks/opencl/loop/barrier-no-loop-1.cl

@@ -0,0 +1,13 @@
+// clspv barrier-no-loop-1.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-1.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    x[tid] = tid;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] += 1;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] += 2;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] += 3;
+}

benchmarks/opencl/loop/barrier-no-loop-2.cl

@@ -0,0 +1,15 @@
+// clspv barrier-no-loop-2.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-2.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    uint gid = get_group_id(0);
+    if (gid == 0) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+        x[tid] = tid;
+    }
+    if (gid == 1) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+        x[tid] = tid + 1;
+    }
+}

benchmarks/opencl/loop/barrier-no-loop-3.cl

@@ -0,0 +1,19 @@
+// clspv barrier-no-loop-3.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-3.spv.dis
+
+__kernel void test(global uint* x) {
+    uint tid = get_global_id(0);
+    x[tid] += tid;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] += 1;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] *= 2;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] *= 3;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] += 2;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] *= 2;
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    x[tid] *= 3;
+}

benchmarks/opencl/loop/barrier-no-loop-4.cl

@@ -0,0 +1,14 @@
+// clspv barrier-no-loop-4.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-4.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+
+    atomic_store_explicit(&(x[tid]), 1, memory_order_release);
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    r0[tid] = atomic_load_explicit(&(x[1 - tid]), memory_order_acquire);
+
+    atomic_store_explicit(&(x[tid + 2]), 1, memory_order_release);
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    r0[2 + tid] = atomic_load_explicit(&(x[3 - tid]), memory_order_acquire);
+}

benchmarks/opencl/loop/barrier-no-loop-5.cl

@@ -0,0 +1,16 @@
+// clspv barrier-no-loop-5.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-5.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+
+    atomic_store_explicit(&(x[tid]), 1, memory_order_release);
+    if (tid >= 2) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+    }
+    r0[tid] = atomic_load_explicit(&(x[1 - tid]), memory_order_acquire);
+
+    atomic_store_explicit(&(x[tid + 2]), 1, memory_order_release);
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    r0[2 + tid] = atomic_load_explicit(&(x[3 - tid]), memory_order_acquire);
+}

benchmarks/opencl/loop/barrier-no-loop-6.cl

@@ -0,0 +1,16 @@
+// clspv barrier-no-loop-6.cl --cl-std=CL2.0 --inline-entry-points --spv-version=1.6
+// spirv-dis a.spv > barrier-no-loop-6.spv.dis
+
+__kernel void test(global atomic_uint* x, global uint* r0) {
+    uint tid = get_global_id(0);
+
+    atomic_store_explicit(&(x[tid]), 1, memory_order_release);
+    barrier(CLK_GLOBAL_MEM_FENCE);
+    r0[tid] = atomic_load_explicit(&(x[1 - tid]), memory_order_acquire);
+
+    atomic_store_explicit(&(x[tid + 2]), 1, memory_order_release);
+    if (tid >= 2) {
+        barrier(CLK_GLOBAL_MEM_FENCE);
+    }
+    r0[2 + tid] = atomic_load_explicit(&(x[3 - tid]), memory_order_acquire);
+}

dartagnan/src/main/antlr4/LitmusPTX.g4

@@ -151,14 +151,22 @@ fenceAlias
     ;
 
 barrier
-    :   Barrier Period CTA Period barrierMode value
+    :   Barrier Period CTA Period barrierMode constant (Comma barrierId (Comma barrierQuorum)?)?
     ;
 
 barrierMode
     :   Sync
     |   Arrive
     ;
 
+barrierId
+    : value
+    ;
+
+barrierQuorum
+    : value
+    ;
+
 atomInstruction
     :   atomOp
     |   atomCAS

dartagnan/src/main/antlr4/LitmusVulkan.g4

@@ -136,7 +136,7 @@ memoryBarrierInstruction
     ;
 
 controlBarrierInstruction
-    :   ControlBarrier (scope | moAcq scope semSc+ semVis? | moRel scope semSc+ semAv? | moAcqRel scope semSc+ semAv? semVis?) value
+    :   ControlBarrier (scope | moAcq scope semSc+ semVis? | moRel scope semSc+ semAv? | moAcqRel scope semSc+ semAv? semVis?) constant (Comma barrierId (Comma barrierQuorum)?)?
     ;
 
 localInstruction
@@ -160,6 +160,14 @@ deviceOperation
     |   VISDEVICE
     ;
 
+barrierId
+    : value
+    ;
+
+barrierQuorum
+    : value
+    ;
+
 value
     :   constant
     |   register

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java

@@ -17,10 +17,7 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.MemoryEvent;
 import com.dat3m.dartagnan.program.event.RegWriter;
-import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.Load;
-import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
-import com.dat3m.dartagnan.program.event.core.Store;
+import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.verification.Context;
 import com.dat3m.dartagnan.verification.VerificationTask;
@@ -80,6 +77,7 @@ public final class EncodingContext {
 
     private final Map<Event, BooleanFormula> controlFlowVariables = new HashMap<>();
     private final Map<Event, BooleanFormula> executionVariables = new HashMap<>();
+    private final Map<NamedBarrier, BooleanFormula> syncVariables = new HashMap<>();
     private final Map<Event, Formula> addresses = new HashMap<>();
     private final Map<Event, Formula> values = new HashMap<>();
     private final Map<Event, Formula> results = new HashMap<>();
@@ -197,6 +195,10 @@ public BooleanFormula jumpCondition(CondJump event) {
         return encodeExpressionAsBooleanAt(event.getGuard(), event);
     }
 
+    public BooleanFormula sync(NamedBarrier event) {
+        return syncVariables.get(event);
+    }
+
     public BooleanFormula execution(Event event) {
         return (event.cfImpliesExec() ? controlFlowVariables : executionVariables).get(event);
     }
@@ -267,7 +269,7 @@ public BooleanFormula equal(Formula left, Formula right) {
         throw new UnsupportedOperationException(String.format("Unknown types for equal(%s,%s)", left, right));
     }
 
-    private IntegerFormula toInteger(Formula formula) {
+    public IntegerFormula toInteger(Formula formula) {
         if (formula instanceof IntegerFormula f) {
             return f;
         }
@@ -417,6 +419,9 @@ private void initialize() {
 
         // ------- Event variables  -------
         for (Event e : verificationTask.getProgram().getThreadEvents()) {
+            if (e instanceof NamedBarrier b) {
+                syncVariables.put(b, booleanFormulaManager.makeVariable("sync " + e.getGlobalId()));
+            }
             if (!e.cfImpliesExec()) {
                 executionVariables.put(e, booleanFormulaManager.makeVariable("exec " + e.getGlobalId()));
             }