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.

Sign up for GitHub

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

add privIsScoped check and update tests #578

Merged
merged 2 commits into from
Nov 28, 2023
Merged

add privIsScoped check and update tests #578

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
079b7e8
add privIsScoped check and update tests
tonghaining Nov 28, 2023
d936db3
use PRIV
tonghaining Nov 28, 2023
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
4 changes: 4 additions & 0 deletions cat/spirv-check.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,10 @@ flag ~empty nonprivIsRW as checkNonprivIsRW
let atomicIsNonpriv = ([ATOM] \ [NONPRIV])
flag ~empty atomicIsNonpriv as checkAtomicIsNonpriv

// Private operations are not scoped
let privIsScoped = (([M \ NONPRIV]) & [DV | QF | WG | SG])
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can use PRIV instead

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right I forgot, updated.

flag ~empty privIsScoped as checkPrivIsScoped

// Atomic operations implicitly have availability/visibility operations
let atomicIsAv = ([W & ATOM] \ [AV])
flag ~empty atomicIsAv as checkAtomicIsAv
Expand Down
5 changes: 0 additions & 5 deletions ...agnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,11 +423,6 @@ private void tagControl(Event e, Boolean atomic, String mo, String avvis, String
e.addTags(Tag.Vulkan.NON_PRIVATE);
}

// add nonpriv tag to all M with scope
if (!scope.isEmpty() && (e instanceof MemoryEvent)) {
e.addTags(Tag.Vulkan.NON_PRIVATE);
}

// Atomics implicitly have AV/VIS ops, hence they are implicitly nonpriv
if (atomic && e instanceof Store) {
e.addTags(Tag.Vulkan.AVAILABLE);
Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/test/resources/VULKAN-CK-expected.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,6 @@ litmus/VULKAN/Data-Race/test7-filter.litmus,1
litmus/VULKAN/Data-Race/test9-filter.litmus,1
litmus/VULKAN/Data-Race/waw-filter.litmus,1
litmus/VULKAN/Kronos-Group/asmo.litmus,1
litmus/VULKAN/Kronos-Group/asmo-weak.litmus,1
litmus/VULKAN/Kronos-Group/atomicsc.litmus,1
litmus/VULKAN/Kronos-Group/atomwrongsc.litmus,1
litmus/VULKAN/Kronos-Group/cbarinst.litmus,1
Expand Down Expand Up @@ -144,6 +143,7 @@ litmus/VULKAN/Kronos-Group/test5.litmus,1
litmus/VULKAN/Kronos-Group/test6.litmus,1
litmus/VULKAN/Kronos-Group/test9.litmus,1
litmus/VULKAN/Kronos-Group/waw.litmus,1
litmus/VULKAN/Manual/asmo-weak.litmus,1
litmus/VULKAN/Manual/CoWW-RR.litmus,1
litmus/VULKAN/Manual/SB-2-wg.litmus,1
litmus/VULKAN/Manual/SB-2-dv.litmus,1
Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/test/resources/VULKAN-DR-expected.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,4 +85,4 @@ litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1
litmus/VULKAN/Manual/XF-Barrier-relacq.litmus,1
litmus/VULKAN/Manual/XF-Barrier-rlx.litmus,0
litmus/VULKAN/Manual/XF-Barrier-weak.litmus,0
litmus/VULKAN/Kronos-Group/asmo-weak.litmus,0
litmus/VULKAN/Manual/asmo-weak.litmus,0
2 changes: 1 addition & 1 deletion dartagnan/src/test/resources/VULKAN-expected.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
litmus/VULKAN/Kronos-Group/asmo.litmus,1
litmus/VULKAN/Kronos-Group/asmo-weak.litmus,0
litmus/VULKAN/Kronos-Group/atomicsc.litmus,1
litmus/VULKAN/Kronos-Group/atomwrongsc.litmus,1
litmus/VULKAN/Kronos-Group/cbarinst.litmus,1
Expand Down Expand Up @@ -74,6 +73,7 @@ litmus/VULKAN/Kronos-Group/test5.litmus,1
litmus/VULKAN/Kronos-Group/test6.litmus,1
litmus/VULKAN/Kronos-Group/test9.litmus,1
litmus/VULKAN/Kronos-Group/waw.litmus,1
litmus/VULKAN/Manual/asmo-weak.litmus,0
litmus/VULKAN/Manual/ticketlock-same-wg.litmus,0
litmus/VULKAN/Manual/ticketlock-diff-wg.litmus,1
litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus,0
Expand Down
4 changes: 2 additions & 2 deletions litmus/VULKAN/Manual/MP-no-avvis.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ x=0;
y=0;
}
P0@sg 0, wg 0, qf 0 | P1@sg 1,wg 0, qf 0 ;
st.dv.sc0 x, 1 | ld.atom.acq.wg.sc0.semsc0 r0, y ;
st.atom.rel.wg.sc0.semsc0 y, 1 | ld.dv.sc0 r1, x ;
st.sc0 x, 1 | ld.atom.acq.wg.sc0.semsc0 r0, y ;
st.atom.rel.wg.sc0.semsc0 y, 1 | ld.sc0 r1, x ;
exists
(P1:r0 == 1 /\ P1:r1 == 0)
8 changes: 4 additions & 4 deletions litmus/VULKAN/Manual/XF-Barrier-weak.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,13 @@ P1:r0=0;
}
P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ;
st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ;
LC00: | st.dv.sc0 f, 1 | cbar.wg 2 ;
ld.dv.sc0 r2, f | LC10: | ;
bne r2, 0, LC01 | ld.dv.sc0 r2, f | ;
LC00: | st.sc0 f, 1 | cbar.wg 2 ;
ld.sc0 r2, f | LC10: | ;
bne r2, 0, LC01 | ld.sc0 r2, f | ;
goto LC00 | bne r2, 1, LC11 | ;
LC01: | goto LC10 | ;
cbar.wg 1 | LC11: | ;
st.dv.sc0 f, 0 | cbar.wg 2 | ;
st.sc0 f, 0 | cbar.wg 2 | ;
| ld.vis.dv.sc0 r1, x | ;
exists
(P1:r2 != 1 /\ P1:r1 == 0)
2 changes: 1 addition & 1 deletion litmus/VULKAN/Kronos-Group/asmo-weak.litmus → litmus/VULKAN/Manual/asmo-weak.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ P3:r3=0;
x=0;
}
P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 | P2@sg 0,wg 2, qf 0 | P3@sg 0,wg 3, qf 0 ;
st.dv.sc0 x, 1 | st.dv.sc0 x, 2 | ld.atom.dv.sc0 r0, x | ld.atom.dv.sc0 r2, x ;
st.sc0 x, 1 | st.sc0 x, 2 | ld.atom.dv.sc0 r0, x | ld.atom.dv.sc0 r2, x ;
| | ld.atom.dv.sc0 r1, x | ld.atom.dv.sc0 r3, x ;
~exists
(P2:r0 == 1 /\ P2:r1 == 2 /\ P3:r2 == 2 /\ P3:r3 == 1)