From 35f36bc6fc82066404e9e5046d83fdb8ab088d98 Mon Sep 17 00:00:00 2001 From: haining Date: Fri, 6 Oct 2023 20:52:04 +0300 Subject: [PATCH 1/2] Fix ptx tests (#529) * fix expectation file * update plus to add * Fix grammar and parsing of CAS --------- Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/LitmusPTX.g4 | 6 +++--- .../program/visitors/VisitorLitmusPTX.java | 6 +++--- .../src/test/resources/PTXv6_0-expected.csv | 4 ++-- .../src/test/resources/PTXv7_5-expected.csv | 16 ++++++++-------- litmus/PTX/Manual/MP-dlb-no-fence-1.litmus | 2 +- litmus/PTX/Manual/MP-dlb-no-fence-2.litmus | 2 +- litmus/PTX/Manual/MP-dlb.litmus | 2 +- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/dartagnan/src/main/antlr4/LitmusPTX.g4 b/dartagnan/src/main/antlr4/LitmusPTX.g4 index 5823b261bd..2692b39be6 100644 --- a/dartagnan/src/main/antlr4/LitmusPTX.g4 +++ b/dartagnan/src/main/antlr4/LitmusPTX.g4 @@ -160,7 +160,7 @@ fenceAlias ; barrier - : Barrier Period CTA Period Sync barID + : Barrier Period CTA Period Sync value ; atomInstruction @@ -178,7 +178,7 @@ atomRegister ; atomCAS - : atom Period mo Period scope Period Cas register Comma location Comma constant Comma constant + : atom Period mo Period scope Period Cas register Comma location Comma value Comma value ; redInstruction @@ -253,7 +253,7 @@ gpuID returns [int id] : t = DigitSequence {$id = Integer.parseInt($t.text);} ; -barID +value : constant | register ; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java index 35362348f4..2998b6cfdc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java @@ -279,8 +279,8 @@ public Object visitAtomRegister(LitmusPTXParser.AtomRegisterContext ctx) { public Object visitAtomCAS(LitmusPTXParser.AtomCASContext ctx) { Register register_destination = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType); MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - Register expected = programBuilder.getOrNewRegister(mainThread, ctx.constant().get(0).getText(), archType); - Register value = programBuilder.getOrNewRegister(mainThread, ctx.constant().get(1).getText(), archType); + Expression expected = (Expression) ctx.value(0).accept(this); + Expression value = (Expression) ctx.value(1).accept(this); String mo = ctx.mo().content; String scope = ctx.scope().content; if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { @@ -349,7 +349,7 @@ public Object visitFenceAlias(LitmusPTXParser.FenceAliasContext ctx) { @Override public Object visitBarrier(LitmusPTXParser.BarrierContext ctx) { - Expression fenceId = (Expression) ctx.barID().accept(this); + Expression fenceId = (Expression) ctx.value().accept(this); Event fence = EventFactory.newFenceWithId(ctx.getText().toLowerCase(), fenceId); return programBuilder.addChild(mainThread, fence); } diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index 1a34a15558..31bcfa82ae 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -55,5 +55,5 @@ litmus/PTX/Manual/MP-dlb-no-fence-2,1 litmus/PTX/Manual/LB-dlb,0 litmus/PTX/Manual/LB-dlb-no-fence-1,1 litmus/PTX/Manual/LB-dlb-no-fence-2,1 -litmus/PTX/Nvidia/SB+bar-dyn-reg-const,1 -litmus/PTX/Nvidia/SB+bar-sta-reg-const,0 +litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0 +litmus/PTX/Nvidia/SB+bar-sta-reg-const,1 diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index 2c7c425bba..2828bd12fd 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -114,11 +114,11 @@ litmus/PTX/Manual/Ticketlock-diff-gpu.litmus,1 litmus/PTX/Manual/Ticketlock-acq2rlx-1.litmus,0 litmus/PTX/Manual/Ticketlock-acq2rlx-2.litmus,1 litmus/PTX/Manual/Ticketlock-rel2rlx.litmus,1 -litmus/PTX/Manual/MP-dlb,0 -litmus/PTX/Manual/MP-dlb-no-fence-1,1 -litmus/PTX/Manual/MP-dlb-no-fence-2,1 -litmus/PTX/Manual/LB-dlb,0 -litmus/PTX/Manual/LB-dlb-no-fence-1,1 -litmus/PTX/Manual/LB-dlb-no-fence-2,1 -litmus/PTX/Nvidia/SB+bar-dyn-reg-const,1 -litmus/PTX/Nvidia/SB+bar-sta-reg-const,0 +litmus/PTX/Manual/MP-dlb.litmus,0 +litmus/PTX/Manual/MP-dlb-no-fence-1.litmus,1 +litmus/PTX/Manual/MP-dlb-no-fence-2.litmus,1 +litmus/PTX/Manual/LB-dlb.litmus,0 +litmus/PTX/Manual/LB-dlb-no-fence-1.litmus,1 +litmus/PTX/Manual/LB-dlb-no-fence-2.litmus,1 +litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0 +litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1 diff --git a/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus b/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus index cd7d1863b7..f1a401994e 100644 --- a/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus +++ b/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus @@ -11,7 +11,7 @@ P1:r3=0; st.relaxed.cta d, 1 | ld.weak r0, t ; | beq r0, r3, LC00 ; ld.weak r2, t | fence.sc.gpu ; - plus r2, r2, 1 | ld.relaxed.cta r1, d ; + add r2, r2, 1 | ld.relaxed.cta r1, d ; st.weak t, r2 | LC00: ; exists (P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus b/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus index 0907261fab..d16268f683 100644 --- a/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus +++ b/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus @@ -11,7 +11,7 @@ P1:r3=0; st.relaxed.cta d, 1 | ld.weak r0, t ; fence.sc.gpu | beq r0, r3, LC00 ; ld.weak r2, t | ; - plus r2, r2, 1 | ld.relaxed.cta r1, d ; + add r2, r2, 1 | ld.relaxed.cta r1, d ; st.weak t, r2 | LC00: ; exists (P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/MP-dlb.litmus b/litmus/PTX/Manual/MP-dlb.litmus index 9b43752f38..41e8e73b63 100644 --- a/litmus/PTX/Manual/MP-dlb.litmus +++ b/litmus/PTX/Manual/MP-dlb.litmus @@ -11,7 +11,7 @@ P1:r3=0; st.relaxed.cta d, 1 | ld.weak r0, t ; fence.sc.gpu | beq r0, r3, LC00 ; ld.weak r2, t | fence.sc.gpu ; - plus r2, r2, 1 | ld.relaxed.cta r1, d ; + add r2, r2, 1 | ld.relaxed.cta r1, d ; st.weak t, r2 | LC00: ; exists (P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file From 3f3c8ceba5886172e0595d9a4fcd5247d960aa42 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 08:32:23 +0200 Subject: [PATCH 2/2] Properly define asmo and fr in Vulkan (#528) Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- cat/ptx-v6.0.cat | 2 ++ cat/ptx-v7.5.cat | 2 ++ cat/spirv-check.cat | 11 +++++++++-- cat/spirv-nochains.cat | 12 +++++++++--- cat/spirv.cat | 13 ++++++++++--- dartagnan/src/test/resources/PTXv6_0-expected.csv | 1 + dartagnan/src/test/resources/PTXv7_5-expected.csv | 1 + dartagnan/src/test/resources/VULKAN-expected.csv | 1 + litmus/PTX/Manual/CoWW-RR.litmus | 12 ++++++++++++ litmus/VULKAN/Manual/CoWW-RR.litmus | 12 ++++++++++++ 10 files changed, 59 insertions(+), 8 deletions(-) create mode 100644 litmus/PTX/Manual/CoWW-RR.litmus create mode 100644 litmus/VULKAN/Manual/CoWW-RR.litmus diff --git a/cat/ptx-v6.0.cat b/cat/ptx-v6.0.cat index b712a3a354..85b9124ad7 100644 --- a/cat/ptx-v6.0.cat +++ b/cat/ptx-v6.0.cat @@ -17,7 +17,9 @@ PTX (*******************) // Explicitly add transitivity for coherence since the co in PTX is not total +// and recompute fr based on the new co let co = co+ +let fr = rf^-1; co (* Events *) let strong-write = W & (RLX | REL) diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index 2ee92f58b5..58868482f0 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -31,7 +31,9 @@ PTX (*******************) // Explicitly add transitivity for coherence since the co in PTX is not total +// and recompute fr based on the new co let co = co+ +let fr = rf^-1; co (* Events *) let strong-write = W & (RLX | REL) diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat index 9081cdb82c..0807636688 100644 --- a/cat/spirv-check.cat +++ b/cat/spirv-check.cat @@ -44,7 +44,8 @@ let inscope = (DV * DV) | (swg & ((DV | QF | WG) * (DV | QF | WG))) | (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG))) -let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id // mutually ordered atomics + // mutually ordered atomics + let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE)) | (SC0 * ((SEMAV | SEMVIS) & SEMSC0)) @@ -56,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) | let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po -let asmo = co & (ATOM * ATOM) +let asmo = co & ((ATOM | IW) * ATOM) +// From-read is defined based on scoped modification order +// instead of coherence. For reads that read-from init, they +// from-read all writes at the same location. +let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) +let fre = fr & ext + let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* diff --git a/cat/spirv-nochains.cat b/cat/spirv-nochains.cat index 1ba1adf98e..89941c8c89 100644 --- a/cat/spirv-nochains.cat +++ b/cat/spirv-nochains.cat @@ -57,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) | let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po -let asmo = co & (ATOM * ATOM) +let asmo = co & ((ATOM | IW) * ATOM) +// From-read is defined based on scoped modification order +// instead of coherence. For reads that read-from init, they +// from-read all writes at the same location. +let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) +let fre = fr & ext + let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* @@ -68,7 +74,7 @@ let sw = inscope & ( ([REL & ATOM]; rs; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) | // atomic->fence ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) | // fence->fence // (stor[CBAR]) terms are redundant because scbarinst is an equivalence relation on scbarinst, but they make the sequence of instructions more clear. - ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F]) // fence->cbar->cbar->fence, + ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F]) // fence->cbar->cbar->fence, ) let ithbsemsc0 = ( ssw | @@ -139,7 +145,7 @@ acyclic (locord | rf | fr | asmo) as consistency-cycle empty (rf; ([R \ ATOM])) & (([W]; locord); ([W]; locord)+) as consistency-rf // rmw events are atomic -empty rmw & (fre; coe) as atomic +empty rmw & (fre; (asmo & ext)) as atomic let non-rmw-reads = (R \ RMW) * (R \ RMW) empty ((((locord | locord^-1) | mutordatom) \ non-rmw-reads) \ (loc \ id \ non-rmw-reads)) as locord-complete diff --git a/cat/spirv.cat b/cat/spirv.cat index 8196d08d0f..d46758d168 100644 --- a/cat/spirv.cat +++ b/cat/spirv.cat @@ -44,7 +44,8 @@ let inscope = (DV * DV) | (swg & ((DV | QF | WG) * (DV | QF | WG))) | (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG))) -let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id // mutually ordered atomics +// mutually ordered atomics +let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE)) | (SC0 * ((SEMAV | SEMVIS) & SEMSC0)) @@ -56,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) | let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po -let asmo = co & (ATOM * ATOM) +let asmo = co & ((ATOM | IW) * ATOM) +// From-read is defined based on scoped modification order +// instead of coherence. For reads that read-from init, they +// from-read all writes at the same location. +let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) +let fre = fr & ext + let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* @@ -138,7 +145,7 @@ acyclic (locord | rf | fr | asmo) as consistency-cycle empty (rf; ([R \ ATOM])) & (([W]; locord); ([W]; locord)+) as consistency-rf // rmw events are atomic -empty rmw & (fre; coe) as atomic +empty rmw & (fre; (asmo & ext)) as atomic let non-rmw-reads = (R \ RMW) * (R \ RMW) empty ((((locord | locord^-1) | mutordatom) \ non-rmw-reads) \ (loc \ id \ non-rmw-reads)) as locord-complete diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index 31bcfa82ae..b07d6dd039 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -57,3 +57,4 @@ litmus/PTX/Manual/LB-dlb-no-fence-1,1 litmus/PTX/Manual/LB-dlb-no-fence-2,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const,1 +litmus/PTX/Manual/CoWW-weak.litmus,1 diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index 2828bd12fd..0f3fba15a6 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -122,3 +122,4 @@ litmus/PTX/Manual/LB-dlb-no-fence-1.litmus,1 litmus/PTX/Manual/LB-dlb-no-fence-2.litmus,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1 +litmus/PTX/Manual/CoWW-weak.litmus,1 diff --git a/dartagnan/src/test/resources/VULKAN-expected.csv b/dartagnan/src/test/resources/VULKAN-expected.csv index 66565bf071..0b42481b11 100644 --- a/dartagnan/src/test/resources/VULKAN-expected.csv +++ b/dartagnan/src/test/resources/VULKAN-expected.csv @@ -83,3 +83,4 @@ litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus,0 litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1 litmus/VULKAN/Manual/MP-avvis.litmus,0 litmus/VULKAN/Manual/MP-no-avvis.litmus,1 +litmus/VULKAN/Manual/CoWW-RR.litmus,1 diff --git a/litmus/PTX/Manual/CoWW-RR.litmus b/litmus/PTX/Manual/CoWW-RR.litmus new file mode 100644 index 0000000000..72f90e87ff --- /dev/null +++ b/litmus/PTX/Manual/CoWW-RR.litmus @@ -0,0 +1,12 @@ +PTX CoWW-RR +"Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread" +{ +P1:r0 = 0; +P1:r1 = 0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 0,gpu 0 ; + st.weak x, 1 | ld.weak r0, x ; + st.weak x, 2 | ld.weak r1, x ; +exists +(P1:r0 == 2 /\ P1:r1 == 1) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/CoWW-RR.litmus b/litmus/VULKAN/Manual/CoWW-RR.litmus new file mode 100644 index 0000000000..bc1dd8bd9a --- /dev/null +++ b/litmus/VULKAN/Manual/CoWW-RR.litmus @@ -0,0 +1,12 @@ +Vulkan CoWW-RR +"Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread" +{ +P1:r0 = 0; +P1:r1 = 0; +x=0; +} + P0@sg 0, wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; + st.sc0 x, 1 | ld.sc0 r0, x ; + st.sc0 x, 2 | ld.sc0 r1, x ; +exists +(P1:r0 == 2 /\ P1:r1 == 1) \ No newline at end of file