update fence-sc encoding

hernanponcedeleon · Nov 13, 2023 · 5615e59 · 5615e59
1 parent 3e362cf
commit 5615e59
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 2 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java
@@ -606,10 +606,11 @@ public Void visitSyncFence(Relation syncFence) {
                 for (Event z : allFenceSC.subList(i + 1, allFenceSC.size())) {
                     String scope1 = Tag.getScopeTag(x, program.getArch());
                     String scope2 = Tag.getScopeTag(z, program.getArch());
-                    if (!scope1.equals(scope2) || scope1.isEmpty()) {
+                    if (scope1.isEmpty() || scope2.isEmpty()) {
                         continue;
                     }
-                    if (!x.getThread().getScopeHierarchy().sameAtHigherScope((z.getThread().getScopeHierarchy()), scope1)) {
+                    if (!x.getThread().getScopeHierarchy().sameAtHigherScope((z.getThread().getScopeHierarchy()), scope1) ||
+                            !z.getThread().getScopeHierarchy().sameAtHigherScope((x.getThread().getScopeHierarchy()), scope2)) {
                         continue;
                     }
                     boolean forwardPossible = maySet.contains(x, z);

diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv
@@ -179,6 +179,7 @@ litmus/PTX/Manual/SB+sc-gpu.litmus,1
 litmus/PTX/Manual/SB+sc-gpu-multiFence.litmus,1
 litmus/PTX/Manual/SB+sc-gpu-multiFence-TotalOrder.litmus,1
 litmus/PTX/Manual/SB+sc-sys.litmus,1
+litmus/PTX/Manual/SB+sc-sys-gpu.litmus,1
 litmus/PTX/Manual/SB-weak.litmus,1
 litmus/PTX/Manual/Ticketlock-same-gpu.litmus,0
 litmus/PTX/Manual/Ticketlock-diff-gpu.litmus,1

diff --git a/litmus/PTX/Manual/SB+sc-sys-gpu.litmus b/litmus/PTX/Manual/SB+sc-sys-gpu.litmus
@@ -0,0 +1,14 @@
+PTX SB+sc-sys-gpu
+"SB is not allowed because sc fences are morally strong and thus synchronize"
+{
+x=0;
+y=0;
+P0:r1=0;
+P1:r2=0;
+}
+ P0@cta 0,gpu 0         | P1@cta 1,gpu 0         ;
+ st.weak x, 1           | st.weak y, 1           ;
+ fence.sc.sys           | fence.sc.gpu           ;
+ ld.weak r1, y          | ld.weak r2, x          ;
+~exists
+(P0:r1 != 1 /\ P1:r2 != 1)