Mon Dec 28 13:27:50 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 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P3_3_: lwsync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 6,0(9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 5,0(9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bclwsrw000 Allowed
Histogram (101 states)
6 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
3 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
2 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
25724 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
62540 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
104407:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
77508 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
827704:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
152136:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
47339 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1120677:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1213638:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
465248:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
148334:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
24172 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
175987:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
35178 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
82461 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
45364 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
27777 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
144989:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
131300:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1137244:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
102633:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
498292:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
40229 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
954464:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
125288:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2145448:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
1992139:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
121756:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
86861 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
769703:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
50194 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1677050:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
807370:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
112167:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2539276:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
427594:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
115828:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
386830:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
984293:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2417053:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1479528:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
164460:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
755863:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
1612002:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
2205932:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
348610:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
668967:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1458193:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
603215:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
144870:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
2875800:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
1038345:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
2703556:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
2859355:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
3171267:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
6757728:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
804062:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
234463:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2216549:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
912879:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
1706838:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
753024:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1913124:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1787045:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
5736525:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
709177:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
1965342:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
2022074:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
6870297:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
656803:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
3755130:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
1907078:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
162895:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
2239830:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
5276827:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
3279044:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
1874905:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1190627:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
171773:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
6832962:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
3841799:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
1082450:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
9244310:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
1945281:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
8844575:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
4358637:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2643946:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
2603524:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3485852:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
4263607:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
5724673:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
956856:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3483427:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
182368:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
1107522:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 94.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_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 bclwsrw001 Allowed
Histogram (17 states)
1477152:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
15396845:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
8612070:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
14532245:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
20460990:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
2620823:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9048459:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4128861:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
4596949:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2717588:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
5766872:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
1915676:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
36230953:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
22428452:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
23785948:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
15928442:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
10351675:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 50.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 26,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 27,0(11)
_litmus_P2_3_: xor 8,27,27
_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 5,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_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 bclwsrw002 Allowed
Histogram (33 states)
3 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
61488 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
60593 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
471853:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
636111:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
465140:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1646317:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
5604694:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
7079377:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
430633:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
1547393:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
431677:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
2285492:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
2183076:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
754208:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
2031095:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
11271880:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1709598:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
4333629:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1076434:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
3874780:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
21120935:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
34927262:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
24265939:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
11962672:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
2914255:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
10576324:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
16079545:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
15585401:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
562815:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
14049379:>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: 200000000
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 57.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 26,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 27,0(11)
_litmus_P2_3_: xor 8,27,27
_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 5,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_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 bclwsrw003 Allowed
Histogram (34 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
2 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
4 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
309379:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
227946:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
2626 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
2679 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
198624:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
123002:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
70628 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
225709:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
362522:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
79272 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1055948:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
93397 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
6555636:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1766214:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
763615:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
95897 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
4802593:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
10323181:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
2456948:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
7038673:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
15666603:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
28661002:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
2585063:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
21716388:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3642970:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
12958869:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
14576392:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
36155545:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
11781781:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
15700890:>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: 200000000
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 58.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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 (26 states)
47 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
47 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
263 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
344 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
251919:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
246868:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
97886 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
335083:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
13716698:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
10773790:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
3274538:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
4930394:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1812409:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
1457180:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3035318:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
11256248:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
4000233:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
1910412:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
2206040:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
8670489:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
10617768:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
14098086:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
14049019:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
18712123:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
39842433:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
34704365:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
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 55.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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)
217993:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
209393:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
416114:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
13844887:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
6764522:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1175432:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
1053057:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
14536004:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
6196139:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
3001785:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
1861020:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
10438504:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
3394887:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
33628707:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
7953832:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
6385959:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
2173823:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
11522538:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
14338784:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
16432502:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
43756755:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
697363:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 56.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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)
184618:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
313395:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
153255:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
8407997:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
2157577:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
10344077:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
863745:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
1148604:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
7184423:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
2474829:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
1164262:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
3664858:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3567608:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
12546920:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
17756150:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
11273120:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
6026180:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
43133362:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
33435485:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
16832048:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
4945807:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
12421680:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 55.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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)
4 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
4 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1965785:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
2515001:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
2302087:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
6711409:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
13405835:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
3909935:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
12463711:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
11364230:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
2903341:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
12478008:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
1796002:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
34227682:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
11392027:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
43518662:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
21151064:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9561547:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
8333666:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
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 51.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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 (19 states)
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
9469706:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
14030692:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
1232302:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
2009975:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
3630383:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
5072519:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
12708071:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
3866347:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
9339471:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
2625659:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
6720002:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
13211894:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
35740385:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
2353761:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
19241573:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
49946180:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
8801077:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
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 51.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: lwz 5,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_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)
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
18 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
12183420:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
10278172:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
12233431:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
9967038:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
8588091:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
4078307:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
2463651:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
7382677:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
2214941:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
12134323:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
4012180:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
35119159:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
48232656:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
2431977:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
21511468:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
1942052:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
5226437:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 51.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 26,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 27,0(11)
_litmus_P0_3_: xor 8,27,27
_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)
274307:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
770056:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
3847497:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
617685:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4414480:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
21315359:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
738212:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
7233333:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
3135173:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
2479269:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3617375:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
730720:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
9563638:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
5382023:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
10917466:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9400974:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
23532948:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
28430240:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
13493295:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
35453177:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
10326205:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4326568:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
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 52.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 26,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 27,0(11)
_litmus_P0_3_: xor 8,27,27
_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)
40072 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
743181:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
79388 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
81453 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
688175:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3281963:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
109062:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
14498966:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
11253516:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3288339:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4662739:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6983139:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
13032118:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6251378:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
25059858:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
20867834:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4449191:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
3526565:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
31951778:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9560279:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
11215039:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
28375967:>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: 200000000
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 53.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 31,0(9)
_litmus_P2_1_: xor 10,31,31
_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 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_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 bclwsrw014 Allowed
Histogram (21 states)
316011:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
69927 :>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
57119 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
1528756:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
25744487:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
161808:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
16736897:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
3523423:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
3962037:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
2696173:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
7318527:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
7510669:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
7696874:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
18628846:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
33080299:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
5257418:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
9728402:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
6384039:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
5785713:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
31623218:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
12189357:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 52.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_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_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_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_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,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 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,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 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P1_1_: xor 8,30,30
_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 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P1_1_: xor 8,30,30
_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 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_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 27,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)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_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 27,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)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_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 27,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)
Failure: malloc
$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 (16 < N ? 1 : 16 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 16 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 1000000 -r 40
Mon Dec 28 13:40:17 GMT 2009