From 4b84cc82c3dc3bc5549878502c9232926a4cb7c7 Mon Sep 17 00:00:00 2001 From: haining Date: Wed, 10 Jan 2024 22:29:54 +0200 Subject: [PATCH] add memalloy-ptx tests (#600) --- dartagnan/src/main/antlr4/LitmusPTX.g4 | 2 +- .../src/test/resources/PTXv6_0-expected.csv | 6 ++++++ .../src/test/resources/PTXv7_5-expected.csv | 6 ++++++ litmus/PTX/Manual/LB-dlb-no-fence-1.litmus | 4 ++-- litmus/PTX/Manual/LB-dlb-no-fence-2.litmus | 4 ++-- litmus/PTX/Manual/LB-dlb.litmus | 4 ++-- litmus/PTX/Manual/MP-dlb-no-fence-1.litmus | 4 ++-- litmus/PTX/Manual/MP-dlb-no-fence-2.litmus | 4 ++-- litmus/PTX/Manual/SL-cas-minus.litmus | 4 ++-- litmus/PTX/Manual/SL-cas-plus.litmus | 4 ++-- litmus/PTX/Manual/SL-future-minus.litmus | 6 +++--- litmus/PTX/Manual/SL-future-plus.litmus | 4 ++-- litmus/PTX/Memalloy/IRIW_gl_cta.litmus | 18 +++++++++++++++++ litmus/PTX/Memalloy/IRIW_uniproc.litmus | 18 +++++++++++++++++ litmus/PTX/Memalloy/IRRWIW_uniproc.litmus | 19 ++++++++++++++++++ litmus/PTX/Memalloy/IRWIW_gl_cta.litmus | 20 +++++++++++++++++++ litmus/PTX/Memalloy/README.md | 1 + litmus/PTX/Memalloy/RWC_uniproc.litmus | 18 +++++++++++++++++ litmus/PTX/Memalloy/WRR+2W.litmus | 19 ++++++++++++++++++ 19 files changed, 145 insertions(+), 20 deletions(-) create mode 100644 litmus/PTX/Memalloy/IRIW_gl_cta.litmus create mode 100644 litmus/PTX/Memalloy/IRIW_uniproc.litmus create mode 100644 litmus/PTX/Memalloy/IRRWIW_uniproc.litmus create mode 100644 litmus/PTX/Memalloy/IRWIW_gl_cta.litmus create mode 100644 litmus/PTX/Memalloy/README.md create mode 100644 litmus/PTX/Memalloy/RWC_uniproc.litmus create mode 100644 litmus/PTX/Memalloy/WRR+2W.litmus diff --git a/dartagnan/src/main/antlr4/LitmusPTX.g4 b/dartagnan/src/main/antlr4/LitmusPTX.g4 index 25e5d62f9a..43b86f3b23 100644 --- a/dartagnan/src/main/antlr4/LitmusPTX.g4 +++ b/dartagnan/src/main/antlr4/LitmusPTX.g4 @@ -107,7 +107,7 @@ loadInstruction ; localValue - : load Period mo (Period scope)? register Comma value + : load register Comma value ; localAdd diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index 4deda48732..dabc7e3aac 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -78,3 +78,9 @@ litmus/PTX/Manual/PC-bar-sync-sync-1.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-2.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-3.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-4.litmus,1 +litmus/PTX/Memalloy/IRIW_gl_cta.litmus,1 +litmus/PTX/Memalloy/IRIW_uniproc.litmus,1 +litmus/PTX/Memalloy/IRRWIW_uniproc.litmus,1 +litmus/PTX/Memalloy/IRWIW_gl_cta.litmus,1 +litmus/PTX/Memalloy/RWC_uniproc.litmus,1 +litmus/PTX/Memalloy/WRR+2W.litmus,1 diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index dbc40933ff..7398021682 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -207,3 +207,9 @@ litmus/PTX/Manual/PC-bar-sync-sync-1.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-2.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-3.litmus,1 litmus/PTX/Manual/PC-bar-sync-sync-4.litmus,1 +litmus/PTX/Memalloy/IRIW_gl_cta.litmus,1 +litmus/PTX/Memalloy/IRIW_uniproc.litmus,1 +litmus/PTX/Memalloy/IRRWIW_uniproc.litmus,1 +litmus/PTX/Memalloy/IRWIW_gl_cta.litmus,1 +litmus/PTX/Memalloy/RWC_uniproc.litmus,1 +litmus/PTX/Memalloy/WRR+2W.litmus,1 diff --git a/litmus/PTX/Manual/LB-dlb-no-fence-1.litmus b/litmus/PTX/Manual/LB-dlb-no-fence-1.litmus index 0fdf290d0c..fae0decfad 100644 --- a/litmus/PTX/Manual/LB-dlb-no-fence-1.litmus +++ b/litmus/PTX/Manual/LB-dlb-no-fence-1.litmus @@ -8,8 +8,8 @@ h=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - atom.relaxed.gpu.cas r0, h, 0, 1 | ld.relaxed.gpu r1, t ; + atom.relaxed.gpu.cas r0, h, 0, 1 | ld.weak r1, t ; | fence.sc.gpu ; - st.relaxed.gpu t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; + st.weak t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; exists (P0:r0 == 1 /\ P1:r1 == 1) \ No newline at end of file diff --git a/litmus/PTX/Manual/LB-dlb-no-fence-2.litmus b/litmus/PTX/Manual/LB-dlb-no-fence-2.litmus index 4252b780ed..f9d175d9b8 100644 --- a/litmus/PTX/Manual/LB-dlb-no-fence-2.litmus +++ b/litmus/PTX/Manual/LB-dlb-no-fence-2.litmus @@ -8,8 +8,8 @@ h=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - atom.relaxed.gpu.cas r0, h, 0, 1 | ld.relaxed.gpu r1, t ; + atom.relaxed.gpu.cas r0, h, 0, 1 | ld.weak r1, t ; fence.sc.gpu | ; - st.relaxed.gpu t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; + st.weak t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; exists (P0:r0 == 1 /\ P1:r1 == 1) \ No newline at end of file diff --git a/litmus/PTX/Manual/LB-dlb.litmus b/litmus/PTX/Manual/LB-dlb.litmus index fe853b8ba2..55efc46e6e 100644 --- a/litmus/PTX/Manual/LB-dlb.litmus +++ b/litmus/PTX/Manual/LB-dlb.litmus @@ -8,8 +8,8 @@ h=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - atom.relaxed.gpu.cas r0, h, 0, 1 | ld.relaxed.gpu r1, t ; + atom.relaxed.gpu.cas r0, h, 0, 1 | ld.weak r1, t ; fence.sc.gpu | fence.sc.gpu ; - st.relaxed.gpu t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; + st.weak t, 1 | atom.relaxed.gpu.cas r3, h, 0, 1 ; exists (P0:r0 == 1 /\ P1:r1 == 1) \ No newline at end of file diff --git a/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus b/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus index 4fbf0fa57b..e2b895e581 100644 --- a/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus +++ b/litmus/PTX/Manual/MP-dlb-no-fence-1.litmus @@ -8,10 +8,10 @@ d=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - st.relaxed.gpu d, 1 | ld.weak r0, t ; + st.weak d, 1 | ld.weak r0, t ; | beq r0, r3, LC00 ; ld.weak r2, t | fence.sc.gpu ; - add r2, r2, 1 | ld.relaxed.gpu r1, d ; + add r2, r2, 1 | ld.weak 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 162ee62861..b81a3862b1 100644 --- a/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus +++ b/litmus/PTX/Manual/MP-dlb-no-fence-2.litmus @@ -8,10 +8,10 @@ d=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - st.relaxed.gpu d, 1 | ld.weak r0, t ; + st.weak d, 1 | ld.weak r0, t ; fence.sc.gpu | beq r0, r3, LC00 ; ld.weak r2, t | ; - add r2, r2, 1 | ld.relaxed.gpu r1, d ; + add r2, r2, 1 | ld.weak 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/SL-cas-minus.litmus b/litmus/PTX/Manual/SL-cas-minus.litmus index 3cccb371fa..266c854559 100644 --- a/litmus/PTX/Manual/SL-cas-minus.litmus +++ b/litmus/PTX/Manual/SL-cas-minus.litmus @@ -11,9 +11,9 @@ P1:r2=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - st.relaxed.gpu x, 1 | atom.relaxed.gpu.cas r1, m, 0, 1 ; + st.weak x, 1 | atom.relaxed.gpu.cas r1, m, 0, 1 ; atom.relaxed.gpu.exch r0, m, 0 | bne r1, 0, LC00 ; - | ld.relaxed.gpu r3, x ; + | ld.weak r3, x ; | LC00: ; exists (P1:r1 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/SL-cas-plus.litmus b/litmus/PTX/Manual/SL-cas-plus.litmus index ba9a8ccd66..7c4c58bf5c 100644 --- a/litmus/PTX/Manual/SL-cas-plus.litmus +++ b/litmus/PTX/Manual/SL-cas-plus.litmus @@ -11,10 +11,10 @@ P1:r2=0; P1:r3=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - st.relaxed.gpu x, 1 | atom.relaxed.gpu.cas r1, m, 0, 1 ; + st.weak x, 1 | atom.relaxed.gpu.cas r1, m, 0, 1 ; fence.sc.gpu | bne r1, 0, LC00 ; atom.relaxed.gpu.exch r0, m, 0 | fence.sc.gpu ; - | ld.relaxed.gpu r3, x ; + | ld.weak r3, x ; | LC00: ; exists (P1:r1 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/SL-future-minus.litmus b/litmus/PTX/Manual/SL-future-minus.litmus index b29c5a887a..1d2fd3451e 100644 --- a/litmus/PTX/Manual/SL-future-minus.litmus +++ b/litmus/PTX/Manual/SL-future-minus.litmus @@ -10,9 +10,9 @@ P0:r1=0; P1:r2=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - ld.relaxed.gpu r0, x | atom.relaxed.gpu.cas r2, m, 0, 1 ; - st.relaxed.gpu m, 0 | bne r2, 0, LC00 ; - fence.sc.gpu | st.relaxed.gpu x, 1 ; + ld.weak r0, x | atom.relaxed.gpu.cas r2, m, 0, 1 ; + st.weak m, 0 | bne r2, 0, LC00 ; + fence.sc.gpu | st.weak x, 1 ; | LC00: ; exists (P0:r0 == 1 /\ P1:r2 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/SL-future-plus.litmus b/litmus/PTX/Manual/SL-future-plus.litmus index ac24042f0a..cf2efaf4f0 100644 --- a/litmus/PTX/Manual/SL-future-plus.litmus +++ b/litmus/PTX/Manual/SL-future-plus.litmus @@ -10,10 +10,10 @@ P0:r1=0; P1:r2=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - ld.relaxed.gpu r0, x | atom.relaxed.gpu.cas r2, m, 0, 1 ; + ld.weak r0, x | atom.relaxed.gpu.cas r2, m, 0, 1 ; fence.sc.gpu | bne r2, 0, LC00 ; atom.relaxed.gpu.exch r1, m, 0 | fence.sc.gpu ; - | st.relaxed.gpu x, 1 ; + | st.weak x, 1 ; | LC00: ; exists (P0:r0 == 1 /\ P1:r2 == 0) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/IRIW_gl_cta.litmus b/litmus/PTX/Memalloy/IRIW_gl_cta.litmus new file mode 100644 index 0000000000..f1cb163f81 --- /dev/null +++ b/litmus/PTX/Memalloy/IRIW_gl_cta.litmus @@ -0,0 +1,18 @@ +PTX IRIW_gl_cta +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/IRIW_gl_cta/IRIW_gl_cta.txt" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P3:r0=0; +P3:r2=0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + ld r0, 1 | ld.weak r0, x | ld r0, 1 | ld.weak r0, x ; + st.weak x, r0 | fence.sc.gpu | st.weak x, r0 | fence.sc.cta ; + | ld.weak r2, x | | ld.weak r2, x ; +exists +(P1:r0 == 1 /\ P1:r2 == 0 /\ P3:r0 == 1 /\ P3:r2 == 0) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/IRIW_uniproc.litmus b/litmus/PTX/Memalloy/IRIW_uniproc.litmus new file mode 100644 index 0000000000..7c003f1cb8 --- /dev/null +++ b/litmus/PTX/Memalloy/IRIW_uniproc.litmus @@ -0,0 +1,18 @@ +PTX IRIW_uniproc +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/IRIW_uniproc/IRIW_uniproc.litmus" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P3:r0=0; +P3:r2=0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + ld r0, 1 | ld.weak r0, x | ld r0, 2 | ld.weak r0, x ; + st.weak x, r0 | fence.sc.cta | st.weak x, r0 | fence.sc.gpu ; + | ld.weak r2, x | | ld.weak r2, x ; +exists +(P1:r0 == 1 /\ P1:r2 == 0 /\ P3:r0 == 2 /\ P3:r2 == 2 /\ x == 1) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/IRRWIW_uniproc.litmus b/litmus/PTX/Memalloy/IRRWIW_uniproc.litmus new file mode 100644 index 0000000000..f4f7439d02 --- /dev/null +++ b/litmus/PTX/Memalloy/IRRWIW_uniproc.litmus @@ -0,0 +1,19 @@ +PTX IRRWIW_uniproc +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/IRRWIW_uniproc/IRRWIW_uniproc.litmus" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P3:r0=0; +P3:r2=0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + ld r0, 1 | ld.weak r0, x | ld r0, 2 | ld r2, 3 ; + st.weak x, r0 | fence.sc.cta | st.weak x, r0 | ld.weak r0, x ; + | ld.weak r2, x | | fence.sc.gpu ; + | | | st.weak x, r2 ; +exists +(P1:r0 == 1 /\ P1:r2 == 0 /\ P3:r0 == 2 /\ x == 1) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/IRWIW_gl_cta.litmus b/litmus/PTX/Memalloy/IRWIW_gl_cta.litmus new file mode 100644 index 0000000000..19e922757c --- /dev/null +++ b/litmus/PTX/Memalloy/IRWIW_gl_cta.litmus @@ -0,0 +1,20 @@ +PTX IRWIW_gl_cta +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/IRWIW_gl_cta/IRWIW_gl_cta.litmus" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P3:r0=0; +P3:r2=0; +x=0; +y=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + ld r0, 2 | ld r2, 1 | ld r0, 2 | ld r2, 2 ; + st.weak x, r0 | ld.weak r0, x | st.weak y, r0 | ld.weak r0, y ; + | fence.sc.gpu | | fence.sc.cta ; + | st.weak y, r2 | | st.weak x, r2 ; +exists +(P1:r0 == 2 /\ P3:r0 == 2 /\ x == 2 /\ y == 2) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/README.md b/litmus/PTX/Memalloy/README.md new file mode 100644 index 0000000000..33ec5a41b8 --- /dev/null +++ b/litmus/PTX/Memalloy/README.md @@ -0,0 +1 @@ +The tests in this folder were manually written using the tests from the [memalloy](https://github.com/johnwickerson/memalloy) repository as a guide. \ No newline at end of file diff --git a/litmus/PTX/Memalloy/RWC_uniproc.litmus b/litmus/PTX/Memalloy/RWC_uniproc.litmus new file mode 100644 index 0000000000..19af8ca7e3 --- /dev/null +++ b/litmus/PTX/Memalloy/RWC_uniproc.litmus @@ -0,0 +1,18 @@ +PTX RWC_uniproc +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/RWC_uniproc/RWC_uniproc.litmus" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P2:r2=0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + ld r0, 1 | ld.weak r0, x | ld r0, 2 ; + st.weak x, r0 | fence.sc.cta | st.weak x, r0 ; + | ld.weak r2, x | fence.sc.gpu ; + | | ld.weak r2, x ; +exists +(P1:r0 == 1 /\ P1:r2 == 0 /\ P2:r2 == 2 /\ x == 1) \ No newline at end of file diff --git a/litmus/PTX/Memalloy/WRR+2W.litmus b/litmus/PTX/Memalloy/WRR+2W.litmus new file mode 100644 index 0000000000..55292fb4fd --- /dev/null +++ b/litmus/PTX/Memalloy/WRR+2W.litmus @@ -0,0 +1,19 @@ +PTX WRR+2W +"CoRR" +"https://github.com/johnwickerson/memalloy/blob/master/ptx_testing/WRR%2B2W_uniproc/WRR%2B2W.litmus" +{ +P0:r0=0; +P1:r0=0; +P1:r2=0; +P2:r0=0; +P2:r2=0; +x=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + ld r0, 1 | ld.weak r0, x | ld r0, 2 ; + st.weak x, r0 | fence.sc.cta | ld r2, 3 ; + | ld.weak r2, x | st.weak x, r0 ; + | | fence.sc.gpu ; + | | st.weak x, r2 ; +exists +(P1:r0 == 1 /\ P1:r2 == 0 /\ x == 1) \ No newline at end of file