Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -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);
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -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);
}
}
2 changes: 2 additions & 0 deletions dartagnan/src/test/resources/PTXv6_0-expected.csv
Original file line number Diff line number Diff line change
@@ -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
2 changes: 2 additions & 0 deletions dartagnan/src/test/resources/PTXv7_5-expected.csv
Original file line number Diff line number Diff line change
@@ -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
13 changes: 13 additions & 0 deletions litmus/PTX/Manual/MP-cta-gpu.litmus
Original file line number Diff line number Diff line change
@@ -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)
14 changes: 14 additions & 0 deletions litmus/PTX/Manual/SB+sc-sys-gpu.litmus
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 1 addition & 1 deletion litmus/VULKAN/Kronos-Group/ssw1.litmus
Original file line number Diff line number Diff line change
@@ -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)