From 9324fb7cc242077f319b9e4e1bd7a324cbf292f8 Mon Sep 17 00:00:00 2001 From: haining Date: Tue, 14 Nov 2023 16:25:22 +0200 Subject: [PATCH] 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 --- .../dat3m/dartagnan/encoding/WmmEncoder.java | 5 +++-- .../dat3m/dartagnan/program/ScopeHierarchy.java | 17 ++++++++--------- .../wmm/analysis/RelationAnalysis.java | 5 +++-- .../src/test/resources/PTXv6_0-expected.csv | 2 ++ .../src/test/resources/PTXv7_5-expected.csv | 2 ++ litmus/PTX/Manual/MP-cta-gpu.litmus | 13 +++++++++++++ litmus/PTX/Manual/SB+sc-sys-gpu.litmus | 14 ++++++++++++++ litmus/VULKAN/Kronos-Group/ssw1.litmus | 2 +- 8 files changed, 46 insertions(+), 14 deletions(-) create mode 100644 litmus/PTX/Manual/MP-cta-gpu.litmus create mode 100644 litmus/PTX/Manual/SB+sc-sys-gpu.litmus diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 804b4364da..6f79724beb 100644 --- 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 index e2eac20850..28b0450fa0 100644 --- 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 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 index 8e13c77323..4d732ec6e0 100644 --- 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 index 339d60a486..15fca5d113 100644 --- 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 index f5483c688a..062faf2de8 100644 --- 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 new file mode 100644 index 0000000000..7cf91b2c91 --- /dev/null +++ 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) \ No newline at end of file diff --git a/litmus/PTX/Manual/SB+sc-sys-gpu.litmus b/litmus/PTX/Manual/SB+sc-sys-gpu.litmus new file mode 100644 index 0000000000..749d041920 --- /dev/null +++ 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) \ No newline at end of file diff --git a/litmus/VULKAN/Kronos-Group/ssw1.litmus b/litmus/VULKAN/Kronos-Group/ssw1.litmus index 36adc17e63..d054b1fcb0 100644 --- 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) \ No newline at end of file