Update morally-strong to follow HRF-indirect and add test (#569)

* Update morally-strong to follow HRF-indirect * Update fence-sc encoding * Some clean up in ScopeHierarchy class * Fix typo in vulkan test --------- Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Nov 14, 2023 · 9324fb7 · 9324fb7
1 parent d3981bf
commit 9324fb7
Show file tree

Hide file tree

Showing 8 changed files with 46 additions and 14 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().canSyncAtScope((z.getThread().getScopeHierarchy()), scope1) ||
+                            !z.getThread().getScopeHierarchy().canSyncAtScope((x.getThread().getScopeHierarchy()), scope2)) {
                         continue;
                     }
                     boolean forwardPossible = maySet.contains(x, z);

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/ScopeHierarchy.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/ScopeHierarchy.java
@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program;
 
-import com.dat3m.dartagnan.configuration.Arch;
 import com.dat3m.dartagnan.program.event.Tag;
 
 import java.util.ArrayList;
@@ -40,27 +39,27 @@ public int getScopeId(String scope) {
         return scopeIds.getOrDefault(scope, -1);
     }
 
-    // For each scope S higher than flag, we check both events are in the same scope S
-    public boolean sameAtHigherScope(ScopeHierarchy thread, String flag) {
-        if (!this.getClass().equals(thread.getClass()) || !this.getScopes().contains(flag)) {
+    // For any scope higher than the given one, we check both threads have the same scope id.
+    public boolean canSyncAtScope(ScopeHierarchy other, String scope) {
+        if (!this.getScopes().contains(scope)) {
             return false;
         }
 
         ArrayList<String> scopes = this.getScopes();
-        int validIndex = scopes.indexOf(flag);
+        int validIndex = scopes.indexOf(scope);
         // scopes(0) is highest in hierarchy
         // i = 0 is global, every thread will always have the same id, so start from i = 1
         for (int i = 1; i <= validIndex; i++) {
-            if (!sameAtSingleScope(thread, scopes.get(i))) {
+            if (!atSameScopeId(other, scopes.get(i))) {
                 return false;
             }
         }
         return true;
     }
 
-    private boolean sameAtSingleScope(ScopeHierarchy thread, String scope) {
+    private boolean atSameScopeId(ScopeHierarchy other, String scope) {
         int thisId = this.getScopeId(scope);
-        int threadId = thread.getScopeId(scope);
-        return (thisId == threadId && thisId != -1);
+        int otherId = other.getScopeId(scope);
+        return (thisId == otherId && thisId != -1);
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java
@@ -938,13 +938,14 @@ public Knowledge visitSameScope(Relation rel, String specificScope) {
                     Thread thread1 = e1.getThread();
                     Thread thread2 = e2.getThread();
                     if (specificScope != null) { // scope specified
-                        if (thread1.getScopeHierarchy().sameAtHigherScope(thread2.getScopeHierarchy(), specificScope)) {
+                        if (thread1.getScopeHierarchy().canSyncAtScope(thread2.getScopeHierarchy(), specificScope)) {
                             must.add(e1, e2);
                         }
                     } else {
                         String scope1 = Tag.getScopeTag(e1, program.getArch());
                         String scope2 = Tag.getScopeTag(e2, program.getArch());
-                        if (scope1.equals(scope2) && !scope1.isEmpty() && thread1.getScopeHierarchy().sameAtHigherScope(thread2.getScopeHierarchy(), scope1)) {
+                        if (!scope1.isEmpty() && !scope2.isEmpty() && thread1.getScopeHierarchy().canSyncAtScope(thread2.getScopeHierarchy(), scope1)
+                                && thread2.getScopeHierarchy().canSyncAtScope(thread1.getScopeHierarchy(), scope2)) {
                             must.add(e1, e2);
                         }
                     }

diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv
@@ -29,6 +29,7 @@ litmus/PTX/Manual/LB+NoThinAir-location_.litmus,1
 litmus/PTX/Manual/LB+NoThinAir-register.litmus,1
 litmus/PTX/Manual/MP-3-transitive.litmus,1
 litmus/PTX/Manual/MP-cta.litmus,1
+litmus/PTX/Manual/MP-cta-gpu.litmus,1
 litmus/PTX/Manual/MP-gpu.litmus,1
 litmus/PTX/Manual/MP-relaxed.litmus,1
 litmus/PTX/Manual/MP-sys.litmus,1
@@ -56,6 +57,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/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv
@@ -152,6 +152,7 @@ litmus/PTX/Manual/LB+NoThinAir-location_.litmus,1
 litmus/PTX/Manual/LB+NoThinAir-register.litmus,1
 litmus/PTX/Manual/MP-3-transitive.litmus,1
 litmus/PTX/Manual/MP-cta.litmus,1
+litmus/PTX/Manual/MP-cta-gpu.litmus,1
 litmus/PTX/Manual/MP-gpu.litmus,1
 litmus/PTX/Manual/MP-relaxed.litmus,1
 litmus/PTX/Manual/MP-sys.litmus,1
@@ -178,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/MP-cta-gpu.litmus b/litmus/PTX/Manual/MP-cta-gpu.litmus
@@ -0,0 +1,13 @@
+PTX MP-cta-gpu
+"Message passing, sync because release/acquire operations are morally strong"
+{
+x=0;
+y=0;
+P1:r1=0;
+P1:r2=0;
+}
+ P0@cta 0,gpu 0         | P1@cta 0,gpu 0         ;
+ st.weak x, 1           | ld.acquire.gpu r1, y   ;
+ st.release.cta y, 1    | ld.weak r2, x          ;
+~exists
+(P1:r1 == 1 /\ P1:r2 != 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)
diff --git a/litmus/VULKAN/Kronos-Group/ssw1.litmus b/litmus/VULKAN/Kronos-Group/ssw1.litmus
@@ -10,7 +10,7 @@ ssw 0 1;
 ssw 1 2;
 }
  P0@sg 0,wg 0, qf 0               | P1@sg 1,wg 0, qf 0               | P2@sg 2,wg 0, qf 0               ;
- st.sc0 x, 1                      | avdevice                         | ld.sc1 r0, x                     ;
+ st.sc0 x, 1                      | avdevice                         | ld.sc1 r0, y                     ;
                                   | visdevice                        |                                  ;
 exists
 (P2:r0 == 1)