Mon Dec 28 22:21:40 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)
46174402:>1:r1=0; 1:r3=1;
116105932:>1:r1=1; 1:r3=1;
157719666:>1:r1=0; 1:r3=0;
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.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2016791:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1253759:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
11333775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
849146:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
10119037:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
2164828:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
11878728:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
17739595:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
12473451:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
35350563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
15192425:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
12910905:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
15694399:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
9790694:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
1231904:>1:r1=1; 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.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
17093 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
344395:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1090610:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
536350:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
419124:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
803521:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
818157:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1088733:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2479767:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2283455:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
1994269:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
526883:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
35802 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1316733:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1937200:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
89151 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
713376:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
10607993:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1047053:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
434208:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
136370:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
754292:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
19722275:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
7622942:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1628087:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
12170326:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
9081859:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
13638419:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
6714009:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
3528318:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
13091964:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
32170179:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
11157087:>1:r1=0; 1:r3=1; 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.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
21202998:>1:r1=0; 2:r1=1; 2:r3=0;
12822697:>1:r1=1; 2:r1=1; 2:r3=1;
5311334:>1:r1=0; 2:r1=0; 2:r3=1;
60083580:>1:r1=0; 2:r1=0; 2:r3=0;
47115028:>1:r1=0; 2:r1=1; 2:r3=1;
44560416:>1:r1=1; 2:r1=0; 2:r3=1;
18903947:>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.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
702585:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1412186:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
8154241:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
1200536:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1183713:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
8202425:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
11184909:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
18227953:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
13439758:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
15756333:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
13483571:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
21964630:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
30196847:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
13459161:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1431152:>1:r1=0; 2:r1=1; 3:r1=1; 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.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
78604 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
356311:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
6390 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
183627:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
542379:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
331777:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
513497:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
687996:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1230295:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
1195279:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
1225077:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
585041:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
2730094:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
109898:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
1251531:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1952353:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
8049112:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
786690:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
486710:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1230067:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
2198684:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
459929:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
8903513:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
13360351:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
9938511:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
12282219:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
24904946:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
27973911:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
12236873:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
6736289:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
15430534:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
411028:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1630484:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; 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 21.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
282633:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
258036:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
859397:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2626187:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
3181453:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
1198334:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
4452400:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
4152297:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
2165829:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
28352297:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
43458469:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
18621465:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
31888410:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
22248770:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
46254023:>1:r1=0; 2:r1=0; 2:r3=0; 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.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1083488:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
261961:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
683892:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
1392497:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1564813:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
2875148:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
646248:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1092636:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
4501121:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1250189:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
2175555:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
6852905:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
2961673:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
4478450:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
12914933:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1761267:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
12179182:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
10640469:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
2470156:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
704827:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
4756030:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
9025330:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
1384548:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
8524379:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
5348207:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
10906044:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
14792944:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
1234798:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
12055409:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
253489:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
19227412:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; 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.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
71 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
225 :>1:r1=0; 1:r3=1; 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;
526 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1763 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1872 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5012 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
5399 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
8369 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
16804 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
38994 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
7227 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
31950 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
152164:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
10055 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9304 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
47244 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
109269:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
160526:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
137576:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
39965 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
128889:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
33692 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
60315 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
96233 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
120011:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
53377 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1018923:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
225203:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
712176:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
780767:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
215176:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
124731:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
652088:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
588507:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
696948:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1219093:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
842212:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
853482:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1049817:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1421289:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
733944:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
374888:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
724571:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
826017:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1138630:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
654357:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
745228:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1190094:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1144811:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
653708:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
727958:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5963756:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
853828:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
639615:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1441148:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1177376:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1096972:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3680052:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3724391:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
974887:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
10351348:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
29205517:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6177103:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3969701:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5851851:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3989955:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
11228388:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5913569:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
11182681:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
10224535:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
21761672:>1:r1=2; 1:r3=2; 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 /\ 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.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
33 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
3079569:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
4786405:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
5766080:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
15107790:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
17573184:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
24057370:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
11823406:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
10461109:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
52880889:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
23825512:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
17675775:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
3778966:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
19183912:>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 (32 states)
1 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
527609:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
470129:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1235376:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
563855:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
590321:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1913533:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
1367674:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1293931:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
1502764:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1112902:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
3330957:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
678519:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
570481:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
2568621:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
2630083:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
7053759:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
5169934:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
3217708:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
5321819:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1291977:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
11091498:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
6900705:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
10508078:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
14346751:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
10567849:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
11469456:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
14634651:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
6132324:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
3382502:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
18289375:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
10264858:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 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 21.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5590 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
8614 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
84293 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
55383 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
50218 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
56718 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
197667:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
31802 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
147557:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
273279:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
10368 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
114613:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
131942:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
48085 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
148188:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
79678 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
349134:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
361674:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
325584:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
210494:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
259885:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
1014423:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
97161 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
128813:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
156907:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
388494:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
237850:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
360790:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
769681:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
865031:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
617698:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
544322:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
307036:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
619575:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
2004032:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1005850:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
2996944:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
2318232:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
3610126:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
692444:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
420510:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
847557:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
765237:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
412217:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
530994:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
997811:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
5341724:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
2727508:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
1640607:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
596484:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
4408833:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
2910244:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
7074443:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
5640671:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
2273173:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
2011615:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
6969400:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
2840148:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
15882428:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
8099657:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
9225835:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
10154364:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
14004392:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
15455207:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
9838524:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
7244242:>1:r1=0; 2:r1=1; 3:r1=1; 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.61
$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 22:25:48 NFT 2009