Sat Dec 26 14:06:36 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe036
"SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 8,1
_litmus_P0_4_: stw 8,0(9)
_litmus_P1_0_: li 10,2
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 8,1
_litmus_P1_4_: stw 8,0(9)
Test safe036 Allowed
Histogram (3 states)
33480597:>x=1; y=1;
301454716:>x=2; y=1;
305064687:>x=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=b13e0c20b3a95ec28cc7a23efa1563b6
Cycle=SyncdWW Wse SyncdWW Wse
Relax safe036 No
Safe=Wse SyncdWW
Time safe036 106.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe037
"SyncdWW Wse SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,1
_litmus_P2_4_: stw 10,0(9)
Test safe037 Allowed
Histogram (7 states)
23404245:>x=1; y=2; z=2;
22916096:>x=2; y=1; z=2;
25231141:>x=2; y=2; z=1;
4965869:>x=1; y=1; z=1;
106472793:>x=1; y=1; z=2;
106471121:>x=1; y=2; z=1;
110538735:>x=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=29e092e26d25015c351a682f181e1b0f
Cycle=SyncdWW Wse SyncdWW Wse SyncdWW Wse
Relax safe037 No
Safe=Wse SyncdWW
Time safe037 103.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe038
"LwSyncdWW Wse SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 10,1
_litmus_P2_4_: stw 10,0(9)
Test safe038 Allowed
Histogram (7 states)
29832448:>x=2; y=2; z=1;
26300958:>x=2; y=1; z=2;
102289536:>x=1; y=2; z=1;
103104505:>x=1; y=1; z=2;
23442184:>x=1; y=2; z=2;
110548335:>x=2; y=1; z=1;
4482034:>x=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=9fdaf07975754951c834724222b34025
Cycle=LwSyncdWW Wse SyncdWW Wse SyncdWW Wse
Relax safe038 No
Safe=Wse SyncdWW LwSyncdWW
Time safe038 103.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe040.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe040
"SyncdWR Fre SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe040 Allowed
Histogram (7 states)
25872469:>2:r3=1; y=2; z=2;
2694915:>2:r3=1; y=1; z=1;
29867478:>2:r3=0; y=2; z=1;
89292774:>2:r3=1; y=1; z=2;
99105767:>2:r3=1; y=2; z=1;
111676983:>2:r3=0; y=1; z=1;
41489614:>2:r3=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=60904a5b2739e8950875099ac77c27af
Cycle=SyncdWR Fre SyncdWW Wse SyncdWW Wse
Relax safe040 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe040 98.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe045.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe045
"LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | lwsync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 8,1
_litmus_P0_4_: stw 8,0(9)
_litmus_P1_0_: li 10,2
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 8,1
_litmus_P1_4_: stw 8,0(9)
Test safe045 Allowed
Histogram (3 states)
304233663:>x=1; y=2;
316000023:>x=2; y=1;
19766314:>x=1; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=68b87fd4beebe403e166c8646f0170ab
Cycle=LwSyncdWW Wse SyncdWW Wse
Relax safe045 No
Safe=Wse SyncdWW LwSyncdWW
Time safe045 106.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe046.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe046
"LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 10,1
_litmus_P2_4_: stw 10,0(9)
Test safe046 Allowed
Histogram (7 states)
29621431:>x=1; y=2; z=2;
26493652:>x=2; y=1; z=2;
3442739:>x=1; y=1; z=1;
34773315:>x=2; y=2; z=1;
103473865:>x=1; y=2; z=1;
106100134:>x=2; y=1; z=1;
96094864:>x=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=ef787314c1fb4635934ec5bee20106c0
Cycle=LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse
Relax safe046 No
Safe=Wse SyncdWW LwSyncdWW
Time safe046 101.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe048.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe048
"SyncdWR Fre LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe048 Allowed
Histogram (7 states)
2042282:>2:r3=1; y=1; z=1;
31310547:>2:r3=1; y=2; z=2;
34045329:>2:r3=0; y=2; z=1;
40576431:>2:r3=0; y=1; z=2;
98768597:>2:r3=1; y=2; z=1;
106933686:>2:r3=0; y=1; z=1;
86323128:>2:r3=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=fded52f6a8a54c4d9bf3c0cde8ee353b
Cycle=SyncdWR Fre LwSyncdWW Wse SyncdWW Wse
Relax safe048 No
Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW
Time safe048 97.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe069.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe069
"SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | ;
exists (y=2 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 8,1
_litmus_P0_4_: stw 8,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 7,0(9)
Test safe069 Allowed
Histogram (3 states)
24877149:>1:r3=1; y=1;
314051746:>1:r3=0; y=1;
301071105:>1:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (y=2 /\ 1:r3=0) is NOT validated
Hash=7da20a2ab953c9d18488d3f4e7841bb2
Cycle=SyncdWR Fre SyncdWW Wse
Relax safe069 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe069 97.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe070.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe070
"LwSyncdWW Wse SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | lwsync ;
lwz r3,0(r4) | li r3,1 | li r3,1 ;
| stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ z=2 /\ 0:r3=0)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 10,1
_litmus_P2_4_: stw 10,0(9)
Test safe070 Allowed
Histogram (7 states)
3093320:>0:r3=1; x=1; z=1;
95648417:>0:r3=1; x=1; z=2;
48188880:>0:r3=0; x=2; z=1;
29575356:>0:r3=0; x=1; z=2;
104811804:>0:r3=0; x=1; z=1;
28935404:>0:r3=1; x=2; z=2;
89746819:>0:r3=1; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ z=2 /\ 0:r3=0) is NOT validated
Hash=41c68cedc1ddadab686061c793b3d241
Cycle=LwSyncdWW Wse SyncdWR Fre SyncdWW Wse
Relax safe070 No
Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW
Time safe070 99.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe072.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe072
"SyncdWR Fre SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
lwz r3,0(r4) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (z=2 /\ 0:r3=0 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe072 Allowed
Histogram (7 states)
1437268:>0:r3=1; 2:r3=1; z=1;
88166618:>0:r3=1; 2:r3=0; z=1;
31869252:>0:r3=0; 2:r3=1; z=2;
44797667:>0:r3=1; 2:r3=0; z=2;
51875202:>0:r3=0; 2:r3=0; z=1;
101153716:>0:r3=0; 2:r3=1; z=1;
80700277:>0:r3=1; 2:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated
Hash=545ab7a6a327dd4d73e4f0fc0d60719e
Cycle=SyncdWR Fre SyncdWR Fre SyncdWW Wse
Relax safe072 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe072 97.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe077.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe077
"SyncdWR Fre SyncsWR Fre SyncdWW Wse"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 8,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe077 Allowed
Histogram (13 states)
71643 :>0:r3=2; 2:r3=1; x=2; y=1;
381695:>0:r3=2; 2:r3=2; x=2; y=1;
2900286:>0:r3=2; 2:r3=2; x=2; y=2;
1037282:>0:r3=1; 2:r3=1; x=1; y=1;
8928616:>0:r3=2; 2:r3=0; x=2; y=1;
62561451:>0:r3=1; 2:r3=0; x=1; y=1;
15339139:>0:r3=1; 2:r3=2; x=1; y=1;
38662277:>0:r3=1; 2:r3=2; x=2; y=1;
39758916:>0:r3=1; 2:r3=2; x=1; y=2;
32404308:>0:r3=1; 2:r3=2; x=2; y=2;
80312818:>0:r3=1; 2:r3=1; x=1; y=2;
54218804:>0:r3=1; 2:r3=0; x=2; y=1;
63422765:>0:r3=1; 2:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated
Hash=90440690a11b718ea7844fef30ba96c5
Cycle=SyncdWR Fre SyncsWR Fre SyncdWW Wse
Relax safe077 No
Safe=Fre Wse SyncsWR SyncdWW SyncdWR
Time safe077 103.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe135.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe135
"LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 8,1
_litmus_P0_4_: stw 8,0(9)
_litmus_P1_0_: li 10,2
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 8,1
_litmus_P1_4_: stw 8,0(9)
Test safe135 Allowed
Histogram (3 states)
9223035:>x=1; y=1;
314574085:>x=1; y=2;
316202880:>x=2; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=829af8195a1482485057a881cab011a8
Cycle=LwSyncdWW Wse LwSyncdWW Wse
Relax safe135 No
Safe=Wse LwSyncdWW
Time safe135 102.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe136.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe136
"LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 10,1
_litmus_P2_4_: stw 10,0(9)
Test safe136 Allowed
Histogram (7 states)
1945641:>x=1; y=1; z=1;
34032986:>x=2; y=1; z=2;
98657673:>x=1; y=2; z=1;
34386096:>x=2; y=2; z=1;
34104332:>x=1; y=2; z=2;
97983741:>x=1; y=1; z=2;
98889531:>x=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=20a6a34b6dc3f52d89ffdf88575062ca
Cycle=LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse
Relax safe136 No
Safe=Wse LwSyncdWW
Time safe136 102.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe138.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe138
"SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 10,1
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe138 Allowed
Histogram (7 states)
1352143:>2:r3=1; y=1; z=1;
34619220:>2:r3=0; y=2; z=1;
35284440:>2:r3=1; y=2; z=2;
47865661:>2:r3=0; y=1; z=2;
93474441:>2:r3=1; y=2; z=1;
100791115:>2:r3=0; y=1; z=1;
86612980:>2:r3=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=d9622bc66160015a9bfad53625a07803
Cycle=SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse
Relax safe138 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe138 99.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe158.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe158
"SyncdWR Fre LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync ;
li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | ;
exists (y=2 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 8,1
_litmus_P0_4_: stw 8,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 7,0(9)
Test safe158 Allowed
Histogram (3 states)
9046843:>1:r3=1; y=1;
315172678:>1:r3=0; y=1;
315780479:>1:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (y=2 /\ 1:r3=0) is NOT validated
Hash=178cdf8fa414f9851e5cbee2c97136b0
Cycle=SyncdWR Fre LwSyncdWW Wse
Relax safe158 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe158 95.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe160.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe160
"SyncdWR Fre SyncdWR Fre LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | lwsync | sync ;
lwz r3,0(r4) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (z=2 /\ 0:r3=0 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe160 Allowed
Histogram (7 states)
963057:>0:r3=1; 2:r3=1; z=1;
47747906:>0:r3=1; 2:r3=0; z=2;
35736244:>0:r3=0; 2:r3=1; z=2;
82488758:>0:r3=1; 2:r3=1; z=2;
49846569:>0:r3=0; 2:r3=0; z=1;
97282773:>0:r3=0; 2:r3=1; z=1;
85934693:>0:r3=1; 2:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated
Hash=1aec03977a16ccd6a8c5fc1afed64860
Cycle=SyncdWR Fre SyncdWR Fre LwSyncdWW Wse
Relax safe160 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe160 96.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe165.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe165
"SyncdWR Fre SyncsWR Fre LwSyncdWW Wse"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | lwsync | sync ;
lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 8,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 10,1
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe165 Allowed
Histogram (13 states)
76351 :>0:r3=2; 2:r3=1; x=2; y=1;
2438093:>0:r3=2; 2:r3=2; x=2; y=2;
210675:>0:r3=2; 2:r3=2; x=2; y=1;
497987:>0:r3=1; 2:r3=1; x=1; y=1;
10241490:>0:r3=1; 2:r3=2; x=1; y=1;
7280222:>0:r3=2; 2:r3=0; x=2; y=1;
62618688:>0:r3=1; 2:r3=1; x=2; y=1;
79722587:>0:r3=1; 2:r3=1; x=1; y=2;
64428818:>0:r3=1; 2:r3=0; x=1; y=1;
34923269:>0:r3=1; 2:r3=2; x=2; y=1;
45638772:>0:r3=1; 2:r3=2; x=1; y=2;
55268470:>0:r3=1; 2:r3=0; x=2; y=1;
36654578:>0:r3=1; 2:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated
Hash=c2358315f3b0a52cdef1288bea12e53f
Cycle=SyncdWR Fre SyncsWR Fre LwSyncdWW Wse
Relax safe165 No
Safe=Fre Wse SyncsWR SyncdWR LwSyncdWW
Time safe165 107.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe358.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe358
"SyncdWR Fre SyncdWR Fre"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
lwz r3,0(r4) | lwz r3,0(r4) ;
exists (0:r3=0 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 7,0(9)
Test safe358 Allowed
Histogram (3 states)
12649176:>0:r3=1; 1:r3=1;
313167047:>0:r3=0; 1:r3=1;
314183777:>0:r3=1; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=0 /\ 1:r3=0) is NOT validated
Hash=5db67b28ae44dfb0497cda13c245c4e4
Cycle=SyncdWR Fre SyncdWR Fre
Relax safe358 No
Safe=Fre SyncdWR
Time safe358 104.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe359.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe359
"SyncdWR Fre SyncdWR Fre SyncdWR Fre"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
lwz r3,0(r4) | lwz r3,0(r4) | lwz r3,0(r4) ;
exists (0:r3=0 /\ 1:r3=0 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 7,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 7,0(9)
Test safe359 Allowed
Histogram (7 states)
584798:>0:r3=1; 1:r3=1; 2:r3=1;
79645643:>0:r3=1; 1:r3=0; 2:r3=1;
53928575:>0:r3=0; 1:r3=0; 2:r3=1;
53331164:>0:r3=1; 1:r3=0; 2:r3=0;
53287987:>0:r3=0; 1:r3=1; 2:r3=0;
79335773:>0:r3=0; 1:r3=1; 2:r3=1;
79886060:>0:r3=1; 1:r3=1; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated
Hash=1bb05ee290fb3d2f94afc422c308bf1a
Cycle=SyncdWR Fre SyncdWR Fre SyncdWR Fre
Relax safe359 No
Safe=Fre SyncdWR
Time safe359 92.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe360.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe360
"SyncsWR Fre SyncdWR Fre SyncdWR Fre"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
lwz r3,0(r4) | lwz r3,0(r4) | lwz r3,0(r2) ;
exists (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1)
Generated assembler
_litmus_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 7,0(9)
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 8,0(9)
Test safe360 Allowed
Histogram (13 states)
90069 :>0:r3=1; 1:r3=1; 2:r3=2; y=2;
416868:>0:r3=1; 1:r3=1; 2:r3=1; y=1;
4689535:>0:r3=1; 1:r3=2; 2:r3=1; y=1;
89524 :>0:r3=1; 1:r3=2; 2:r3=2; y=2;
7053515:>0:r3=1; 1:r3=0; 2:r3=2; y=2;
2688039:>0:r3=0; 1:r3=2; 2:r3=2; y=2;
49734396:>0:r3=0; 1:r3=2; 2:r3=1; y=1;
54231110:>0:r3=0; 1:r3=2; 2:r3=1; y=2;
57024033:>0:r3=1; 1:r3=0; 2:r3=1; y=2;
16712046:>0:r3=1; 1:r3=2; 2:r3=1; y=2;
63271121:>0:r3=1; 1:r3=1; 2:r3=1; y=2;
63360455:>0:r3=1; 1:r3=0; 2:r3=1; y=1;
80639289:>0:r3=0; 1:r3=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1) is NOT validated
Hash=73d6bfa4ac7e4a6fa2da6911e5f8c2e3
Cycle=SyncsWR Fre SyncdWR Fre SyncdWR Fre
Relax safe360 No
Safe=Fre SyncsWR SyncdWR
Time safe360 101.20
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O0 -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O0 -pthread"
LITMUSOPTS=
Sat Dec 26 14:40:15 GMT 2009