Tue Dec 29 09:21:00 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw000
"DpdR LwSyncsRW Rfe LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | xor r3,r1,r1 | lwsync | xor r3,r1,r1 ;
li r3,2 | lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
stw r3,0(r2) | lwsync | stw r3,0(r2) | lwsync ;
| li r6,1 | | li r6,1 ;
| stw r6,0(r5) | | stw r6,0(r5) ;
exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 30,10,9
_litmus_P3_3_: lwsync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 7,0(9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 7,0(9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bclwsrw000 Allowed
Histogram (80 states)
2 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
42 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
14 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
412 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
2 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
8 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
37 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
447 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
7 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
11 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
115 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
16 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
171 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
15 :>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2717 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
35 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
367 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
290 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
44 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
212 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
28 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
374 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
8 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
153 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
54 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
4561 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
98 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
14383 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
4604 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3667 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
586 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
3116 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
17437 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
7322 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
121 :>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1619 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
5559 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
16202 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
18002 :>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
153474:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
50 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
6884 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
15086 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
543181:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1835553:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
5032 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2507 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
195121:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
1884 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
5101 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
6081 :>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
35894 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1404017:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
86 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
9611 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
18798 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
1284662:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
715310:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
16696 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
323034:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3382 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2235 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
10456 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
306572:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
2692 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
7580 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
49334 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
74434 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
1832707:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
94934 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
1686104:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
1492 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
101768:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
113033:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
806018:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
1198 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
1212948:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
148339084:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
13022713:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
145650396:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=2cd7bba2d47d08c57cdb5c01d1ab5803
Cycle=DpdR LwSyncsRW Rfe LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw000 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw000 70.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw001
"DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync | xor r3,r1,r1 ;
lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
lwsync | stw r3,0(r2) | lwsync ;
li r6,1 | | li r6,1 ;
stw r6,0(r5) | | stw r6,0(r5) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw001 Allowed
Histogram (17 states)
34 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
1892 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
64 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4247 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
257 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
59403 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
77057 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
2819753:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
2711816:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
511178:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
159647854:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
8650325:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
220620210:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
2115472:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4342 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
17372 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
2758724:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=2f27c228a337798a8409128f0e839ede
Cycle=DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw001 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw001 33.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw002
"SyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync | sync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
lwsync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | lwsync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 29,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: lwsync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw002 Allowed
Histogram (30 states)
11 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
3 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
9 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
15 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
79 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
1433 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
406 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
13 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
824 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
6 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
226 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
62025 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
10751 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
58115 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
113547:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
2040942:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
75274 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
972 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
3746953:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
6334 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1272355:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
4468113:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
2649493:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
118224680:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1148 :>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
266371255:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
1 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
895014:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=425f7ff81484948d2280c1ec43353c48
Cycle=SyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw002 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw002 35.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw003
"LwSyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync | lwsync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
lwsync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | lwsync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 29,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: lwsync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw003 Allowed
Histogram (28 states)
1 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
3 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
56 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
5 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2375 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
239 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
313 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
4 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
15205 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
45 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
15525 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
2969 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
335525:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
240 :>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2026108:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
30367 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3153574:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
9643811:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
9069 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1522236:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
120945023:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
964319:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
254081224:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
93766 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
153097:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3665500:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3339400:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=0aed6f5e4734fb8fd04865e50a598856
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw003 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw003 36.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw004
"DpdW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | xor r3,r1,r1 ;
sync | li r3,2 | li r4,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 4,0(11)
_litmus_P2_1_: xor 5,4,4
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,5,9
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw004 Allowed
Histogram (22 states)
17 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
13 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
5 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
4 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
6 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
6 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
18 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
39 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
385 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3005 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
150 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
136 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
187073:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
1752 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
350356:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
1544 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
2902376:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
37459 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
5889116:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
384399729:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
1471 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
6225340:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=09fcfa7799cf0e228eb4f62e08bff0c4
Cycle=DpdW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw004 No BCLwSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bclwsrw004 37.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw005
"SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | sync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 5,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw005 Allowed
Histogram (22 states)
237 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
11 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
23 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
46 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
63 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
27 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
100 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
814 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
68761 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
4577 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
1539148:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
4364832:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
126944:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
266959:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
7192435:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
704 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
358297:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
350204162:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
30969817:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
1039 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
30185 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
4870819:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=f7e3765a1295f9e21cc78bf562fdd37e
Cycle=SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw005 No BCLwSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bclwsrw005 38.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw006
"LwSyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | lwsync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 5,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw006 Allowed
Histogram (22 states)
4 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
16 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
43 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
56 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
38 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
52 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
4013 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
15 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
469 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
307144312:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
91215 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
272961:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
4487831:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
602 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3813 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
100198:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
82808118:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
1234 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
27446 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
4905369:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
23031 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
129164:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=354ee334787e30f2c0e6c3aa84959816
Cycle=LwSyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw006 No BCLwSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bclwsrw006 39.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw007
"DpdR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | xor r3,r1,r1 ;
sync | li r3,2 | lwzx r4,r3,r5 ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 4,10,9
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw007 Allowed
Histogram (19 states)
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
7 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
21 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
79 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
17 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
474 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
2314 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
90494 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
12331050:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1745 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
4158075:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
1204 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
21293 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
6194573:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
1423 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
163670:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
377033557:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=d3ebd0130f5f22c064cad06ccbecce5e
Cycle=DpdR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw007 No BCLwSyncsRW
Safe=Fre SyncsWR DpdR
Time bclwsrw007 32.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw008
"SyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | sync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 4,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw008 Allowed
Histogram (17 states)
12 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
237 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
32 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
46 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
1028 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
17865 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
160738:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
149865:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
1093 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
3845048:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
3908089:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
7371112:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
648 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
4697 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
133223:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
335728628:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
48677639:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=9567e26c5742196dbcac25b4fb763766
Cycle=SyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw008 No BCLwSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bclwsrw008 34.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw009
"LwSyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | lwsync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
lwsync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 4,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw009 Allowed
Histogram (19 states)
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
4 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
14 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
164 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
42 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
47 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
166 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
624 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
3681 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
473560:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
1837088:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
5800350:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
1106 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
12859 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
4467643:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
40361 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
146873:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
330992638:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
56222779:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=bb9b9e63b559c6e43dcf679ffa8398cb
Cycle=LwSyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw009 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bclwsrw009 34.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw010
"DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
sync | lwsync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | lwsync ;
lwzx r5,r4,r6 | | li r6,1 ;
lwsync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 29,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw010 Allowed
Histogram (22 states)
41 :>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
62 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
38 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
48 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
585 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
4727 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
30 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
1400 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
9318 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
186574:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
3111505:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
5154665:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
808 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5991993:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
535737:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
1208448:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
298238601:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
6754062:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
77682400:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
1197 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
38439 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
1079322:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=093579cdc7d8f214af6101115f0d8b4c
Cycle=DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw010 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw010 33.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw011
"DpdR LwSyncsRW Rfe LwSyncsRR DpdR LwSyncsRW Rfe LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | lwsync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | lwsync ;
lwzx r5,r4,r6 | | li r6,1 ;
lwsync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 29,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw011 Allowed
Histogram (22 states)
10 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
22 :>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
290 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
1831 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
126 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
3971 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
2816 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
48904 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
25904 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
1030417:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
1073861:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
285412:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
81009258:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
10381931:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9221 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
7907 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
2934444:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
747869:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
299577038:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
2858764:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=4be537dfd1e39a4c98845248feca8b29
Cycle=DpdR LwSyncsRW Rfe LwSyncsRR DpdR LwSyncsRW Rfe LwSyncsRW Rfe
Relax bclwsrw011 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw011 35.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw012
"DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
lwsync | lwsync ;
li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 4,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw012 Allowed
Histogram (3 states)
310471805:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0;
29904309:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0;
299623886:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=138606a77ccb32f9d127a952601f26cc
Cycle=DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw012 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw012 20.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw013
"DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
lwsync | lwsync | lwsync ;
li r6,1 | li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 4,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 4,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw013 Allowed
Histogram (7 states)
133665:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
70268177:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
73859445:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
65343839:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
61545027:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
58800083:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
70049764:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=c2348c97f33f2ba898984873da5d4807
Cycle=DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw013 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw013 33.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw014
"DpsR LwSyncsRW Rfe DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe"
{0:r2=y; 0:r5=x; 1:r2=x; 1:r5=y; 2:r2=y;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r2 ;
lwsync | lwsync | lwsync ;
li r6,1 | li r6,1 | li r5,2 ;
stw r6,0(r5) | stw r6,0(r5) | stw r5,0(r2) ;
exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 4,0(9)
_litmus_P2_1_: xor 10,4,4
_litmus_P2_2_: lwzx 11,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,2
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw014 Allowed
Histogram (20 states)
1 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
24 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
275 :>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
3070 :>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
756 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
511 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
2471545:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
6 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
38 :>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
44971 :>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
3393762:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
3575011:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
4476 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
8230 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
2989313:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
201516491:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
2518022:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
36672 :>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
178502414:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
4934412:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=f2c235590f3eee5e0325effcdbb3b7a4
Cycle=DpsR LwSyncsRW Rfe DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw014 No BCLwSyncsRW
Safe=DpsR DpdR
Time bclwsrw014 33.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw015
"SyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
lwsync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | lwsync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: lwsync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw015 Allowed
Histogram (4 states)
836180:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
474009809:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
800605:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
164353406:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=7fd3dfd255f25b83fe014eed6c45b685
Cycle=SyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw015 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw015 21.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw016
"LwSyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
lwsync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | lwsync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: lwsync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw016 Allowed
Histogram (4 states)
241242:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
451317372:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
9028873:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
179412513:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=898c0b81592367ec9511da918b08041e
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw016 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw016 21.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw017
"DpdW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 ;
lwz r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: xor 5,4,4
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,5,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw017 Allowed
Histogram (4 states)
628795536:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
537 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
5779 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
11198148:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=20086dd564a511b714a1da610330fdea
Cycle=DpdW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw017 No BCLwSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bclwsrw017 24.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw018
"SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 6,1
_litmus_P1_3_: stw 6,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw018 Allowed
Histogram (4 states)
8983 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
47807 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
23505592:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
616437618:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=f68fe5834d4a291ee56368caf658541c
Cycle=SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw018 No BCLwSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bclwsrw018 26.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw019
"DpdR SyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw019 Allowed
Histogram (6 states)
227629314:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
1185973:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
100780:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
492220:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
1311257:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
409280456:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=b29e6d271ad79fd47834aeea490fe672
Cycle=DpdR SyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw019 No BCLwSyncsRW
Safe=Wse SyncsWR SyncsRW DpdR
Time bclwsrw019 26.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw020
"LwSyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 6,1
_litmus_P1_3_: stw 6,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw020 Allowed
Histogram (4 states)
6679 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
622207150:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
71996 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
17714175:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=2af7591a084823d06f5daf38cddf2810
Cycle=LwSyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw020 No BCLwSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bclwsrw020 23.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw021
"DpdR LwSyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw021 Allowed
Histogram (6 states)
215405149:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
41096 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
314668:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
239128:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
744064:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
423255895:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=142234d1ba15bd10e18be7f09f8f1444
Cycle=DpdR LwSyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw021 No BCLwSyncsRW
Safe=Wse SyncsWR LwSyncsRW DpdR
Time bclwsrw021 25.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw022
"DpdR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: xor 10,4,4
_litmus_P1_2_: lwzx 5,10,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw022 Allowed
Histogram (3 states)
5670 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
8844229:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
631150101:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=935c81207cb119f597f888551d4ae64c
Cycle=DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw022 No BCLwSyncsRW
Safe=Fre SyncsWR DpdR
Time bclwsrw022 19.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw023
"SyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw023 Allowed
Histogram (4 states)
601409056:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
648193:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
444041:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
37498710:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=fbca6700101a4e61c40ebe4e8f0b6024
Cycle=SyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw023 No BCLwSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bclwsrw023 20.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw024
"LwSyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r2) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw024 Allowed
Histogram (4 states)
10440 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
612532051:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
76113 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
27381396:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=07a402855c0d8e1458af975e691f32b1
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw024 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bclwsrw024 20.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw025
"SyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 6,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw025 Allowed
Histogram (3 states)
613167165:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
150420:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
26682415:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=ddd0348fd97714270e542c995072c3a8
Cycle=SyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw025 No BCLwSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bclwsrw025 20.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw026
"DpdR SyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 8,3,3
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: sync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw026 Allowed
Histogram (4 states)
5077756:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
2186986:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
187666584:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
445068674:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=017873a2b19800dddfae60695ee89d93
Cycle=DpdR SyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw026 No BCLwSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bclwsrw026 22.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw027
"LwSyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 6,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw027 Allowed
Histogram (3 states)
33432 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
21961083:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
618005485:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=830ed120688dff2053cc7dba6535b84c
Cycle=LwSyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw027 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bclwsrw027 19.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw028
"DpdR LwSyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 8,3,3
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw028 Allowed
Histogram (4 states)
84623 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
660223:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
183813620:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
455441534:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=727bd8ebc9ec0842952ba5fed4705e15
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw028 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bclwsrw028 21.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw029
"SyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | sync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
lwsync | lwsync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: lwsync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw029 Allowed
Histogram (5 states)
2320990:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
326733811:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
2405181:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
2290004:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
306250014:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=48f1cf92dfad83c716bb2dae18706b3a
Cycle=SyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw029 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw029 23.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw030
"LwSyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
lwsync | lwsync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: lwsync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw030 Allowed
Histogram (5 states)
22789 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
2732234:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
262836497:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
5367263:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
369041217:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=04a596352ad38ea4e25d65100097777b
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw030 No BCLwSyncsRW
Safe=SyncsRR LwSyncsRR DpdR
Time bclwsrw030 23.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw031
"LwSyncsRR DpdR LwSyncsRW Rfe LwSyncsRR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
lwsync | lwsync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: lwsync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw031 Allowed
Histogram (5 states)
77450 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
300205071:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
20151594:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
165052:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
319400833:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=1a177962a3eea2f1418257e4566de980
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe LwSyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw031 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw031 23.21
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: none */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 100000 -r 400
Tue Dec 29 09:36:35 GMT 2009