Mon Dec 28 15:23:54 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_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_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 safe036 Allowed
Histogram (3 states)
294906819:>x=2; y=1;
50811363:>x=1; y=1;
294281818:>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 63.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,2
_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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_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 safe037 Allowed
Histogram (7 states)
23676068:>x=2; y=1; z=2;
24024646:>x=1; y=2; z=2;
6777449:>x=1; y=1; z=1;
107780258:>x=2; y=1; z=1;
107801683:>x=1; y=1; z=2;
106843247:>x=1; y=2; z=1;
23096649:>x=2; y=2; 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 64.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_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 safe038 Allowed
Histogram (7 states)
5218184:>x=1; y=1; z=1;
29562832:>x=2; y=2; z=1;
27187302:>x=2; y=1; z=2;
98806960:>x=1; y=2; z=1;
111988038:>x=2; y=1; z=1;
103472257:>x=1; y=1; z=2;
23764427:>x=1; y=2; z=2;
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 66.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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 safe040 Allowed
Histogram (7 states)
39685280:>2:r3=0; y=1; z=2;
3638429:>2:r3=1; y=1; z=1;
33762911:>2:r3=0; y=2; z=1;
23781055:>2:r3=1; y=2; z=2;
92487431:>2:r3=1; y=1; z=2;
94178006:>2:r3=1; y=2; z=1;
112466888:>2:r3=0; y=1; z=1;
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 64.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_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 safe045 Allowed
Histogram (3 states)
34248306:>x=1; y=1;
293814401:>x=1; y=2;
311937293:>x=2; 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 62.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe046 Allowed
Histogram (7 states)
3195565:>x=1; y=1; z=1;
30387419:>x=1; y=2; z=2;
106487921:>x=2; y=1; z=1;
95924975:>x=1; y=1; z=2;
102751162:>x=1; y=2; z=1;
33743951:>x=2; y=2; z=1;
27509007:>x=2; 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 67.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe048 Allowed
Histogram (7 states)
29744347:>2:r3=1; y=2; z=2;
2314024:>2:r3=1; y=1; z=1;
39084459:>2:r3=0; y=1; z=2;
37797844:>2:r3=0; y=2; z=1;
108453493:>2:r3=0; y=1; z=1;
85730623:>2:r3=1; y=1; z=2;
96875210:>2:r3=1; y=2; z=1;
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 63.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,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 safe069 Allowed
Histogram (3 states)
32393137:>1:r3=1; y=1;
309905878:>1:r3=0; y=1;
297700985:>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 64.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe070 Allowed
Histogram (7 states)
2854909:>0:r3=1; x=1; z=1;
27231667:>0:r3=1; x=2; z=2;
94962059:>0:r3=1; x=2; z=1;
104387371:>0:r3=0; x=1; z=1;
47349346:>0:r3=0; x=2; z=1;
90750038:>0:r3=1; x=1; z=2;
32464610:>0:r3=0; x=1; z=2;
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 64.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe072 Allowed
Histogram (7 states)
1292832:>0:r3=1; 2:r3=1; z=1;
40028275:>0:r3=1; 2:r3=0; z=2;
35100994:>0:r3=0; 2:r3=1; z=2;
54130181:>0:r3=0; 2:r3=0; z=1;
93673554:>0:r3=1; 2:r3=0; z=1;
77754448:>0:r3=1; 2:r3=1; z=2;
98019716:>0:r3=0; 2:r3=1; z=1;
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 65.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test safe077 Allowed
Histogram (13 states)
486158:>0:r3=2; 2:r3=2; x=2; y=1;
117819:>0:r3=2; 2:r3=1; x=2; y=1;
2260074:>0:r3=2; 2:r3=2; x=2; y=2;
6568237:>0:r3=2; 2:r3=0; x=2; y=1;
63770467:>0:r3=1; 2:r3=0; x=1; y=1;
1485340:>0:r3=1; 2:r3=1; x=1; y=1;
35958043:>0:r3=1; 2:r3=2; x=2; y=1;
63287861:>0:r3=1; 2:r3=1; x=2; y=1;
36442952:>0:r3=1; 2:r3=2; x=1; y=2;
78494273:>0:r3=1; 2:r3=1; x=1; y=2;
34286384:>0:r3=1; 2:r3=2; x=2; y=2;
19134299:>0:r3=1; 2:r3=2; x=1; y=1;
57708093:>0:r3=1; 2:r3=0; 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 62.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test safe135 Allowed
Histogram (3 states)
18222440:>x=1; y=1;
311326892:>x=1; y=2;
310450668:>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 65.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe136 Allowed
Histogram (7 states)
34859751:>x=1; y=2; z=2;
34453756:>x=2; y=1; z=2;
1986883:>x=1; y=1; z=1;
99221496:>x=2; y=1; z=1;
98296528:>x=1; y=1; z=2;
97610878:>x=1; y=2; z=1;
33570708:>x=2; y=2; 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 66.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe138 Allowed
Histogram (7 states)
1328739:>2:r3=1; y=1; z=1;
36819247:>2:r3=0; y=2; z=1;
93508673:>2:r3=1; y=2; z=1;
87978382:>2:r3=1; y=1; z=2;
34478193:>2:r3=1; y=2; z=2;
99696707:>2:r3=0; y=1; z=1;
46190059:>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=d9622bc66160015a9bfad53625a07803
Cycle=SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse
Relax safe138 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe138 63.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test safe158 Allowed
Histogram (3 states)
17165945:>1:r3=1; y=1;
307701685:>1:r3=0; y=1;
315132370:>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 64.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe160 Allowed
Histogram (7 states)
724509:>0:r3=1; 2:r3=1; z=1;
48251544:>0:r3=1; 2:r3=0; z=2;
38777100:>0:r3=0; 2:r3=1; z=2;
85991391:>0:r3=1; 2:r3=0; z=1;
81200368:>0:r3=1; 2:r3=1; z=2;
94099317:>0:r3=0; 2:r3=1; z=1;
50955771:>0:r3=0; 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 63.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test safe165 Allowed
Histogram (13 states)
3046706:>0:r3=2; 2:r3=2; x=2; y=2;
472705:>0:r3=2; 2:r3=2; x=2; y=1;
136071:>0:r3=2; 2:r3=1; x=2; y=1;
516975:>0:r3=1; 2:r3=1; x=1; y=1;
7971581:>0:r3=2; 2:r3=0; x=2; y=1;
12016769:>0:r3=1; 2:r3=2; x=1; y=1;
44058507:>0:r3=1; 2:r3=2; x=1; y=2;
37591829:>0:r3=1; 2:r3=2; x=2; y=2;
62005720:>0:r3=1; 2:r3=1; x=2; y=1;
63616863:>0:r3=1; 2:r3=0; x=1; y=1;
79985062:>0:r3=1; 2:r3=1; x=1; y=2;
34056846:>0:r3=1; 2:r3=2; x=2; y=1;
54524366:>0:r3=1; 2:r3=0; 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=c2358315f3b0a52cdef1288bea12e53f
Cycle=SyncdWR Fre SyncsWR Fre LwSyncdWW Wse
Relax safe165 No
Safe=Fre Wse SyncsWR SyncdWR LwSyncdWW
Time safe165 61.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test safe358 Allowed
Histogram (3 states)
23992815:>0:r3=1; 1:r3=1;
307467559:>0:r3=1; 1:r3=0;
308539626:>0:r3=0; 1:r3=1;
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 73.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 4,1
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe359 Allowed
Histogram (7 states)
395379:>0:r3=1; 1:r3=1; 2:r3=1;
52952014:>0:r3=1; 1:r3=0; 2:r3=0;
53612988:>0:r3=0; 1:r3=1; 2:r3=0;
53323167:>0:r3=0; 1:r3=0; 2:r3=1;
79528921:>0:r3=1; 1:r3=1; 2:r3=0;
80072619:>0:r3=1; 1:r3=0; 2:r3=1;
80114912:>0:r3=0; 1:r3=1; 2:r3=1;
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 77.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 4,0(9)
_litmus_P1_0_: li 30,1
_litmus_P1_1_: stw 30,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe360 Allowed
Histogram (13 states)
101359:>0:r3=1; 1:r3=1; 2:r3=2; y=2;
2677767:>0:r3=0; 1:r3=2; 2:r3=2; y=2;
237641:>0:r3=1; 1:r3=1; 2:r3=1; y=1;
4521668:>0:r3=1; 1:r3=2; 2:r3=1; y=1;
6049506:>0:r3=1; 1:r3=0; 2:r3=2; y=2;
81706 :>0:r3=1; 1:r3=2; 2:r3=2; y=2;
64226058:>0:r3=1; 1:r3=0; 2:r3=1; y=1;
62547247:>0:r3=1; 1:r3=1; 2:r3=1; y=2;
54199590:>0:r3=0; 1:r3=2; 2:r3=1; y=2;
79025956:>0:r3=0; 1:r3=1; 2:r3=1; y=1;
16788330:>0:r3=1; 1:r3=2; 2:r3=1; y=2;
51622259:>0:r3=0; 1:r3=2; 2:r3=1; y=1;
57920913:>0:r3=1; 1:r3=0; 2:r3=1; y=2;
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 64.52
$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 -O -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 -O -pthread"
LITMUSOPTS=
Mon Dec 28 15:45:47 GMT 2009