From 3e362cf0412ce1f0d3cb119321b264c214bd34c6 Mon Sep 17 00:00:00 2001 From: haining Date: Mon, 13 Nov 2023 20:15:25 +0200 Subject: [PATCH 1/4] Update morally-strong to follow HRF-indirect and add test --- .../dartagnan/wmm/analysis/RelationAnalysis.java | 3 ++- dartagnan/src/test/resources/PTXv7_5-expected.csv | 1 + litmus/PTX/Manual/MP-cta1.litmus | 13 +++++++++++++ litmus/VULKAN/Kronos-Group/ssw1.litmus | 2 +- 4 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 litmus/PTX/Manual/MP-cta1.litmus 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..e9cf84c12d 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 @@ -944,7 +944,8 @@ public Knowledge visitSameScope(Relation rel, String specificScope) { } 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().sameAtHigherScope(thread2.getScopeHierarchy(), scope1) + && thread2.getScopeHierarchy().sameAtHigherScope(thread1.getScopeHierarchy(), scope2)) { must.add(e1, e2); } } diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index f5483c688a..eed979dff1 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-cta1.litmus,1 litmus/PTX/Manual/MP-gpu.litmus,1 litmus/PTX/Manual/MP-relaxed.litmus,1 litmus/PTX/Manual/MP-sys.litmus,1 diff --git a/litmus/PTX/Manual/MP-cta1.litmus b/litmus/PTX/Manual/MP-cta1.litmus new file mode 100644 index 0000000000..121d248e16 --- /dev/null +++ b/litmus/PTX/Manual/MP-cta1.litmus @@ -0,0 +1,13 @@ +PTX MP-cta1 +"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/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 From 5615e5987945c6782ca5b1c5865ba0d3449db763 Mon Sep 17 00:00:00 2001 From: haining Date: Mon, 13 Nov 2023 21:51:57 +0200 Subject: [PATCH 2/4] update fence-sc encoding --- .../com/dat3m/dartagnan/encoding/WmmEncoder.java | 5 +++-- dartagnan/src/test/resources/PTXv7_5-expected.csv | 1 + litmus/PTX/Manual/SB+sc-sys-gpu.litmus | 14 ++++++++++++++ 3 files changed, 18 insertions(+), 2 deletions(-) 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..78ad36f86f 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().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 index eed979dff1..ee80aac24e 100644 --- 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 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 From 9d82f58d41723cc18745469bfec9fa73a08c0dcc Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 14 Nov 2023 11:08:49 +0100 Subject: [PATCH 3/4] Some clean up in ScopeHierarchy class --- .../dat3m/dartagnan/encoding/WmmEncoder.java | 4 ++-- .../dat3m/dartagnan/program/ScopeHierarchy.java | 17 ++++++++--------- .../wmm/analysis/RelationAnalysis.java | 6 +++--- 3 files changed, 13 insertions(+), 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 index 78ad36f86f..6f79724beb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -609,8 +609,8 @@ public Void visitSyncFence(Relation syncFence) { if (scope1.isEmpty() || scope2.isEmpty()) { continue; } - if (!x.getThread().getScopeHierarchy().sameAtHigherScope((z.getThread().getScopeHierarchy()), scope1) || - !z.getThread().getScopeHierarchy().sameAtHigherScope((x.getThread().getScopeHierarchy()), scope2)) { + 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 e9cf84c12d..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,14 +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.isEmpty() && !scope2.isEmpty() && thread1.getScopeHierarchy().sameAtHigherScope(thread2.getScopeHierarchy(), scope1) - && thread2.getScopeHierarchy().sameAtHigherScope(thread1.getScopeHierarchy(), scope2)) { + if (!scope1.isEmpty() && !scope2.isEmpty() && thread1.getScopeHierarchy().canSyncAtScope(thread2.getScopeHierarchy(), scope1) + && thread2.getScopeHierarchy().canSyncAtScope(thread1.getScopeHierarchy(), scope2)) { must.add(e1, e2); } } From daba280fb28af2d55b8febf31c0ba38fcad2817e Mon Sep 17 00:00:00 2001 From: Haining Date: Tue, 14 Nov 2023 13:46:26 +0200 Subject: [PATCH 4/4] change MP test name and add expectation to PTXv6_0 --- dartagnan/src/test/resources/PTXv6_0-expected.csv | 2 ++ dartagnan/src/test/resources/PTXv7_5-expected.csv | 2 +- litmus/PTX/Manual/{MP-cta1.litmus => MP-cta-gpu.litmus} | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) rename litmus/PTX/Manual/{MP-cta1.litmus => MP-cta-gpu.litmus} (95%) 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 ee80aac24e..062faf2de8 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -152,7 +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-cta1.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 diff --git a/litmus/PTX/Manual/MP-cta1.litmus b/litmus/PTX/Manual/MP-cta-gpu.litmus similarity index 95% rename from litmus/PTX/Manual/MP-cta1.litmus rename to litmus/PTX/Manual/MP-cta-gpu.litmus index 121d248e16..7cf91b2c91 100644 --- a/litmus/PTX/Manual/MP-cta1.litmus +++ b/litmus/PTX/Manual/MP-cta-gpu.litmus @@ -1,4 +1,4 @@ -PTX MP-cta1 +PTX MP-cta-gpu "Message passing, sync because release/acquire operations are morally strong" { x=0;