Review comments - part 4

dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ConstructExpr.java

@@ -9,7 +9,6 @@
 import com.dat3m.dartagnan.expression.type.ArrayType;
 
 import java.util.List;
-import java.util.Objects;
 import java.util.stream.Collectors;
 
 import static com.google.common.base.Preconditions.checkArgument;
@@ -38,17 +37,4 @@ public <T> T accept(ExpressionVisitor<T> visitor) {
     public String toString() {
         return operands.stream().map(Expression::toString).collect(Collectors.joining(", ", "{ ", " }"));
     }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (o == null || getClass() != o.getClass()) return false;
-        ConstructExpr that = (ConstructExpr) o;
-        return Objects.equals(type, that.type) && Objects.equals(operands, that.operands);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(type, operands);
-    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/MemoryTransformer.java

@@ -22,6 +22,7 @@
 
 public class MemoryTransformer extends ExprTransformer {
 
+    // Thread / Subgroup / Workgroup / QueueFamily / Device
     private static final List<String> namePrefixes = List.of("T", "S", "W", "Q", "D");
 
     private final Function function;

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/TagSet.java

@@ -1,5 +1,7 @@
 package com.dat3m.dartagnan.program.event;
 
+import com.google.common.base.Preconditions;
+
 import java.util.*;
 
 public final class TagSet extends AbstractSet<String> {
@@ -8,12 +10,11 @@ public final class TagSet extends AbstractSet<String> {
 
     @Override
     public boolean add(String tag) {
-        if (tag != null) {
-            final int index = Collections.binarySearch(sortedTags, tag);
-            if (index < 0) {
-                sortedTags.add(~index, tag);
-                return true;
-            }
+        Preconditions.checkNotNull(tag);
+        final int index = Collections.binarySearch(sortedTags, tag);
+        if (index < 0) {
+            sortedTags.add(~index, tag);
+            return true;
         }
         return false;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java

@@ -203,10 +203,10 @@ public EventGraph findTransitivelyImpliedCo(Relation co) {
             final MemoryEvent x = (MemoryEvent) e1;
             final MemoryEvent z = (MemoryEvent) e2;
             boolean hasIntermediary = mustOut.getOrDefault(x, Set.of()).stream().anyMatch(y -> y != x && y != z &&
-                    (exec.isImplied(y, x) && exec.isImplied(z, y)) &&
+                    (exec.isImplied(x, y) || exec.isImplied(z, y)) &&
                     !k.getMaySet().contains(z, y))
                     || mustIn.getOrDefault(z, Set.of()).stream().anyMatch(y -> y != x && y != z &&
-                    (exec.isImplied(x, y) && exec.isImplied(y, z)) &&
+                    (exec.isImplied(x, y) || exec.isImplied(z, y)) &&
                     !k.getMaySet().contains(y, x));
             if (hasIntermediary) {
                 transCo.add(e1, e2);
@@ -755,11 +755,15 @@ public Knowledge visitReadModifyWrites(ReadModifyWrites rmw) {
         @Override
         public Knowledge visitCoherence(Coherence co) {
             logger.trace("Computing knowledge about memory order");
+            List<Store> allWrites = program.getThreadEvents(Store.class);
             List<Store> nonInitWrites = program.getThreadEvents(Store.class);
             nonInitWrites.removeIf(Init.class::isInstance);
             EventGraph may = new EventGraph();
             for (Store w1 : program.getThreadEvents(Store.class)) {
-                for (Store w2 : nonInitWrites) {
+                // It is possible to have multiple initial writes
+                // to the same memory location via different virtual memory aliases
+                List<Store> writes = w1 instanceof Init ? allWrites : nonInitWrites;
+                for (Store w2 : writes) {
                     if (w1.getGlobalId() != w2.getGlobalId() && !exec.areMutuallyExclusive(w1, w2)
                             && alias.mayAlias(w1, w2)) {
                         may.add(w1, w2);

dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java

@@ -48,7 +48,6 @@ public SpirvChecksTest(String file, int bound, Result expected) {
     @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}")
     public static Iterable<Object[]> data() throws IOException {
         return Arrays.asList(new Object[][]{
-                // Agree with gpu-verify
                 {"atomics/atomic_read_race.spv.dis", 1, PASS},
                 {"atomics/equality_fail.spv.dis", 1, PASS},
                 {"atomics/forloop.spv.dis", 2, UNKNOWN},
@@ -65,15 +64,19 @@ public static Iterable<Object[]> data() throws IOException {
                 {"divergence/race_no_divergence.spv.dis", 1, PASS},
                 {"inter_group_and_barrier_flag_tests/fail/local_id.spv.dis", 1, PASS},
                 {"inter_group_and_barrier_flag_tests/fail/missing_local_barrier_flag.spv.dis", 1, PASS},
+
                 // Fails check checkRelIsSem for a barrier with semantics 0x8 (rel_acq, no storage class semantics)
                 // {"inter_group_and_barrier_flag_tests/fail/no_barrier_flags.spv.dis", 1, PASS},
+
                 {"inter_group_and_barrier_flag_tests/fail/sync.spv.dis", 1, PASS},
                 {"inter_group_and_barrier_flag_tests/pass/local_barrier_flag.spv.dis", 1, PASS},
                 {"inter_group_and_barrier_flag_tests/pass/local_id_benign_write_write.spv.dis", 1, PASS},
                 {"inter_group_and_barrier_flag_tests/pass/pass_due_to_intra_group_flag.spv.dis", 1, PASS},
                 {"localarrayaccess.spv.dis", 1, PASS},
+
                 // Fails check checkRelIsSem for a barrier with semantics 0x8 (rel_acq, no storage class semantics)
                 // {"mem_fence.spv.dis", 1, PASS},
+
                 {"misc/fail/miscfail1.spv.dis", 1, PASS},
                 {"misc/fail/miscfail3.spv.dis", 1, PASS},
                 {"misc/fail/struct_member_race.spv.dis", 1, PASS},
@@ -108,22 +111,17 @@ public static Iterable<Object[]> data() throws IOException {
                 {"test_structs/use_element.spv.dis", 1, PASS},
                 {"test_structs/use_struct_element.spv.dis", 1, PASS},
 
-                // Fails in gpu-verify, but should pass (even according to the annotation in the test)
                 {"saturate/sadd.spv.dis", 1, PASS},
                 {"saturate/ssub.spv.dis", 1, PASS},
 
-                // Passes in gpu-verify, but has race (even according to the annotation in the test)
                 {"atomics/refined_atomic_abstraction/bad_local_counters.spv.dis", 1, PASS},
                 {"atomics/refined_atomic_abstraction/intra_local_counters.spv.dis", 1, PASS},
 
-                // Should pass according to gpu-verify, suspecting a bug in the memory model
                 {"atomics/counter.spv.dis", 1, PASS},
 
-                // In gpu-verify fails barrier divergence but not leading to a data race
                 {"barrier_intervals/test2.spv.dis", 1, PASS},
                 {"sourcelocation_tests/barrier_divergence/fail.spv.dis", 1, PASS},
 
-                // In gpu-verify fails command-line test, no races
                 {"global_size/local_size_fail_divide_global_size.spv.dis", 1, PASS},
                 {"global_size/mismatch_dims.spv.dis", 1, PASS},
                 {"global_size/num_groups_and_global_size.spv.dis", 1, PASS},