diff --git a/litmus/VULKAN/Manual/PC-bar-atom.litmus b/litmus/VULKAN/Manual/PC-bar-atom.litmus index 2103246d7d..04ea17b6d7 100644 --- a/litmus/VULKAN/Manual/PC-bar-atom.litmus +++ b/litmus/VULKAN/Manual/PC-bar-atom.litmus @@ -7,7 +7,7 @@ x=0; P0:r0=0 } P0@sg 0, wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - ld.atom.wg.sc0 r0, x | cbar.wg.semsc0 0 ; - cbar.wg.semsc0 0 | st.atom.wg.sc0 x, 1 ; + ld.atom.wg.sc0 r0, x | cbar.wg 0 ; + cbar.wg 0 | st.atom.wg.sc0 x, 1 ; ~exists (P0:r0 == 1) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/PC-bar-nonpriv.litmus b/litmus/VULKAN/Manual/PC-bar-nonpriv.litmus index 0c641d6635..3afc4d08a6 100644 --- a/litmus/VULKAN/Manual/PC-bar-nonpriv.litmus +++ b/litmus/VULKAN/Manual/PC-bar-nonpriv.litmus @@ -7,7 +7,7 @@ x=0; P0:r0=0 } P0@sg 0, wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - ld.nonpriv.sc0 r0, x | cbar.wg.semsc0 0 ; - cbar.wg.semsc0 0 | st.nonpriv.sc0 x, 1 ; + ld.nonpriv.sc0 r0, x | cbar.wg 0 ; + cbar.wg 0 | st.nonpriv.sc0 x, 1 ; ~exists (P0:r0 == 1) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus b/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus index 3b357ae285..858aeb1aab 100644 --- a/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus +++ b/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus @@ -4,15 +4,15 @@ VULKAN ticketlock-acq2rlx-1 in=0; out=0; x=0; } - P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; - LC00: | LC00: ; - ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; - beq r1, r2, LC01 | beq r1, r2, LC01 ; - goto LC00 | goto LC00 ; - LC01: | LC01: ; - ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; - st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; + P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; + rmw.atom.wg.sc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; + LC00: | LC00: ; + ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; + beq r1, r2, LC01 | beq r1, r2, LC01 ; + goto LC00 | goto LC00 ; + LC01: | LC01: ; + ld.nonpriv.sc0 r3, x | ld.nonpriv.sc0 r3, x ; + st.nonpriv.sc0 x, 1 | st.nonpriv.sc0 x, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus b/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus index a0b41290cc..b5b3ae12a7 100644 --- a/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus +++ b/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus @@ -4,15 +4,15 @@ VULKAN ticketlock-acq2rlx-2 in=0; out=0; x=0; } - P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; - LC00: | LC00: ; - ld.atom.wg.sc0.semsc0 r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; - beq r1, r2, LC01 | beq r1, r2, LC01 ; - goto LC00 | goto LC00 ; - LC01: | LC01: ; - ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; - st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; + P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; + LC00: | LC00: ; + ld.atom.wg.sc0 r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; + beq r1, r2, LC01 | beq r1, r2, LC01 ; + goto LC00 | goto LC00 ; + LC01: | LC01: ; + ld.nonpriv.sc0 r3, x | ld.nonpriv.sc0 r3, x ; + st.nonpriv.sc0 x, 1 | st.nonpriv.sc0 x, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus b/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus index 85f9faec37..8ebe2f03ed 100644 --- a/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus +++ b/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus @@ -4,15 +4,15 @@ VULKAN ticketlock-rel2rlx in=0; out=0; x=0; } - P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; - LC00: | LC00: ; - ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; - beq r1, r2, LC01 | beq r1, r2, LC01 ; - goto LC00 | goto LC00 ; - LC01: | LC01: ; - ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; - st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; + P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; + LC00: | LC00: ; + ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; + beq r1, r2, LC01 | beq r1, r2, LC01 ; + goto LC00 | goto LC00 ; + LC01: | LC01: ; + ld.nonpriv.sc0 r3, x | ld.nonpriv.sc0 r3, x ; + st.nonpriv.sc0 x, 1 | st.nonpriv.sc0 x, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus b/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus index 495a384224..076680f354 100644 --- a/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus +++ b/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus @@ -4,15 +4,15 @@ VULKAN ticketlock-same-wg in=0; out=0; x=0; } - P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; - LC00: | LC00: ; - ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; - beq r1, r2, LC01 | beq r1, r2, LC01 ; - goto LC00 | goto LC00 ; - LC01: | LC01: ; - ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; - st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.wg.sc0.semsc0.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; + P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; + LC00: | LC00: ; + ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; + beq r1, r2, LC01 | beq r1, r2, LC01 ; + goto LC00 | goto LC00 ; + LC01: | LC01: ; + ld.nonpriv.sc0 r3, x | ld.nonpriv.sc0 r3, x ; + st.nonpriv.sc0 x, 1 | st.nonpriv.sc0 x, 1 ; + rmw.atom.wg.sc0.semsc0.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-same-wg.litmus b/litmus/VULKAN/Manual/ticketlock-same-wg.litmus index 673cd2b843..94f7447885 100644 --- a/litmus/VULKAN/Manual/ticketlock-same-wg.litmus +++ b/litmus/VULKAN/Manual/ticketlock-same-wg.litmus @@ -4,15 +4,15 @@ VULKAN ticketlock-same-wg in=0; out=0; x=0; } - P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; - LC00: | LC00: ; - ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; - beq r1, r2, LC01 | beq r1, r2, LC01 ; - goto LC00 | goto LC00 ; - LC01: | LC01: ; - ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; - st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; + P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; + LC00: | LC00: ; + ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; + beq r1, r2, LC01 | beq r1, r2, LC01 ; + goto LC00 | goto LC00 ; + LC01: | LC01: ; + ld.nonpriv.sc0 r3, x | ld.nonpriv.sc0 r3, x ; + st.nonpriv.sc0 x, 1 | st.nonpriv.sc0 x, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file