Mon Dec 28 14:46:29 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw000
"DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW 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) ;
sync | xor r3,r1,r1 | sync | xor r3,r1,r1 ;
li r3,2 | lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
stw r3,0(r2) | sync | stw r3,0(r2) | sync ;
| 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P3_3_: sync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_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_: lwz 5,0(9)
_litmus_P0_1_: sync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bcssrw000 Allowed
Histogram (101 states)
1 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
2 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
4 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
368332:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
309562:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
347466:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
205388:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
583878:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
410077:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
392770:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
143322:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
867710:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
255028:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
229932:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
1992525:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
2270443:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
1436763:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
348875:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
178854:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
1822100:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
463039:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
748326:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
648504:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
413098:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
224508:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
499989:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
471568:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
4321172:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
319447:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
682199:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
1256860:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
243549:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
6543827:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
1120002:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
581214:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
6582978:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
403830:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
267051:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
14562503:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
612249:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
1018338:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
6296600:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3121176:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
220155:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1288352:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
2272882:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
168550:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
13432457:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
3140887:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
15743863:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1002934:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
237122:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
581449:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
211676:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
3249349:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
280096:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
382210:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
357839:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
3389658:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
290498:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
4015334:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
7310944:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
2133167:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
7159325:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
470022:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
2421505:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
6636429:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
268845:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
3744237:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
11596411:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
10268858:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
9110216:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2713907:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
7837139:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2506106:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
14157164:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
1962258:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
4147207:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
483526:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
8719135:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
6782935:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
3093634:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1454465:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
7384498:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3074333:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
3977820:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
438202:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
5062892:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
5097100:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
18178701:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
794646:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
4774795:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
6948455:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
13258270:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
6863248:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
3942202:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4002978:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
7394052:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
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=b7e6e6df4355fb418bf475952119efba
Cycle=DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw000 No BCSyncsRW
Safe=DpdR
Time bcssrw000 114.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw001
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW 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 | sync | xor r3,r1,r1 ;
lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
sync | stw r3,0(r2) | sync ;
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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw001 Allowed
Histogram (18 states)
2 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3489490:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
36235933:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
9442960:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
4662263:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
35689512:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
12896582:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
3773681:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
43021094:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
9641307:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
14025151:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
7106426:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
66764603:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
36661404:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
17980252:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
19470590:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
56435975:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
22702775:>0:r1=0; 0:r4=0; 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:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=0b5e63c8ef234eb2e941f5c51f0aef20
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw001 No BCSyncsRW
Safe=DpdR
Time bcssrw001 66.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw002
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW 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 | sync | sync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | 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 25,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw002 Allowed
Histogram (30 states)
462914:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
448678:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
2096527:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
1823843:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
1137435:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1565546:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
1605333:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
1922815:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2716046:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
5297978:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
16224447:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
4127206:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
35379588:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
1474650:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
11639675:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
30032695:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
47697561:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
13853904:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
1880190:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
10931413:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
9767137:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
9851484:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
3138709:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
5815234:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
39706141:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3605450:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
30460924:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
56545768:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
33134296:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
15656413:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 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=11796ca5759756e415169a54d5d677e2
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw002 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw002 73.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw003
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW 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 | sync | lwsync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | 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 25,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw003 Allowed
Histogram (31 states)
3 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
22209 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
53567 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
513306:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
254012:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
1170916:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
1085801:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
954888:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
134020:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
3567392:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
9702559:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
4616870:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
3861617:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
590342:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
2338330:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3327915:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
18306019:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
7622881:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1955858:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
32188487:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
56871639:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
697977:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
16196192:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
36117397:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
41295023:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
13182478:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
58479175:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
40272890:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
4578027:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
27956781:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
12085429:>0:r1=1; 0:r4=0; 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=f0d60999a697d3eb825e725dab825965
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw003 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw003 72.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw004
"DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw004 Allowed
Histogram (24 states)
3 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
7 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
1558845:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1027336:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
664040:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
28993060:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
5372769:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
718838:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3405371:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
20477521:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
13307961:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
9102283:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
1665999:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
53532882:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
6440658:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
9824520:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
30230700:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
3932387:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
12661286:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
15353840:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
100046840:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
31625082:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
23983442:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
26074330:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
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=2b45cfbf06c32c061b1ef2291b80e3a8
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw004 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw004 69.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw005
"SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw005 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
645543:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
756692:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
589072:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
557281:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
1521360:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
11523104:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
2761988:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
24963136:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
27382998:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
15255067:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
6640955:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
5817624:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
34682949:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
13928751:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
23689859:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
24622795:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
4130398:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
16980043:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
22582981:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
98996121:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
5198971:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
56772311:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
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=921da9ec68c9cae42224f4aee8da9e15
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw005 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw005 69.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw006
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw006 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
687779:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
844904:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
1392064:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1864429:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1877399:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
3211966:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
4669700:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
6484942:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
13100661:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
5254026:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
25336653:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
25029887:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
32151791:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
25995425:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
22563926:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
54163123:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
22263867:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
12139983:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
15286991:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
17474826:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
103483969:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
4721688:>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=ec356be30e18f54ebeedc96f10f9b03d
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw006 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw006 70.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw007
"DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw007 Allowed
Histogram (19 states)
10 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
4859835:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
3804868:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
10339539:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
13245924:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
6221696:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
6339122:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
22117238:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
32243101:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
18162392:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
15530057:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
25114301:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
9226131:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
26029230:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
101952970:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
32297745:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
51567541:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
20948298:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
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=befe5b0646d37c624367af2f5d68102e
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw007 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw007 66.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw008
"SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw008 Allowed
Histogram (18 states)
5 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
27914000:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
5677053:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
24424210:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
4141606:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
7545636:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
5559642:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
9563640:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
4961471:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
26718043:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
32106652:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
19047166:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
16088454:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
21456290:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
105376801:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
13403685:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
24506532:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
51509114:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; 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=a20320b515d5d6be92359c592ff3a749
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw008 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw008 68.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw009
"LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW 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) | sync | 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 | | ;
sync | | ;
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 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw009 Allowed
Histogram (19 states)
5 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
16 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
23016744:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
27090126:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
23492147:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
15761013:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
19100863:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
5063381:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
6127898:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
8254035:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
50277105:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
9387896:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
13061150:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
3565174:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
21689905:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
107003816:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
5440089:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
28154071:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
33514566:>0:r3=1; 0:r5=0; 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=b007f90666b53b8e1b409ebed80da9b2
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw009 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw009 67.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw010
"DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW 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 | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw010 Allowed
Histogram (22 states)
4624260:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3015673:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
7373478:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
5514475:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
1193874:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
13388266:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
9028209:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6196306:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
40455242:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
5374681:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
39345762:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4248272:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4194212:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
22477683:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
23854344:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
16665245:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
14673707:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
2195829:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
56460540:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
64671461:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
41314667:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
13733814:>0:r1=0; 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=2770695d9c722f87a04175621ac51ca6
Cycle=DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw010 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw010 67.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw011
"DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW 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 | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw011 Allowed
Histogram (22 states)
787443:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1826529:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4239262:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
42230148:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
8033074:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
13203047:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
24951649:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
42664638:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
19268430:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3767324:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
5016299:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
29190143:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
1154800:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
617315:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
1298544:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
6571723:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5733318:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
56440403:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
43771234:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
16668436:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
63572427:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
8993814:>0:r1=1; 0:r3=1; 0:r5=0; 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=ae75e3d1140839ad4046415fb4f32715
Cycle=DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw011 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw011 66.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw012
"DpdR SyncsRW Rfe DpdR SyncsRW 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 ;
sync | sync ;
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_: sync
_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_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw012 Allowed
Histogram (3 states)
174919592:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
194759759:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0;
270320649:>0:r1=0; 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=e494be0d2836eabb8ed392ae5713400a
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw012 No BCSyncsRW
Safe=DpdR
Time bcssrw012 75.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw013
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW 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 ;
sync | sync | sync ;
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_: sync
_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_: sync
_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_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw013 Allowed
Histogram (7 states)
3420853:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
4942569:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
3325699:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
108740278:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
84206033:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
95971328:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
99393240:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 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=873592e9aeb4eb41aabdf201c7c3fd2d
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw013 No BCSyncsRW
Safe=DpdR
Time bcssrw013 77.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw014
"DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW 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 ;
sync | sync | sync ;
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 30,0(9)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 11,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,2
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: xor 10,27,27
_litmus_P1_2_: lwzx 28,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw014 Allowed
Histogram (22 states)
1 :>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
550723:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
1326114:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
9927437:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
408904:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
4371194:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
22691822:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
16742370:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
17935491:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
33002898:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
35072707:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
7232028:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
13337890:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
68627052:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
3465375:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
9695196:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
39339325:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
3939248:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
14903450:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
57481388:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
117081:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
39832306:>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: 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=7bfa463f7adb7b5e7778fa7badd28f31
Cycle=DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw014 No BCSyncsRW
Safe=DpsR DpdR
Time bcssrw014 65.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw015
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW 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) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| 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_: sync
_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_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw015 Allowed
Histogram (4 states)
130915208:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
182714370:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
70776788:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
255593634:>0:r1=0; 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=15f52564e04daa74ee8b809a62b31ce5
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw015 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw015 72.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw016
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW 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) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| 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_: sync
_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_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw016 Allowed
Histogram (4 states)
24069381:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
170488187:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
254298521:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
191143911:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 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=da74259e4b84d84fe8b12e45af381e8e
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw016 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw016 74.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw017
"DpdW Wse SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw017 Allowed
Histogram (4 states)
13976129:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
193585789:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
297368629:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
135069453:>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=97b40d67b76129b3ab3e1a6a5f6305eb
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw017 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw017 64.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw018
"SyncdRW Wse SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw018 Allowed
Histogram (4 states)
12406021:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
266590506:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
275718642:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
85284831:>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=059b61899a92329ffeaf348803309697
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw018 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw018 63.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw019
"DpdR SyncsRW Wse SyncsWR DpdR SyncsRW 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) ;
sync | ;
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 28,0(11)
_litmus_P1_1_: xor 10,28,28
_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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw019 Allowed
Histogram (6 states)
10153571:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
2626982:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
8365241:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
127147627:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
191240964:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
300465615:>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=ef298b82541a3b112e43ae882acb50a5
Cycle=DpdR SyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw019 No BCSyncsRW
Safe=Wse SyncsWR SyncsRW DpdR
Time bcssrw019 66.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw020
"LwSyncdRW Wse SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: lwsync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw020 Allowed
Histogram (4 states)
7417583:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
80722974:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
266116744:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
285742699:>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=7f2323c0dd7502796856c97da172b168
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw020 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw020 63.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw021
"DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW 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) ;
sync | ;
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 28,0(11)
_litmus_P1_1_: xor 10,28,28
_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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw021 Allowed
Histogram (6 states)
686997:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
3758689:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
4926516:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
122274147:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
195279771:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
313073880:>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=3ac226fd1be7f310c6194b6c73f3c232
Cycle=DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw021 No BCSyncsRW
Safe=Wse SyncsWR LwSyncsRW DpdR
Time bcssrw021 67.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw022
"DpdR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw022 Allowed
Histogram (3 states)
141412539:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
178601109:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
319986352:>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=7ac3fafaae301cc73390972bbdd5c0f4
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw022 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw022 72.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw023
"SyncsRR DpdR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw023 Allowed
Histogram (4 states)
76517093:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
130172848:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
124209446:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
309100613:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
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=c2c9c0359658b64e4185d23d932ca70a
Cycle=SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw023 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw023 74.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw024
"LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw024 Allowed
Histogram (4 states)
20976582:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
130358341:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
319261359:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
169403718:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 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=dcde740d5eace2726b3b99bfd0448c43
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw024 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw024 75.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw025
"SyncdRR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw025 Allowed
Histogram (3 states)
133060547:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
310856364:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
196083089:>0:r3=1; 0:r5=0; 1:r1=0; 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=8047871ef7343012976d8a83d92f5d9f
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw025 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw025 75.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw026
"DpdR SyncsRR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw026 Allowed
Histogram (4 states)
12154172:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
122562487:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
307105933:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
198177408:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
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=e601791e1656e598fa3a9bacd4c2c5b2
Cycle=DpdR SyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw026 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw026 76.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw027
"LwSyncdRR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw027 Allowed
Histogram (3 states)
189870740:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
319107777:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
131021483:>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=a9989a08ab5b3cfd8006a16e6ef9efd7
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw027 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw027 74.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw028
"DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW 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 | ;
sync | ;
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_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw028 Allowed
Histogram (4 states)
383116:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
197563303:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
123378326:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
318675255:>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=f96ce8a4017924c7511ae42d30af7292
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw028 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw028 76.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw029
"SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW 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 ;
sync | sync ;
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_: sync
_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_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw029 Allowed
Histogram (5 states)
79194866:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
85853668:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
247280220:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
112690949:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
114980297:>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=69e45967a3fe794a66d57ca3e640a326
Cycle=SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw029 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw029 73.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw030
"LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW 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 ;
sync | sync ;
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_: sync
_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_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw030 Allowed
Histogram (5 states)
130036893:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
19349244:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
74787348:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
245848674:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
169977841:>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=ce33b1e1ca4525573eb6199b87f1a3d7
Cycle=LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw030 No BCSyncsRW
Safe=SyncsRR LwSyncsRR DpdR
Time bcssrw030 73.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw031
"LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW 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 ;
sync | sync ;
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_: sync
_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_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw031 Allowed
Histogram (5 states)
172204964:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
27439652:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
179899272:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
24339277:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
236116835:>0:r1=0; 0:r3=0; 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=ae803005916745f384198d670ee29f6c
Cycle=LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe
Relax bcssrw031 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw031 76.24
$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: user */
/* 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=
Mon Dec 28 15:25:04 GMT 2009