Better may set for sync barrier (#745)

hernanponcedeleon · Sep 30, 2024 · e3fe562 · e3fe562
1 parent 73ba96c
commit e3fe562
Showing 1 changed file with 13 additions and 8 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java
@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.wmm.analysis;
 
+import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.Register.UsageType;
@@ -980,14 +981,18 @@ public Knowledge visitSyncBarrier(SyncBar syncBar) {
             List<ControlBarrier> barriers = program.getThreadEvents(ControlBarrier.class);
             for (ControlBarrier e1 : barriers) {
                 for (ControlBarrier e2 : barriers) {
-                    // “A bar.sync or bar.red or bar.arrive operation synchronizes with a bar.sync
-                    // or bar.red operation executed on the same barrier.”
-                    if (exec.areMutuallyExclusive(e1, e2) || e2.hasTag(PTX.ARRIVE)) {
-                        continue;
-                    }
-                    may.add(e1, e2);
-                    if (e1.getId().equals(e2.getId())) {
-                        must.add(e1, e2);
+                    if (!exec.areMutuallyExclusive(e1, e2) && !e2.hasTag(PTX.ARRIVE)) {
+                        if (e1.getId() instanceof IntLiteral iLit1 && e2.getId() instanceof IntLiteral iLit2) {
+                            int id1 = iLit1.getValueAsInt();
+                            int id2 = iLit2.getValueAsInt();
+                            if (id1 != id2) {
+                                continue;
+                            }
+                        }
+                        may.add(e1, e2);
+                        if (e1.getId().equals(e2.getId())) {
+                            must.add(e1, e2);
+                        }
                     }
                 }
             }