Tue Dec 22 18:59:53 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww000
"DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww000 Allowed
Histogram (3 states)
28775406:>1:r1=0; x=1;
293888938:>1:r1=1; x=1;
317335656:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=c704ed5593f60a49b6fe2873fbc99877
Cycle=DpdW Wse LwSyncdWW Rfe
Relax bclwdww000 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww000 82.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww001
"DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 31,3,3
_litmus_P3_2_: li 10,1
_litmus_P3_3_: stwx 10,31,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww001 Allowed
Histogram (16 states)
11 :>1:r1=1; 3:r1=1; x=2; z=2;
1250096:>1:r1=1; 3:r1=1; x=1; z=2;
1603659:>1:r1=0; 3:r1=0; x=1; z=1;
19591749:>1:r1=1; 3:r1=0; x=1; z=2;
1543517:>1:r1=1; 3:r1=1; x=2; z=1;
1623420:>1:r1=0; 3:r1=1; x=2; z=2;
2056877:>1:r1=1; 3:r1=0; x=2; z=2;
18059692:>1:r1=1; 3:r1=0; x=2; z=1;
32042162:>1:r1=0; 3:r1=1; x=1; z=1;
36632946:>1:r1=0; 3:r1=0; x=1; z=2;
18495252:>1:r1=0; 3:r1=1; x=2; z=1;
63919642:>1:r1=0; 3:r1=0; x=2; z=2;
34533691:>1:r1=1; 3:r1=0; x=1; z=1;
37512992:>1:r1=0; 3:r1=0; x=2; z=1;
35270064:>1:r1=1; 3:r1=1; x=1; z=1;
15864230:>1:r1=0; 3:r1=1; x=1; z=2;
Ok
Witnesses
Positive: 11, Negative: 319999989
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is validated
Hash=d6ca5faa9797f1b1addda6b4fc107253
Cycle=DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww001 Ok BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww001 90.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww002
"LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | li r3,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww002 Allowed
Histogram (16 states)
8 :>1:r1=1; 3:r1=1; x=2; z=2;
938973:>1:r1=0; 3:r1=1; x=2; z=2;
3251421:>1:r1=0; 3:r1=0; x=1; z=1;
987676:>1:r1=1; 3:r1=1; x=2; z=1;
1640231:>1:r1=1; 3:r1=0; x=2; z=2;
1301743:>1:r1=1; 3:r1=1; x=1; z=2;
32473355:>1:r1=1; 3:r1=1; x=1; z=1;
14231064:>1:r1=0; 3:r1=1; x=1; z=2;
17109560:>1:r1=1; 3:r1=0; x=2; z=1;
39365082:>1:r1=1; 3:r1=0; x=1; z=1;
31674233:>1:r1=0; 3:r1=1; x=1; z=1;
40097201:>1:r1=0; 3:r1=0; x=1; z=2;
14138600:>1:r1=0; 3:r1=1; x=2; z=1;
39771624:>1:r1=0; 3:r1=0; x=2; z=1;
20830251:>1:r1=1; 3:r1=0; x=1; z=2;
62188978:>1:r1=0; 3:r1=0; x=2; z=2;
Ok
Witnesses
Positive: 8, Negative: 319999992
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is validated
Hash=f222837c1b9c320fc4731d82df04c0c8
Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww002 Ok BCLwSyncdWW
Safe=Wse LwSyncdRW DpdW
Time bclwdww002 91.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww003
"DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww003 Allowed
Histogram (16 states)
11 :>1:r1=1; 3:r1=1; 3:r4=0; z=2;
1177578:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
34587785:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1445583:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1570654:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1598388:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
34774923:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
15726604:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
31194567:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
18500902:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
21939789:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
66757405:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
32831958:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
37429525:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
17921303:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
2543025:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
Ok
Witnesses
Positive: 11, Negative: 319999989
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated
Hash=13e9eff5346eb465cffd68e7d2363168
Cycle=DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww003 Ok BCLwSyncdWW
Safe=Fre Wse DpdW DpdR
Time bclwdww003 93.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww004
"DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww004 Allowed
Histogram (45 states)
5 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=2;
23 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
4 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=2;
8 :>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=2;
23642 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
6207 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
6357 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
10123 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
19150 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
13337 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
94767 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
36440 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
51147 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
8424 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
50383 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
24485 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
81518 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
33982 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
13943 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
79366 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
71248 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
705027:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3417821:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
134389:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
606284:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1417424:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
706130:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
5432223:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
4558604:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
2488487:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
1949052:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
9973469:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
51766056:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
22175199:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
12080255:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
29770416:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
14097634:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
28052558:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
7490826:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
25741081:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
30708645:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
20916975:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
29617091:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1487408:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
14082387:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
Ok
Witnesses
Positive: 4, Negative: 319999996
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is validated
Hash=819caebc895b4fb2e9c9cb702b8483e8
Cycle=DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww004 Ok BCLwSyncdWW
Safe=Fre Wse DpsR DpdW
Time bclwdww004 93.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww005
"LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww005 Allowed
Histogram (16 states)
13 :>1:r1=1; 3:r1=1; 3:r3=0; z=2;
1413611:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1558078:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
2160764:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
1755514:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
36192417:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
38458262:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
30635568:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
33761115:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
19394182:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
34710352:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
16284764:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
18899146:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
65775750:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
1538756:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
17461708:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
Ok
Witnesses
Positive: 13, Negative: 319999987
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=1b7673dab67cdeed3a93a9f78642c123
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww005 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdRR DpdW
Time bclwdww005 93.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww006
"LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | lwz r3,0(r2) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww006 Allowed
Histogram (46 states)
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=2;
6 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=2;
7 :>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=2;
40 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=2;
2386 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
91467 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
98178 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
218994:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
38336 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
74071 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
168273:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
149704:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
175319:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
2576219:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
216315:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
890169:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
590307:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
142400:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
691715:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
261491:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
2296359:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
1274363:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
1402087:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
659944:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
13501153:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
27464954:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
9800739:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
3744709:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
1776670:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
27384633:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
3802560:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
3225070:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
743713:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
50422630:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
19563395:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
27419280:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
1110830:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
14075616:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
4819683:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
2400157:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
21018220:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
3159020:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
12049829:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
25830855:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
28220185:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
6447948:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
Ok
Witnesses
Positive: 6, Negative: 319999994
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is validated
Hash=355c23adb39c4f8a03f27206e6d5ad02
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww006 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncsRR DpdW
Time bclwdww006 93.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww007
"DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | li r4,1 ;
li r3,1 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww007 Allowed
Histogram (8 states)
48 :>2:r1=1; x=2; y=2;
38025673:>2:r1=0; x=2; y=2;
30832063:>2:r1=1; x=2; y=1;
3520720:>2:r1=0; x=1; y=1;
24099434:>2:r1=1; x=1; y=2;
105212910:>2:r1=0; x=1; y=2;
108041405:>2:r1=0; x=2; y=1;
90267747:>2:r1=1; x=1; y=1;
Ok
Witnesses
Positive: 48, Negative: 399999952
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is validated
Hash=c71f30898deb2fe2dc12be48ca126717
Cycle=DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww007 Ok BCLwSyncdWW
Safe=Wse LwSyncdWW DpdW
Time bclwdww007 74.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww008
"LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | li r3,1 ;
li r3,1 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww008 Allowed
Histogram (7 states)
7193811:>2:r1=0; x=1; y=1;
35315992:>2:r1=0; x=2; y=2;
21771574:>2:r1=1; x=2; y=1;
113231938:>2:r1=0; x=1; y=2;
115142280:>2:r1=0; x=2; y=1;
89348069:>2:r1=1; x=1; y=1;
17996336:>2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=82e869524c51deb209a9e10f0c829a0c
Cycle=LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww008 No BCLwSyncdWW
Safe=Wse LwSyncdWW LwSyncdRW
Time bclwdww008 73.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww009
"DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | lwzx r4,r3,r5 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 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_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww009 Allowed
Histogram (8 states)
158 :>2:r1=1; 2:r4=0; y=2;
16323816:>2:r1=1; 2:r4=1; y=2;
3422081:>2:r1=0; 2:r4=1; y=1;
39431441:>2:r1=0; 2:r4=0; y=2;
28433598:>2:r1=1; 2:r4=0; y=1;
110409266:>2:r1=0; 2:r4=1; y=2;
118889654:>2:r1=0; 2:r4=0; y=1;
83089986:>2:r1=1; 2:r4=1; y=1;
Ok
Witnesses
Positive: 158, Negative: 399999842
Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is validated
Hash=2e3c762333e6fd2b122415c163d1229a
Cycle=DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww009 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpdR
Time bclwdww009 74.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww010
"DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | lwzx r4,r3,r2 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 11,10,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww010 Allowed
Histogram (18 states)
2969 :>2:r1=2; 2:r4=1; x=1; y=1;
1258 :>2:r1=0; 2:r4=1; x=2; y=1;
14188 :>2:r1=0; 2:r4=2; x=1; y=1;
17048 :>2:r1=0; 2:r4=1; x=1; y=1;
80285 :>2:r1=2; 2:r4=1; x=2; y=1;
153360:>2:r1=0; 2:r4=2; x=1; y=2;
58306 :>2:r1=1; 2:r4=2; x=1; y=2;
1153115:>2:r1=2; 2:r4=2; x=1; y=1;
45906 :>2:r1=0; 2:r4=2; x=2; y=1;
61816516:>2:r1=0; 2:r4=0; x=1; y=2;
1439157:>2:r1=0; 2:r4=1; x=1; y=2;
13891173:>2:r1=1; 2:r4=1; x=1; y=1;
45966045:>2:r1=0; 2:r4=0; x=1; y=1;
94871529:>2:r1=2; 2:r4=2; x=2; y=1;
51545506:>2:r1=1; 2:r4=1; x=1; y=2;
41493536:>2:r1=0; 2:r4=0; x=2; y=1;
27665607:>2:r1=1; 2:r4=1; x=2; y=1;
59784496:>2:r1=2; 2:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3b6264a86335c33f3b93e442e8f4ad38
Cycle=DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww010 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpsR
Time bclwdww010 77.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww011
"LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww011 Allowed
Histogram (8 states)
97 :>2:r1=1; 2:r3=0; y=2;
38362106:>2:r1=0; 2:r3=0; y=2;
4605360:>2:r1=0; 2:r3=1; y=1;
16561129:>2:r1=1; 2:r3=1; y=2;
27902430:>2:r1=1; 2:r3=0; y=1;
111363958:>2:r1=0; 2:r3=1; y=2;
116654397:>2:r1=0; 2:r3=0; y=1;
84550523:>2:r1=1; 2:r3=1; y=1;
Ok
Witnesses
Positive: 97, Negative: 399999903
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=cf3c12d91d4069a3e06aed8f569c6ba5
Cycle=LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww011 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdWW LwSyncdRR
Time bclwdww011 78.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww012
"LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 4,0(9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww012 Allowed
Histogram (18 states)
88834 :>2:r1=0; 2:r3=2; x=1; y=1;
196459:>2:r1=0; 2:r3=2; x=2; y=1;
57132 :>2:r1=2; 2:r3=1; x=1; y=1;
128694:>2:r1=0; 2:r3=1; x=1; y=1;
48195 :>2:r1=0; 2:r3=1; x=2; y=1;
12342058:>2:r1=1; 2:r3=1; x=1; y=1;
27516519:>2:r1=1; 2:r3=1; x=2; y=1;
1119588:>2:r1=2; 2:r3=2; x=1; y=1;
3293558:>2:r1=0; 2:r3=2; x=1; y=2;
1204926:>2:r1=2; 2:r3=1; x=2; y=1;
518991:>2:r1=1; 2:r3=2; x=1; y=2;
41791370:>2:r1=0; 2:r3=0; x=2; y=1;
57551678:>2:r1=2; 2:r3=2; x=1; y=2;
44753751:>2:r1=0; 2:r3=0; x=1; y=1;
5610597:>2:r1=0; 2:r3=1; x=1; y=2;
66158305:>2:r1=0; 2:r3=0; x=1; y=2;
43126559:>2:r1=1; 2:r3=1; x=1; y=2;
94492786:>2:r1=2; 2:r3=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=e7d627c7adc87ac2502ce1f2b46f87c5
Cycle=LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww012 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdWW
Time bclwdww012 80.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww013
"LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | li r3,1 ;
li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww013 Allowed
Histogram (3 states)
54165298:>1:r1=0; x=1;
307710156:>1:r1=0; x=2;
278124546:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=4d1c1648955365c08b4c97b22a8d5408
Cycle=LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww013 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww013 77.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww014
"LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | li r3,1 ;
li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww014 Allowed
Histogram (15 states)
837802:>1:r1=1; 3:r1=1; x=2; z=1;
649719:>1:r1=0; 3:r1=1; x=2; z=2;
5562942:>1:r1=0; 3:r1=0; x=1; z=1;
930331:>1:r1=1; 3:r1=0; x=2; z=2;
43263655:>1:r1=0; 3:r1=0; x=1; z=2;
44324427:>1:r1=0; 3:r1=0; x=2; z=1;
37059962:>1:r1=0; 3:r1=1; x=1; z=1;
39450009:>1:r1=1; 3:r1=0; x=1; z=1;
14497090:>1:r1=0; 3:r1=1; x=2; z=1;
15885425:>1:r1=1; 3:r1=0; x=1; z=2;
61015076:>1:r1=0; 3:r1=0; x=2; z=2;
28432116:>1:r1=1; 3:r1=1; x=1; z=1;
14410503:>1:r1=1; 3:r1=0; x=2; z=1;
799827:>1:r1=1; 3:r1=1; x=1; z=2;
12881116:>1:r1=0; 3:r1=1; x=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d40b4d76f7e7419bc76f118bb3639055
Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww014 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww014 91.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww015
"DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww015 Allowed
Histogram (16 states)
8 :>1:r1=1; 3:r1=1; 3:r4=0; z=2;
960834:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
2013831:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1513888:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
2805467:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
14456447:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
17384268:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
40772577:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
31193278:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1072831:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
14211204:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
22485869:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
37245303:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
36731403:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
64981664:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
32171128:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
Ok
Witnesses
Positive: 8, Negative: 319999992
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated
Hash=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 92.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww016
"DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_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 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww016 Allowed
Histogram (42 states)
32 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
7130 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
6221 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
23134 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
12479 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
20220 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
14988 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
37201 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
25913 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
13362 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
72475 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
85311 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
7181 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
5921 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
74621 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
65350 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
30871 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
119262:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
571282:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
4435209:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
51686 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
1275064:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
2221614:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
1233385:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
4410866:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
12236296:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
2645710:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
3681698:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
12004410:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
669501:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
19851441:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
7567038:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
13569514:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
30397249:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
26564275:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
29668171:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1591406:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
13735256:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
49101204:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
30371402:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
22276720:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
29247931:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=cda2e0cac993408d5ce399f8c3bf25da
Cycle=DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww016 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpsR
Time bclwdww016 95.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww017
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww017 Allowed
Histogram (16 states)
7 :>1:r1=1; 3:r1=1; 3:r3=0; z=2;
938726:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1367223:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
4367702:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
43458797:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
35092842:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
29303587:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
14878874:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
14386879:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
36448960:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
19512389:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
64700663:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
1274909:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
839601:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
14357655:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
39071186:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
Ok
Witnesses
Positive: 7, Negative: 319999993
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=bc3782a4ff957f30ebb76bfb73a82170
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww017 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdRW LwSyncdRR
Time bclwdww017 92.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww018
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r2) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_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 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww018 Allowed
Histogram (42 states)
2442 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
50652 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
190689:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
169934:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
112610:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
160837:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
95843 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
228371:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
151299:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
571980:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
2656159:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
944829:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
38483 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
237394:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
3716474:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
1651281:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
4183239:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
657148:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
981898:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
224740:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1922002:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
3239806:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
1069031:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
6488466:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
2329852:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
2478008:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
608947:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
1355520:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
11980222:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
3851963:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
28946261:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
27546907:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
19535018:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
19782786:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
48631177:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
13476904:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
12570408:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
28042677:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
11860661:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
26663469:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
2910408:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
27683205:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=090f9e7edaad20d00811f89adff27ed2
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww018 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdRW
Time bclwdww018 97.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww019
"DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (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 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww019 Allowed
Histogram (3 states)
33354942:>1:r1=0; 1:r4=1;
286494553:>1:r1=1; 1:r4=1;
320150505:>1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=76deedad5ea71bc51dc86d1d5214c15b
Cycle=DpdR Fre LwSyncdWW Rfe
Relax bclwdww019 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww019 80.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww020
"DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww020 Allowed
Histogram (16 states)
29 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0;
613323:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
2287620:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
2292325:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
2153460:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
18499733:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
2147898:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
33681509:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
37397088:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
30278481:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
18523876:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
20804226:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
30474418:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
20717522:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
66418298:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
33710194:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
Ok
Witnesses
Positive: 29, Negative: 319999971
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is validated
Hash=95bd88b4aecb95238880fff470fdbcc8
Cycle=DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww020 Ok BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww020 92.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww021
"DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww021 Allowed
Histogram (45 states)
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
7 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
51 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
32 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
1333 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
7856 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
13409 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
9633 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
6997 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
22359 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
20097 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
8195 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
123081:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
29585 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
14679 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
65684 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
65715 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
46082 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
35845 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
8025 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
25853 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
401855:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
56599 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
265293:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2401351:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
3079476:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
486942:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
7999217:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
25674955:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
1858464:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
49116915:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
23227120:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
13927526:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
2412138:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
27166374:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
14844442:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
10541653:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
4471461:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
26533189:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
26515732:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
5481005:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
3620875:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
19514015:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
21049099:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
28849780:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
Ok
Witnesses
Positive: 6, Negative: 319999994
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is validated
Hash=26c4ea0f855245b74a15911ba593704d
Cycle=DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww021 Ok BCLwSyncdWW
Safe=Fre DpsR DpdR
Time bclwdww021 95.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww022
"LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww022 Allowed
Histogram (16 states)
27 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0;
2134222:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
1566184:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
1497407:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
1326635:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
1664874:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
37380721:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
17921857:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
35059646:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
31681056:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
20784717:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
69102633:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
37643723:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
16637595:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
29899770:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
15698933:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
Ok
Witnesses
Positive: 27, Negative: 319999973
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=18c468c9529c924b0b9eadcf19d0bf8c
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww022 Ok BCLwSyncdWW
Safe=Fre LwSyncdRR DpdR
Time bclwdww022 91.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww023
"LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww023 Allowed
Histogram (47 states)
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
16 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
16 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
101 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
3076 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
48111 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
68852 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
97976 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
55269 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
193434:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
233965:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
242265:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
870280:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
2381335:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
826869:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
185090:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
143605:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
311761:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
220287:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
682555:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
327000:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
3425293:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
8119595:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
3657416:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
2979976:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
2257584:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
3711873:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
26244293:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1188192:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
2317106:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
8959185:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
14643033:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
12594021:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
761030:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
26412865:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
1885206:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
20022099:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
20296850:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
24829663:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
2270102:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
4820801:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
26244490:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
48886227:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
19436514:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
24296499:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
2848221:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
Ok
Witnesses
Positive: 16, Negative: 319999984
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is validated
Hash=cc14d1f72457a494131d0111d5791792
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww023 Ok BCLwSyncdWW
Safe=Fre LwSyncsRR DpdR
Time bclwdww023 93.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww024
"DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r2 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww024 Allowed
Histogram (104 states)
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
6 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
4 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
8 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
15 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
73 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
271 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
26 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
13 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
97 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
37 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
110 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
25 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
58 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
592 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
15 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
381 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
326 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
68 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
893 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
356 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
91 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
32 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
282 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
10371 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
252 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
946 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
754 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
4254 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
28901 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
43418 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
9582 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
3845 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
28261 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
9231 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
11416 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
4064 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
8744 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
15808 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
9031 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
64710 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
36501 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
54294 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
13902 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
4721 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
10954 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
41277 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
9716 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
27568 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
3614 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
127594:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
80029 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
17137 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
199852:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
21229 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
33627 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
2767 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
43073 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
57328 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
130797:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
65513 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
9989 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
71479 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
319734:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
59377 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
95776 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
70520 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
22992 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
125564:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
4000496:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
1088753:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
549110:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
120785:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
3769162:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
490369:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
490294:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
5960550:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
4098933:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
3838460:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
27038983:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
9554758:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
4767464:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
5785872:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
4850396:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
9495007:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
12158250:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
3291616:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
24182490:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1053637:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
29241510:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
6046597:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
24052702:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
21942196:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
174243:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
21400574:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
5827249:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
21395879:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
12162393:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
27009390:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
22147578:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=d9cb89dae7c1c7340715ada64130ec5d
Cycle=DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww024 No BCLwSyncdWW
Safe=Fre DpsR
Time bclwdww024 102.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww025
"LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww025 Allowed
Histogram (45 states)
8 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=2;
9 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=2;
86 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=2;
97 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
9999 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
15817 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
31078 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
11726 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
59473 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
16187 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
9356 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
20295 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
19685 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
47738 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
123593:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
105437:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
109866:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
85014 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
119867:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
165657:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
96309 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
139204:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
1222274:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
3148949:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
1985694:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
4106229:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
628900:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
2958999:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
21361063:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
8227511:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
2460720:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
24839711:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
29168587:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
719238:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
9822273:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
29410495:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
12739246:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
5071546:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
28821083:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
50424043:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
21515932:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
14139333:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
26921638:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
1912705:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
17207330:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
Ok
Witnesses
Positive: 9, Negative: 319999991
Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=9e35ea0c011a355376ee19a400e99599
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww025 Ok BCLwSyncdWW
Safe=Fre LwSyncdRR DpsR
Time bclwdww025 94.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww026
"LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww026 Allowed
Histogram (108 states)
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
2 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
12 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
61 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
50 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
6 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
190 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
57 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
101 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
63 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
126 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1800 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
212 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
11567 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
885 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
373 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
398 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
615 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
621 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
182 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
67 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
20 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
423 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
3795 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
3367 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
1358 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
4109 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
15894 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
408 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
7174 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
6377 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
146 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
2969 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
415 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1099 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
411 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
9891 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
7463 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
50089 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
7165 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
17682 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
3481 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
46876 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3119 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
19781 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
37071 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
270025:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
29202 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
4753 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
57760 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
132153:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
354339:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
114241:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
68607 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
86466 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
247104:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
129697:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
124876:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
68641 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
431867:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
55887 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
32257 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
232845:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
194622:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
12827 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
554649:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
843524:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
2742558:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1141874:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
192543:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
2045406:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
569044:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
3570180:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1181232:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
5985508:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
9151715:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
9556030:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
3845659:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
32579 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
404888:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
2657562:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
170024:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
2777593:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
727453:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
4498209:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
1071470:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
2984920:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
4648943:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
479130:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1105314:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
5382398:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
19915846:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
3016711:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
1676788:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
1330751:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
9823504:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
25319875:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
22910574:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
21726059:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
10370776:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
27692144:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
27656250:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
21929941:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
22172809:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
24643754:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3149042:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
5428626:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1d532d0bb6dcdffd3b5563101102cb60
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww026 No BCLwSyncdWW
Safe=Fre LwSyncsRR DpsR
Time bclwdww026 109.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww027
"LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (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 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww027 Allowed
Histogram (3 states)
41624708:>1:r1=0; 1:r3=1;
278964984:>1:r1=1; 1:r3=1;
319410308:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=9db44a87c6f0512eb7b557fa626432dc
Cycle=LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww027 No BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww027 77.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww028
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww028 Allowed
Histogram (16 states)
10 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0;
1212579:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
3802702:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1232925:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1128956:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
17303067:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
14347298:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
27869342:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1291670:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
18614461:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
40446425:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
33842318:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
70810662:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
33079992:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
39924140:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
15093453:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
Ok
Witnesses
Positive: 10, Negative: 319999990
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=55921b82d0e8bcbda1b708c97c7b56b3
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww028 Ok BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww028 92.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww029
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww029 Allowed
Histogram (46 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
6 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
57 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
3187 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
64535 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
158396:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
258320:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
812762:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
194466:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
726642:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
48270 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
2321289:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
84233 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
237362:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
246842:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
174259:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
177413:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
3277814:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
154420:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
3298579:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
642541:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
2084769:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
3095406:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2599829:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3877743:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
945243:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
6766981:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
4412902:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1384864:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
12040110:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
1222943:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
1855529:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
27302733:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
20597119:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
16847142:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1343488:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2656609:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
13376479:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
24850120:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
10416246:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
26691523:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
19007951:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
49824070:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
26472782:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
27446020:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
Ok
Witnesses
Positive: 5, Negative: 319999995
Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is validated
Hash=ed3e4f2d7ea7b66a761b0ef9aadf9b30
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww029 Ok BCLwSyncdWW
Safe=Fre LwSyncsRR LwSyncdRR
Time bclwdww029 94.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww030
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r2) | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bclwdww030 Allowed
Histogram (108 states)
799 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
388 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1231 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
2265 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
11666 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
3602 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
299 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
8102 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1001 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
322 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
15451 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
3350 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
239 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
6556 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
58010 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
15573 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
6334 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
3758 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
2844 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1423 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
142830:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
6151 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1166 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
10829 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
66697 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
33864 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
4328 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
288973:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
96284 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
65962 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
107980:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
1456 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
196436:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
24722 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
107159:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
39140 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
29687 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
35284 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
105155:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
132125:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
629818:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
78102 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
23016 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
186317:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
34892 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
142942:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
182770:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
700837:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
858864:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
1093601:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
697768:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
73102 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
270207:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
2006353:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
642574:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
292594:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
752160:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
57201 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
50370 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
173409:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
194900:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1365147:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
81588 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
129093:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2664870:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1077498:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
357840:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
3483 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
701467:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
262642:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
767440:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1238328:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
685451:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1342213:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
8686957:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
2833618:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1664058:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
4770378:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
1088516:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2484451:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
251336:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
2640661:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
16115 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
5276434:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
2310718:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1023492:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
3770165:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
4735533:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
3039400:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
9140880:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
3718808:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
3036154:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
1121721:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
5339670:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
19754278:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
2094083:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
8781530:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
3571023:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2570398:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
22014091:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
22700101:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
21876563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
19633439:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
8828740:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
21630857:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
24982041:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
25070223:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
28085270:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=affa727dfb200dd46b9b0942598eb58d
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe
Relax bclwdww030 No BCLwSyncdWW
Safe=Fre LwSyncsRR
Time bclwdww030 110.23
$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: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Tue Dec 22 19:46:11 GMT 2009