Skip to content

Commit

Permalink
Fix benchmarks with ACQ+REL = SEMSC0 + SEMC1 problem
Browse files Browse the repository at this point in the history
  • Loading branch information
@hernan-poncedeleon @hernanponcedeleon
hernan-poncedeleon authored and hernanponcedeleon committed Nov 30, 2023
1 parent 8be3663 commit dcd0c4d
Show file tree
Hide file tree
Showing 7 changed files with 54 additions and 54 deletions.
4 changes: 2 additions & 2 deletions litmus/VULKAN/Manual/PC-bar-atom.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
4 changes: 2 additions & 2 deletions litmus/VULKAN/Manual/PC-bar-nonpriv.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
20 changes: 10 additions & 10 deletions litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
20 changes: 10 additions & 10 deletions litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
20 changes: 10 additions & 10 deletions litmus/VULKAN/Manual/ticketlock-diff-wg.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
20 changes: 10 additions & 10 deletions litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
20 changes: 10 additions & 10 deletions litmus/VULKAN/Manual/ticketlock-same-wg.litmus
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

0 comments on commit dcd0c4d

Please sign in to comment.