Thu Dec 31 15:24:13 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P3_3_: lwsync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: lwsync
_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_: 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 (109 states)
2 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
2 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
15 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
13 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2 :>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=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
2 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
3 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
59 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
82 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
165 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
364861:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
451330:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
360886:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
677254:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
494103:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
518497:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
651942:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
465068:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
497274:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1347592:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
831298:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
611413:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
451233:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
655169:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
4996007:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
777892:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
7147602:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
352023:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
4750125:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
684463:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
3843950:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
5271746:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
401032:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
812185:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1511745:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
566292:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
318572:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
5769173:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4909123:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
11772859:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1183204:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
2557938:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
5922295:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
745758:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
34928547:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
4647786:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
4125156:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
6711814:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
5406232:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
2513036:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
5879471:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
1373422:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
1485769:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
4937274:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
6128755:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
376910:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
8036526:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
404491:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
12927142:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
11108879:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
2580976:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
5214188:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
14331053:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
9852267:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
13613261:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3569532:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2791608:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
2652989:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
1250643:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
645763:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
447799:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
1536513:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1230119:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
5673667:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
10131484:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1106053:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
1369957:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
13739632:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
11370664:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
24879505:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
2268872:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
12322875:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3292047:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
14263624:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
10376540:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
16603960:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
11678479:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
386154:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
6050747:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
27439730:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
17347254:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
32411897:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
1439628:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
721415:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
2287657:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
12825585:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
30395117:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
14232236:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
3106030:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
38483990:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
8357530:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
24911195:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
8018128:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
27652086:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1476088:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 221.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_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_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw001 Allowed
Histogram (19 states)
6 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
12 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
13216834:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
16918400:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
5211405:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
46578457:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
17196744:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
91933078:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
9601870:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
84804512:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
18552671:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
24982047:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
26844901:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
55864573:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
38286197:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
114589627:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
75374433:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
137746875:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
22297358:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 117.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_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_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw002 Allowed
Histogram (33 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
5 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
2 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
696456:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
2758233:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
16833750:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
9767111:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
9373546:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
28764996:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
17695459:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
21389395:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
4004990:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
90278057:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
104075159:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
7757355:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
10083162:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3088387:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
616815:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
3974626:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
39922929:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3669207:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2296460:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
4780919:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
56568254:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
15710187:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
24796077:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
14870694:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
10485867:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
59670320:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
61580946:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
113558702:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
57020983:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3910950:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 130.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_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_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw003 Allowed
Histogram (33 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
11 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
27110 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
1335388:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
201100:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
3552113:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
4727885:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
1326917:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2057011:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1691736:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
2932991:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
12524365:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
17839337:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
10430558:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
3650128:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
92880982:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
883889:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
28953476:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
54814057:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
70870204:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
17679565:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
66069233:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
5671525:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
24255881:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
117127357:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
64119348:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
6049485:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
39210200:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
119833872:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
12525448:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
4979909:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
11778916:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 135.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: 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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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)
7 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
22 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
6368 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
6325 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
2555011:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
837080:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
1025649:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
32038909:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
24108755:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
3344855:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
1779045:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
2037815:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
70128243:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
31677595:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
29355471:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
16504343:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
20450659:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
195070847:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
20285987:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
9467191:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
94143774:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
59914666:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
38088340:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
80251860:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
7727778:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
59193405:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 131.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw005 Allowed
Histogram (24 states)
10 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
4 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
2497277:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
2958222:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
1730233:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
1752218:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1448302:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
9200949:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
13718446:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
64061269:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
45171096:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
20590813:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
26019030:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
42162110:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
8860908:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
6586960:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
30574956:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
190461389:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
59286835:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
63536704:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
35713298:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
111403096:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
8414652:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
53851223:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 131.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw006 Allowed
Histogram (23 states)
7 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
3477849:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
2293771:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
1759074:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
8805693:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
1344711:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
25819144:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
9725309:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
26076647:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
6969664:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
23381745:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
40124997:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
56516070:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
61769086:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
7150005:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
36966316:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
12907446:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
2709392:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
48145140:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
107752912:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
55156225:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
197757992:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
63390805:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 127.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: 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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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)
3956 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
2354 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
24170168:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
3883681:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
96388179:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
66649600:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
58925341:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
29443550:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
9427546:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
37577462:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
15359416:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
20526533:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
38389284:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
58580006:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
20392575:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
11761062:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
29123493:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
83850423:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
195545371:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 123.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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)
32 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
6 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
7497123:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
10932090:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
37217473:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
64783220:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
52906171:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
30160954:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
21741002:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
7870804:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
21543403:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
58442904:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
47106161:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
19025743:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
100057316:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
38005153:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
11715718:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
73155106:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
197839621:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 122.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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)
2100 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
1622 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
13148114:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
38361949:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
20752391:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
75730646:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
8358360:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
37660256:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
29195385:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
8720721:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
65686517:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
6306207:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
21583376:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
42773619:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
202366607:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
50198281:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
91927263:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
62339542:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
24887044:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 123.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_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_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw010 Allowed
Histogram (25 states)
3 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
16384571:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6279894:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
5493144:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
41070915:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
11486879:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9040268:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
8173207:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
11467468:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
69757878:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
13098074:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
78010718:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
17531011:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6898253:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
22454997:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
21625650:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
23781851:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
33732267:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
98623961:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
133792244:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
113682727:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
50937489:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
6676525:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 122.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: lwsync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_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_: lwsync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bclwsrw011 Allowed
Histogram (25 states)
1 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
3 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3182962:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
10051097:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
5587219:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
2813130:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
20875980:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
15065657:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
3508070:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
82492788:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
43047348:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
13687994:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
12009109:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
27796515:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
65380016:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
7805942:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
17953353:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
38989156:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
11566159:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
96902552:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
119030994:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
65165545:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
2653969:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
134434437:>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: 800000000
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 124.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw012 Allowed
Histogram (3 states)
497798074:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0;
410952480:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0;
371249446:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=138606a77ccb32f9d127a952601f26cc
Cycle=DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw012 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw012 96.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw013 Allowed
Histogram (7 states)
186258402:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
200190751:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
204364692:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
8469573:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
12764866:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
177627568:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
10324148:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 800000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=c2348c97f33f2ba898984873da5d4807
Cycle=DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw013 No BCLwSyncsRW
Safe=DpdR
Time bclwsrw013 123.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_1_: xor 10,30,30
_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 27,0(11)
_litmus_P1_1_: xor 10,27,27
_litmus_P1_2_: lwzx 28,10,9
_litmus_P1_3_: lwsync
_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_: lwsync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bclwsrw014 Allowed
Histogram (23 states)
1 :>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
3 :>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
754382:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
578220:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
3367641:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
17282076:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
19349617:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
22269378:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
17322501:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
5279058:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
3639612:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
37650865:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
18857795:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
11609397:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
77216345:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
117904393:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
88216139:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
77588910:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
141138753:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
9713987:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
54722859:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
36112532:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
39425536:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 121.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw015 Allowed
Histogram (4 states)
122653939:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
402418807:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
335337186:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
419590068:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=7fd3dfd255f25b83fe014eed6c45b685
Cycle=SyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw015 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw015 95.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw016 Allowed
Histogram (4 states)
56344198:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
424601456:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
379829706:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
419224640:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=898c0b81592367ec9511da918b08041e
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe DpdR LwSyncsRW Rfe
Relax bclwsrw016 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw016 96.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw017 Allowed
Histogram (4 states)
31371343:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
276389069:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
607170442:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
365069146:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=20086dd564a511b714a1da610330fdea
Cycle=DpdW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw017 No BCLwSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bclwsrw017 96.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwsrw018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsrw018
"SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
lwsync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 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_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw018 Allowed
Histogram (4 states)
27168340:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
432778316:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
535571704:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
284481640:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=f68fe5834d4a291ee56368caf658541c
Cycle=SyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw018 No BCLwSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bclwsrw018 96.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw019 Allowed
Histogram (6 states)
20536186:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
5120806:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
19034120:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
294156600:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
597987150:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
343165138:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=b29e6d271ad79fd47834aeea490fe672
Cycle=DpdR SyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw019 No BCLwSyncsRW
Safe=Wse SyncsWR SyncsRW DpdR
Time bclwsrw019 103.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw020 Allowed
Histogram (4 states)
28752853:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
275262859:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
409824240:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
566160048:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=2af7591a084823d06f5daf38cddf2810
Cycle=LwSyncdRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw020 No BCLwSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bclwsrw020 94.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: lwsync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bclwsrw021 Allowed
Histogram (6 states)
4944466:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
9838117:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
10223093:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
341902232:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
621756706:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
291335386:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=142234d1ba15bd10e18be7f09f8f1444
Cycle=DpdR LwSyncsRW Wse SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw021 No BCLwSyncsRW
Safe=Wse SyncsWR LwSyncsRW DpdR
Time bclwsrw021 103.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw022 Allowed
Histogram (3 states)
214201566:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
425910581:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
639887853:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=935c81207cb119f597f888551d4ae64c
Cycle=DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw022 No BCLwSyncsRW
Safe=Fre SyncsWR DpdR
Time bclwsrw022 95.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw023 Allowed
Histogram (4 states)
163926107:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
356445697:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
146339471:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
613288725:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=fbca6700101a4e61c40ebe4e8f0b6024
Cycle=SyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw023 No BCLwSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bclwsrw023 98.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw024 Allowed
Histogram (4 states)
232900014:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
56978281:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
634283030:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
355838675:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=07a402855c0d8e1458af975e691f32b1
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw024 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bclwsrw024 100.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw025 Allowed
Histogram (3 states)
320853603:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
618769849:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
340376548:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=ddd0348fd97714270e542c995072c3a8
Cycle=SyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw025 No BCLwSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bclwsrw025 95.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw026 Allowed
Histogram (4 states)
22628520:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
300601341:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
341121652:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
615648487:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=017873a2b19800dddfae60695ee89d93
Cycle=DpdR SyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw026 No BCLwSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bclwsrw026 101.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw027 Allowed
Histogram (3 states)
310060627:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
332288996:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
637650377:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=830ed120688dff2053cc7dba6535b84c
Cycle=LwSyncdRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw027 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bclwsrw027 98.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw028 Allowed
Histogram (4 states)
1901168:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
310499402:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
331892649:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
635706781:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=727bd8ebc9ec0842952ba5fed4705e15
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR LwSyncsRW Rfe
Relax bclwsrw028 No BCLwSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bclwsrw028 100.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw029 Allowed
Histogram (5 states)
236527312:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
174594062:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
169396088:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
335159843:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
364322695:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=48f1cf92dfad83c716bb2dae18706b3a
Cycle=SyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw029 No BCLwSyncsRW
Safe=SyncsRR DpdR
Time bclwsrw029 100.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw030 Allowed
Histogram (5 states)
59369430:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
336097580:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
432411937:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
331540342:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
120580711:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=04a596352ad38ea4e25d65100097777b
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe SyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw030 No BCLwSyncsRW
Safe=SyncsRR LwSyncsRR DpdR
Time bclwsrw030 102.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bclwsrw031 Allowed
Histogram (5 states)
41400553:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
42083267:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
375728575:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
390542290:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
430245315:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 1280000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=1a177962a3eea2f1418257e4566de980
Cycle=LwSyncsRR DpdR LwSyncsRW Rfe LwSyncsRR DpdR LwSyncsRW Rfe
Relax bclwsrw031 No BCLwSyncsRW
Safe=LwSyncsRR DpdR
Time bclwsrw031 103.87
$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=-s 4000
Thu Dec 31 16:24:51 GMT 2009