Tue Dec 29 09:44:36 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)
113407262:>1:r1=1; 1:r3=1;
157431998:>1:r1=0; 1:r3=0;
49160740:>1:r1=0; 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.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1165239:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1201092:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1944200:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
955234:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
11289752:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1975410:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
17455221:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
11263468:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
9958394:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
12794710:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
15811762:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
35333455:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
15947221:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
10033454:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
12871388:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
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.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
37732 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
455396:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
16708 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1326072:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
126784:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
551982:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
485953:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
792885:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
79474 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
371793:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2345210:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1127091:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
405490:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
811411:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1979514:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
778272:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
741725:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1125053:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1581193:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
3688236:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
10288428:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
8969671:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
19961263:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
7831012:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2212956:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
10957820:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
954417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
13755479:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
12135812:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
6800829:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1953587:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
13097809:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
32252943:>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.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12363253:>1:r1=1; 2:r1=1; 2:r3=1;
43619591:>1:r1=1; 2:r1=0; 2:r3=1;
5774845:>1:r1=0; 2:r1=0; 2:r3=1;
60884655:>1:r1=0; 2:r1=0; 2:r3=0;
47722134:>1:r1=0; 2:r1=1; 2:r3=1;
20691054:>1:r1=0; 2:r1=1; 2:r3=0;
18944468:>1:r1=1; 2:r1=0; 2:r3=0;
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.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1402620:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1397597:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
699527:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
13397846:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
1069347:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
21622964:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
7926036:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
8268807:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
10851918:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
12982046:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
13919616:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
15747647:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
19243222:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
1255745:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
30215062:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
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.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5763 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
216310:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
540308:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
478508:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
86907 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
380159:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
128313:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
1536192:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
1150619:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
2123877:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
202339:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
427924:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
1160791:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
579649:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1265998:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
444086:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
742947:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1233880:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
2657395:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
765320:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
6606204:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
2013851:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
505382:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
8178053:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
15674735:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1355371:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
12459768:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
12111080:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
27732149:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
9732484:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
9055811:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
13871695:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
24576132:>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.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
250131:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
837144:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2741029:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
279490:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
2156178:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
3944439:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
3128204:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
1205997:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
28053068:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
47579209:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
21803462:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
42637445:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
4365604:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
31768995:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
19249605:>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 17.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1177158:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
2104072:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1360182:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1600067:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
699836:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
1245325:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
2653137:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
4137600:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1117284:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
4929694:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
676564:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
10826910:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
1129498:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
240497:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
12667615:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
692940:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
6817764:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
3115903:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
4674977:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
10414227:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
12024495:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
1846247:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
4815439:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
267918:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
19578176:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
1152919:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
12436004:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
2461288:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
15390778:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
8903704:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
8841782:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
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.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (73 states)
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
216 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
102 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
470 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
204 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1754 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
6013 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1982 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
10451 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
34974 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
39325 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
8202 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
155901:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
34920 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
7781 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
48433 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5274 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
49307 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
141403:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
151394:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
9952 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
121606:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
34035 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
15441 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
89145 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
619303:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
138483:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
98477 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
32225 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
669554:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
191967:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
155859:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
730142:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1014201:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
692932:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1159990:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
785465:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
979307:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
194942:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
710601:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1023752:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1115672:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
526741:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
721238:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
676756:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1152502:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
812222:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
761458:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
803682:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
752458:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3640909:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1045532:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1128413:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
726615:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1142349:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6002540:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
11235396:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1146627:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
647718:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
853774:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6145199:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1398511:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
11046926:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
10282188:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4088972:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6091704:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1384757:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6106674:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3975021:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
10466911:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
21971735:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3623776:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
28359538:>1:r1=0; 1:r3=0; 3:r1=0; 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.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
65 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
4837748:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
11676940:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
5987449:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
23528989:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
3160837:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
17036089:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
10839959:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
17894199:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
14731080:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
3879173:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
53126676:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
24936128:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
18364668:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
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.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
616570:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
544466:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
495947:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1224821:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
1870099:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
6755681:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
553687:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
3180677:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
1359312:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1314350:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
693131:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1328858:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
1458834:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
570098:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
3215587:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
3532941:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
2503914:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
5329885:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
5122395:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
11477909:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
6942315:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
6196324:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
10538066:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
2508463:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
14424506:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
10398473:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
10937720:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1073433:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
10701464:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
18295032:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
14835042:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
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.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (68 states)
1 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
44697 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
5388 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
8238 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
10333 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
320431:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
127931:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
33821 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
353642:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
310645:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
230912:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
314726:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
80906 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
55239 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
81690 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
147200:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
137872:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
399311:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
56992 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
52815 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
248138:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
512266:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
427272:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
147279:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
98241 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
154812:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
118806:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
310214:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
780927:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
242524:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
230067:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
625061:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
1100725:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
1634022:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
638105:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
352252:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
643857:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
2258959:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
526431:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
3684846:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
7045790:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
889500:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
423929:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
709602:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
835951:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
1003180:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
2107663:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
2899050:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
5510089:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
5377590:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
2857772:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
2873341:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
4371380:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
8173930:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
918270:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
2347585:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
14304770:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
6916319:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
6936602:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
9788149:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
2140458:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
738828:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
3072685:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
10004552:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
9180728:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
15285383:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
15779309:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 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.73
$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
Tue Dec 29 09:48:45 NFT 2009