Wed Dec 23 13:43:41 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)
11436640:>1:r1=1; 1:r3=1;
5219586:>1:r1=0; 1:r3=1;
15343774:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 32000000
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 2.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
128573:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
199131:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
108874:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
196178:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1674000:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1160627:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1131763:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1608621:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
105530:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1286602:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3411695:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1615309:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1023832:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
999716:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
1349549:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 16000000
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 6.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5019 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
15977 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
775 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
42568 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
52106 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
322110:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
40246 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
55014 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
48013 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
85587 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
227512:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
178459:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
156900:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
22446 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
177770:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
71255 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
107700:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
164169:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
64577 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
242695:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1500193:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
278896:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1016817:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
746362:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
64344 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
804596:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1913474:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1289053:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
944816:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
227405:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
948172:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1213122:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2971852:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
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 8.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1203527:>1:r1=1; 2:r1=1; 2:r3=1;
747784:>1:r1=0; 2:r1=0; 2:r3=1;
1903046:>1:r1=0; 2:r1=1; 2:r3=0;
6307758:>1:r1=0; 2:r1=0; 2:r3=0;
4670401:>1:r1=0; 2:r1=1; 2:r3=1;
4458283:>1:r1=1; 2:r1=0; 2:r3=1;
1709201:>1:r1=1; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 21000000
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 3.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
75763 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
145884:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
122115:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1113455:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
1343531:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
818097:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
1586975:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
99998 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
133578:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1309608:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
1931623:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
1412534:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
2212066:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
800911:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
2893862:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 16000000
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 4.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
599 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
11372 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
30116 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
138077:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
54631 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
14037 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
94646 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
44224 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
7015 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
85344 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
42495 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
32076 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
130948:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
50803 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
54665 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
679697:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
204500:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
52654 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
123856:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
127385:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
127992:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2707747:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
270923:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
946069:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
206980:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1022911:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
100858:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1387288:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1188256:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
1207047:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
857275:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1597033:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
2400481:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
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 2.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
27300 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
274387:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
230950:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
389905:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
23561 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
83493 :>1:r1=1; 2:r1=0; 2:r3=2; y=2;
102299:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
272340:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
421627:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
1765095:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
3171052:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
2655403:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
4436596:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
2248476:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
4897516:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 21000000
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 1.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
113235:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
276844:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
26675 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
73146 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
21019 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
110662:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
115196:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
131803:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
885084:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
69136 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
62002 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
173433:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
110561:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
496548:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
523840:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
171954:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
839099:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
291165:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
474413:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
242537:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
1248238:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1622379:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
426429:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1203630:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
196481:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1068613:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
1248621:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
1859543:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
1054609:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
721398:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
141707:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 16000000
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 2.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
8 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
19 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
32 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
167 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
452 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
51 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
264 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
55673 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
62434 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
91252 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
50862 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
71045 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
92 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
380657:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
11981 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
564 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2756 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
382626:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
65671 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
585430:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
100168:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
9319 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2783 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
831 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
7327 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
85196 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
366846:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
75454 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
765 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
10420 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
59404 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
74009 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
137010:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
60971 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
64076 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
13141 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1084339:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4301 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
616229:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
8406 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
103798:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
62999 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
379312:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1307 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
75748 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
611570:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
8052 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
89591 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
15936 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
57782 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1100936:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
85808 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3766 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
105377:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
14165 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
117448:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
771 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
114300:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
19141 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17055 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
108425:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
6173 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
138718:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
632216:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
119515:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1043584:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
76505 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5982 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
108289:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2894823:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2263807:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1074070:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 16000000
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 2.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
9 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
489025:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
390429:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
311377:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
2449827:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
1823122:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
991816:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
1487145:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
1268181:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
1875367:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
1679321:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
558884:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
5394504:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
2280993:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 21000000
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 1.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
49180 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
59273 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
131936:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
73247 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
146039:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
670745:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
192200:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
54712 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
134906:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
635191:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
109060:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
58346 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
606154:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
248324:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
134509:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
567218:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
326561:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
138258:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
520540:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
309466:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
1113307:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
238464:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1175274:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1474752:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
53886 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
349354:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1120291:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1104546:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1089619:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1702173:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1412469:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
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 2.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
561 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
869 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
13392 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
12547 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
8645 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
31753 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1014 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
23392 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
2841 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
6230 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
3404 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
21565 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
35584 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
16725 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
19868 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
39232 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
5211 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
4778 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
14644 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
42743 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
41584 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
25445 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
78338 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
16295 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
73232 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
96132 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
34537 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
215565:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
89229 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
9091 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
113392:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
69551 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
15698 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
23694 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
56965 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
11414 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
360090:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
42635 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
35522 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
31688 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
69465 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
56145 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
942538:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
101425:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
279916:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
310371:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
80569 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
485171:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
162186:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
235515:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
294528:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
281979:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
582485:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
698151:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
195745:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
212599:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
724500:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
502991:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
934232:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
946255:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
713179:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
1558301:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1487008:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
856592:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
75081 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
1467978:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 16000000
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 2.21
$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=
Wed Dec 23 13:44:25 NFT 2009