Mon Dec 28 17:05:23 NFT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr000
"Fre SyncdWW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) ;
sync | ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr000 Allowed
Histogram (3 states)
49138076:>1:r1=0; 1:r3=1;
156713220:>1:r1=0; 1:r3=0;
114148704:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3
Cycle=Fre SyncdWW Rfe PodRR
Relax podrr000 No PodRR
Safe=Fre BCSyncdWW
Time podrr000 14.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr001
"Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
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 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr001 Allowed
Histogram (15 states)
1298477:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1249202:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2003901:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
15557130:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
9769740:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
867613:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
17815805:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
15307577:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
12734159:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1985166:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
12856919:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
9936893:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
11681657:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
35376769:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
11558992:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=2e6b2a124722ed948c8f7dc35dc4b80f
Cycle=Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr001 No PodRR
Safe=Fre BCSyncdWW
Time podrr001 22.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr002
"Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 4,1
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr002 Allowed
Histogram (33 states)
18634 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
406609:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
747497:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1086533:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
439482:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1345763:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
543417:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1177523:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
533000:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
98211 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1135364:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
824857:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
397291:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
33888 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2202685:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
1616830:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2459954:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
6567060:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1993155:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
804436:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
789117:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
2142291:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
10508839:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
12950242:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
126854:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3573591:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
7547218:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
12115232:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
8976202:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
11155310:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
13935134:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
19651891:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
32095890:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c594109cf9f75c58c9eec5a696ceb0a0
Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr002 No PodRR
Safe=Fre BCSyncsWW BCSyncdWW
Time podrr002 22.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr003
"Fre SyncdWW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,1 | stw r3,0(r4) | ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr003 Allowed
Histogram (7 states)
21316791:>1:r1=0; 2:r1=1; 2:r3=0;
5287058:>1:r1=0; 2:r1=0; 2:r3=1;
59048039:>1:r1=0; 2:r1=0; 2:r3=0;
44348340:>1:r1=1; 2:r1=0; 2:r3=1;
19665146:>1:r1=1; 2:r1=0; 2:r3=0;
12786556:>1:r1=1; 2:r1=1; 2:r3=1;
47548070:>1:r1=0; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 210000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=3d48b5b0d8516d3d909b0a4f66959c71
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRR
Relax podrr003 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr003 18.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr004
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr004 Allowed
Histogram (15 states)
671908:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1520836:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1155848:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
8064929:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
1165643:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
11158169:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
8294236:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
13452549:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
18875979:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
13691855:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1469238:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
13448397:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
15492032:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
29798154:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
21740227:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=b2067185c885838837d33372d57790fb
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr004 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr004 22.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr005
"Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r2) | | | ;
exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr005 Allowed
Histogram (33 states)
206443:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
6125 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
80306 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
122790:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
348536:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
413923:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
313712:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
483074:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
537569:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
553388:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
779402:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
584497:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1242140:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
2067977:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
759945:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1233750:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
2788323:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
1363807:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
1232616:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
454279:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
1605088:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
2026253:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
1271415:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
8137652:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
9811771:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
13489279:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
15385177:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
12179318:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
6817552:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
8997391:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
12146254:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
27575114:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
24985134:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1a4d6f8ada041391fb8c242b28f54910
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr005 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr005 22.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr006
"Fre SyncsWW Rfe SyncdRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,2 | stw r3,0(r4) | ;
stw r3,0(r2) | | ;
exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr006 Allowed
Histogram (15 states)
240515:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
2672063:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
823939:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2018189:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
260520:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
2915977:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
3946924:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
21938917:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
4367632:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
1211409:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
27569490:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
43449264:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
47068969:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
32521362:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
18994830:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 210000000
Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=f5e5097c67500c52603a1c0158bb8551
Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR
Relax podrr006 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr006 18.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr007
"Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,2 | li r3,1 | ;
li r3,1 | stw r3,0(r2) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 10,2
_litmus_P1_3_: stw 10,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr007 Allowed
Histogram (31 states)
681185:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
249363:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1367676:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1246198:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
262294:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
4369837:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
2943292:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
640127:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1093343:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
1741365:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
12706243:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1544987:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1087154:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
9009828:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
1373019:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
15100988:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
681866:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
8238431:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
6803507:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
12115778:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
2485880:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
2808086:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
5304410:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
4549726:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
4788610:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
19447420:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
11089399:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
2173147:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
12161478:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
1212357:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
10723006:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c22fcb545cb7b0f7f27c11adc702bd5e
Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR
Relax podrr007 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr007 22.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr008
"Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr008 Allowed
Histogram (72 states)
122 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
247 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
550 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1947 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
10978 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1714 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
284 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
5619 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
5607 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8442 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
10414 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
41469 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
32593 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
156070:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
16270 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
34979 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
7802 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
131386:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
41532 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
136311:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
710684:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
760889:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
54662 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
37145 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
209119:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
54994 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
142871:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
910734:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
154628:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
91070 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
134211:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
219235:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
746887:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
103203:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
529802:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
664068:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1051987:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
663738:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
765931:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
839808:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
685747:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
661958:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1432954:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
781653:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
824568:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
991499:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1445591:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1043650:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3599704:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
659359:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1148860:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
508020:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1145826:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3706195:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
712602:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
6079045:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3998526:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5953180:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
862211:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1134236:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1137728:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
5964038:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1190585:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
10286347:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
11289806:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3886107:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
10320212:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1209441:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
6233436:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
21626809:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
28781112:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
11208993:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=58c192e74d841e0ccb20b3014a58a473
Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR
Relax podrr008 No PodRR
Safe=Fre BCSyncsWW
Time podrr008 22.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr009
"Fre SyncdWW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,2 | ;
li r3,1 | stw r3,0(r2) | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 10,2
_litmus_P1_3_: stw 10,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr009 Allowed
Histogram (14 states)
41 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
5786492:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
3125361:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
18687548:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
17590792:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
23805724:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
17682945:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
4872897:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
11983515:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
23733038:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
10478442:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
15315482:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
3829219:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
53108504:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 210000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d6249053a9b844d8e7a3045b38500a3a
Cycle=Fre SyncdWW Rfe SyncsRW Rfe PodRR
Relax podrr009 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW
Time podrr009 17.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr010
"Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r4) | | | ;
exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 10,2
_litmus_P2_3_: stw 10,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr010 Allowed
Histogram (31 states)
715858:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1421985:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1354833:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
490477:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1289563:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
1094515:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
558034:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
3338920:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
582120:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
6205822:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
7024371:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
3244777:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
10667233:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
3203066:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
1245496:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
10334316:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
10878366:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1949254:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
11541811:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
5199996:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
5195707:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
14748338:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
2634945:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
6904208:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
553338:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
2537451:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
10545285:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1422900:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
515450:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
14601831:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
17999734:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=fcb68021656d7cbdb455ef5bd2648d65
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr010 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr010 22.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/podrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr011
"Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r2) | | | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 10,2
_litmus_P2_3_: stw 10,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr011 Allowed
Histogram (66 states)
5039 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
9950 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
7218 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
246879:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
79847 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
41501 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
196319:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
151097:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
58684 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
33043 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
388357:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
79922 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
336570:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
52424 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
331128:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
61204 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
118471:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
157574:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
224471:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
136583:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
132497:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
263667:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
408637:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1010948:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
793161:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
412225:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
94492 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
539208:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
240896:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
162696:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
858875:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
604804:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
403264:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
300686:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
761597:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
613072:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
526875:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
1947089:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
361237:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
1019942:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
838166:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
2773301:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
697095:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
592260:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
4373315:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1665800:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
3669039:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
2299248:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
9784084:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
2892898:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
961767:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
2000730:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
2968885:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
7272469:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
5564370:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
6924801:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
15839460:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
10008673:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
15483603:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
2833231:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
2318699:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
5354606:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
6933333:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
14124164:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
8373863:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
9279991:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a463a88f960487eded38b9c473eec1b5
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr011 No PodRR
Safe=Fre BCSyncsWW BCSyncsRW BCSyncdRW
Time podrr011 21.82
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=-r 100
Mon Dec 28 17:09:32 NFT 2009