Wed Dec 30 17:13:17 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)
48022563:>1:r1=0; 1:r3=1;
114441804:>1:r1=1; 1:r3=1;
157535633:>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.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1244552:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1211342:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2003641:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2009193:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
11419536:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
17526992:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
9860571:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
12619276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
15471610:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
899730:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
11575789:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
35607917:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
12688220:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
9943344:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
15918287:>1:r1=0; 1:r3=0; 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.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
16898 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
143572:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
37679 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
535086:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
96815 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
785900:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
820999:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
504549:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
413091:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
433869:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1972098:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2401157:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
3731428:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1645891:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
6573450:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1119509:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
464460:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
743141:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2083474:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
9269916:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1096687:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1385673:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
812247:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
19609371:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
13848029:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1167958:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
32104851:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
13299083:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
10221528:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2101682:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
11844440:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
11001134:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
7714335:>1:r1=0; 1:r3=0; 3:r1=1; 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.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12641197:>1:r1=1; 2:r1=1; 2:r3=1;
19624241:>1:r1=1; 2:r1=0; 2:r3=0;
20715406:>1:r1=0; 2:r1=1; 2:r3=0;
5637143:>1:r1=0; 2:r1=0; 2:r3=1;
47580376:>1:r1=0; 2:r1=1; 2:r3=1;
43782769:>1:r1=1; 2:r1=0; 2:r3=1;
60018868:>1:r1=0; 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.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
669123:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1431898:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1441933:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
1125059:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
21730893:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
13537824:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1263979:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
18814213:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
30107932:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
7882894:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
8162545:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
11185578:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
13517383:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
15803404:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
13325342:>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.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6302 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
81517 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
251578:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
112420:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
534103:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
428573:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
343963:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
706534:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1208976:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
1237519:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
522570:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
1556043:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
433285:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
2829613:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
1237908:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
2064406:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
765549:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1989555:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1206724:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
200840:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
1300738:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
8287884:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
9843101:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
586879:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
15384043:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
24528711:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
489677:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
13908765:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
9036227:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
6626764:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
12457984:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
27664486:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
12166763:>1:r1=0; 2:r1=0; 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 22.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
227383:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
3390583:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
2497160:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
286421:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
807943:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2138324:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
3931917:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
1247810:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
4123708:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
18465403:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
32278335:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
27726227:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
43708432:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
21687201:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
47483153:>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 17.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
258273:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
223916:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
703743:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
1138558:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
1375170:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1196296:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
732260:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
1275347:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1137678:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
1089690:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1586335:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
1876498:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
2511774:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
6915183:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
12178334:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
4600192:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
10781533:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
2898226:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
670908:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
4317688:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
19362926:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
8473362:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
2938710:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
4784328:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
2203086:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
12259185:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
8817839:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
5044095:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
12798487:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
10833367:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
15017013:>1:r1=0; 2:r1=0; 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.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
111 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
211 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
272 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
600 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1603 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4668 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
10719 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1896 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5220 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
14983 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
10089 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
7439 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
57516 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
33999 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
39967 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
7710 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
36204 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
133398:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
152193:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
132616:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
139851:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
143221:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
502698:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
39755 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
97802 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
33024 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
148592:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
94713 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
201883:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
701818:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
718292:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
941211:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1418840:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
702634:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
51488 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
823130:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
436668:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
782934:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1402659:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
694523:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
206927:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1102739:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1179626:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
778225:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
844456:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
717689:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
632367:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1021042:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1122145:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
913070:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
748612:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
713294:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1135623:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1152791:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
675427:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1053671:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1195680:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
830653:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3913706:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
28934918:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6077383:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3939222:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6010975:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6076792:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3617795:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3583738:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
6346325:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
11027925:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
11306946:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
21835514:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
10101543:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
10476030:>1:r1=2; 1:r3=2; 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.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
24 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
3799885:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
3158297:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
4812737:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
24418420:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
10374475:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
6091564:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
12069837:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
14738846:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
19025105:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
17702209:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
23311685:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
53043296:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
17453620:>1:r1=0; 2:r1=2; 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 18.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1297606:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
601881:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
483652:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1368084:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
588966:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
1903339:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
566483:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
1112366:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
2522407:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
5102034:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1301549:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
691521:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1243417:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
527562:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
6774337:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
6223853:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
7007013:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
3146048:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
3262265:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
18449630:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
10897178:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
11616899:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1499685:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
3405446:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
2525918:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
5378830:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
14566190:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
10890425:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
10242858:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
10190877:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
14611681:>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.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5881 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
7880 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
34318 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
54681 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
56757 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
110235:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
229486:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
10498 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
317990:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
450367:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
137235:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
83308 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
86377 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
244173:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
165806:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
275519:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
396658:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
47175 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
160013:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
151444:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
327910:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
362970:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
546837:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
1204866:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
145980:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
4324208:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
528757:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
764819:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
320286:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
980470:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
2148145:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
2296196:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
2045671:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
923742:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
122556:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
444767:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
701512:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
1006115:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
865297:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
2996573:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
1702566:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
254282:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
408286:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
631736:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
356341:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
2996130:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
56134 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
7052682:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
10168256:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
2194482:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
646272:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
798596:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
7932946:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
2920937:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
14910102:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
9172204:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
7147765:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
609069:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
7107669:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
3715910:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
9821227:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
13980935:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
2821137:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
5571836:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
5433908:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
15505114:>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 22.06
$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
Wed Dec 30 17:17:27 NFT 2009