Mon Dec 28 11:50:43 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)
113202081:>1:r1=1; 1:r3=1;
49776642:>1:r1=0; 1:r3=1;
157021277:>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.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2049895:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1227690:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1179873:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
17697635:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
13051094:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1943808:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
863560:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
11232963:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
15887352:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
9965432:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
11660986:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
15584839:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
35348736:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
9797424:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
12508713:>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.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
37048 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
140445:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
428948:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
93679 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
18119 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
789182:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
408249:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
725070:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1191239:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1400020:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
820876:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
494694:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2246449:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
473285:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
560705:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2079560:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1064334:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2359511:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1608366:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
10146891:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1102276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
8985219:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
13113374:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
3683838:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
2027891:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
10937323:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
19888885:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
7873185:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
802955:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
6754370:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
31818114:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
13906464:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
12019436:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 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.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
18977684:>1:r1=1; 2:r1=0; 2:r3=0;
5691049:>1:r1=0; 2:r1=0; 2:r3=1;
20588502:>1:r1=0; 2:r1=1; 2:r3=0;
43977028:>1:r1=1; 2:r1=0; 2:r3=1;
60655082:>1:r1=0; 2:r1=0; 2:r3=0;
47802593:>1:r1=0; 2:r1=1; 2:r3=1;
12308062:>1:r1=1; 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.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
679763:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1139890:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
1239368:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1427854:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1295642:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
8147759:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
8036631:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
18936026:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
13973666:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
21614569:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
15748562:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
11272592:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
13540048:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
29913371:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
13034259:>1:r1=0; 2:r1=0; 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.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5807 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
85061 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
362342:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
175313:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
1182665:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
284327:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
445735:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
123230:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
2012275:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
680885:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1223288:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
524523:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
546942:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
789450:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1261619:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1255365:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
516758:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
493768:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1510986:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
9755800:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
2701864:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
1352928:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
27938340:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
6540690:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
9090324:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
24568424:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
13835650:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
445632:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
15345985:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
8187253:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
12277797:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
12422127:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
2056847:>1:r1=2; 2:r1=1; 3:r1=0; 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 22.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
237015:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
828630:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2525612:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
4362976:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
3184056:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
284264:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
1250021:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
3877126:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
18859474:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
28115578:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
22198086:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
2074877:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
31604668:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
43504900:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
47092717:>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.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1542463:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1185949:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
1270618:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
737485:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
1163592:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
273144:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
2763335:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
8500178:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
697467:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
8816159:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
237929:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
3106502:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
4195802:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
4917094:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
2068377:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
10867354:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
4682588:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
1123054:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
15319791:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
2506006:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
12264991:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
708598:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
1185367:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
12271910:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
1880870:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
19260697:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
12687057:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
6947414:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
10497676:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
5034252:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
1286281:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; 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.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
94 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
188 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1755 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
532 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
351 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1581 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
10424 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
7179 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
15140 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
9984 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
31749 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
32854 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
35391 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4854 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
31538 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
57400 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
7242 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
39900 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
157452:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
115918:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
125521:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
99935 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
150364:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
5305 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
126492:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
56666 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
125593:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
93563 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
755334:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
562653:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
805482:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
742299:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
769026:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
684817:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
832842:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
971834:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
225950:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
675309:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
692034:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1140329:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
220603:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
987081:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
740948:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
418482:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1096896:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
634172:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1098703:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
5887041:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1169305:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1206444:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1195445:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1438246:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
898172:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3670061:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
6071411:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1435479:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
677020:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
725461:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3704340:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
848342:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1027737:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
10455194:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
10977848:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
6286068:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3986670:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
702421:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
21931645:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
10685842:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6172951:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
11045626:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
28486109:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3915362:>1:r1=2; 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.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
36 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
3113347:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
3934771:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
10618373:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
23574136:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
17814760:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
17460947:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
14529175:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
24831875:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
18411079:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
6097997:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
11731855:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
4751751:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
53129898:>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.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
530083:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
592757:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
474673:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1071370:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
617061:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1311214:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
594778:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
1217370:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
1893035:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
3503892:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
3236209:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
6847208:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
693604:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1378855:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1315856:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
3191089:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
10826772:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
2470704:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
2524821:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
14367769:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
5375347:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
5117109:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
6181371:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
6806671:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
18409704:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
11576803:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
10248028:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
10373063:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1555824:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
14691561:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
11005398:>1:r1=0; 2:r1=0; 3:r1=1; 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.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (67 states)
1 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
7902 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
32495 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
89403 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
85562 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
50160 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
59696 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
159723:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
5675 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
10387 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
139279:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
163825:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
365984:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
101569:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
317618:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1736485:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
49825 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
270022:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
537759:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
156163:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
406380:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
222801:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
668928:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
180468:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
59696 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
881333:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
445844:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1032763:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
1064333:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
2108518:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
224030:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
349465:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
392615:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
2793423:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
619847:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
930334:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
133440:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
7029979:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
2148606:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
422311:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
494927:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
2284807:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
670119:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
3738993:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
845794:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
8536299:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
742149:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
15795098:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
4527664:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
5252026:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
9104309:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
2866457:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
122184:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
254459:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
363119:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
7206775:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
2927135:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
5416062:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
6839269:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
10435427:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
876573:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
2084746:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
9801854:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
2901918:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
652007:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
14008554:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
14796629:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; 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.65
$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 11:54:52 NFT 2009