Tue Dec 29 20:21:09 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)
47689544:>1:r1=0; 1:r3=1;
157547852:>1:r1=0; 1:r3=0;
114762604:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3
Cycle=Fre SyncdWW Rfe PodRR
Relax podrr000 No PodRR
Safe=Fre BCSyncdWW
Time podrr000 14.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2038227:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1253049:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1257015:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
833303:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
11732977:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
11507072:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
15595861:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
12672600:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
10112835:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
10160136:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
12654972:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
34761785:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2026534:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
17767088:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
15626546:>1:r1=0; 1:r3=1; 3:r1=0; 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.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
95623 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
17227 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
35746 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
132769:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
424198:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
475151:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1911912:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
792505:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
700109:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
511201:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
826027:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1388297:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1609881:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1125174:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2314535:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
553014:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1176099:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
769352:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
3662427:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
10902732:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1998510:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
7793683:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
338329:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2316787:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
13116059:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
10408558:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
943345:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
12057853:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
9085240:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
6826865:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
13579729:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
20143631:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
31967432:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c594109cf9f75c58c9eec5a696ceb0a0
Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr002 No PodRR
Safe=Fre BCSyncsWW BCSyncdWW
Time podrr002 22.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12627719:>1:r1=1; 2:r1=1; 2:r3=1;
20798935:>1:r1=0; 2:r1=1; 2:r3=0;
5470072:>1:r1=0; 2:r1=0; 2:r3=1;
44168302:>1:r1=1; 2:r1=0; 2:r3=1;
47628541:>1:r1=0; 2:r1=1; 2:r3=1;
60470360:>1:r1=0; 2:r1=0; 2:r3=0;
18836071:>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.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
695133:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1440780:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
1237752:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1161631:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
13428861:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
8082918:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
1528671:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
13520255:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
8007809:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
15595203:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
18694312:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
21849195:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
11292526:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
13519519:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
29945435:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=b2067185c885838837d33372d57790fb
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr004 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr004 22.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5866 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
348745:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
1210120:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
208464:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
455047:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
123414:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
781478:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
2780800:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
79693 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
590901:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
758770:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1272242:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
576109:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
541947:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
2126044:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
7973681:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
214202:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1705370:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
24705826:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2014512:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
430896:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
9032310:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
471325:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
6899944:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
12428779:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
15330457:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1249396:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1346045:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
1232885:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
13563754:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
27775857:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
12139826:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
9625295:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1a4d6f8ada041391fb8c242b28f54910
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr005 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr005 22.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
261979:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
1174558:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
243408:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
2514488:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
821628:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
4077374:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
2056905:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
2898937:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
18867789:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
4282671:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
27996843:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
32274277:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
46971188:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
22054749:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
43503206:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 210000000
Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=f5e5097c67500c52603a1c0158bb8551
Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR
Relax podrr006 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr006 18.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
722580:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
682346:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1357100:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1229131:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
666820:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
247305:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1388873:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
4429394:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
1122736:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
1217792:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
260147:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
2141102:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1538249:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
2855672:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
2428439:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
4340063:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
4738569:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
8834564:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
12031787:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
1863450:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
10908545:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
8631086:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
10800869:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
19385095:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
12912959:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
14858465:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
1073050:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
2931421:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
12321141:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
6917428:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
5163822:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c22fcb545cb7b0f7f27c11adc702bd5e
Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR
Relax podrr007 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr007 22.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
223 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
144 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
261 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
543 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1701 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1542 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
7309 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
4974 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
147589:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
5167 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
14134 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
39456 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
10366 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8079 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
32669 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
39895 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
118428:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
30103 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
53419 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
50420 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
10006 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
495811:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
138343:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
133005:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
981694:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
501029:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
85667 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
96462 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
683309:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
135188:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
158856:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
37873 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
198546:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
188680:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
685730:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
733898:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1104206:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
608076:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1373295:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1131505:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
657236:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
679143:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
855735:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3947068:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
730579:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1398602:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1007202:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
668991:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
789719:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1130632:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
841058:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
649057:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1047987:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
713889:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1143117:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
793609:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
6166300:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1136014:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1148587:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6051863:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3658519:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5831697:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5869090:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
991510:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3965295:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
22097750:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3696550:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
10358128:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
10340058:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
11264747:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
11085355:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
29237312:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=58c192e74d841e0ccb20b3014a58a473
Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR
Relax podrr008 No PodRR
Safe=Fre BCSyncsWW
Time podrr008 22.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
48 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
3779224:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
11818514:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
3104369:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
4794655:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
17852305:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
5810887:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
18064675:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
10121276:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
15059448:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
23789500:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
52844213:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
23676246:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
19284640:>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 18.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1941208:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
1417914:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1227855:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
576545:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
1284922:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
1049731:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
692616:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
566925:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
1236716:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
2649965:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
1540755:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
483544:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
3226961:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
5197417:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
10514289:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
5232491:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
534281:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
3325702:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
10820630:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
17930319:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
2509809:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
14271920:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
592999:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
3411982:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
11104599:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
11472248:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
10270834:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
6037731:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
7073130:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
7033576:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
14770386:>1:r1=0; 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.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5074 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
7575 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
9754 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
44350 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
133358:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
77773 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
31610 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
134422:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
58677 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
222516:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
50742 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
165508:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
112154:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
364516:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
344196:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
86226 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
217109:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
245087:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
60192 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
241260:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
436288:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
98748 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
822256:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
362874:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
200227:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
423185:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
766094:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
3573716:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
598662:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
416148:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
157132:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
171730:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
703842:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
1043984:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
2383341:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
2357112:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
2946589:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
1998314:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
605125:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
4416764:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1707717:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
518861:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
535472:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
620732:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
981304:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
411719:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
847487:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
3064306:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
5661255:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
835611:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
6995511:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
7007453:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
9413866:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
5291200:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
7117887:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
2864491:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
2762647:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
305152:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
14221231:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
9752426:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
953696:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
15050745:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
10401847:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
15314245:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
2005614:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
8263295:>1:r1=2; 2:r1=0; 3:r1=1; 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.60
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=-r 100
Tue Dec 29 20:25:18 NFT 2009