Thu Dec 24 10:37:58 NFT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/lwswr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
lwswr000
"DpdR Fre LwSyncsWR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR"
{0:r2=x; 1:r2=x; 1:r6=y; 2:r2=y; 3:r2=y; 3:r6=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync | lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) | lwz r3,0(r2) | lwz r3,0(r2) ;
| xor r4,r3,r3 | | xor r4,r3,r3 ;
| lwzx r5,r4,r6 | | lwzx r5,r4,r6 ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 1:r3=2 /\ 1:r5=0 /\ 2:r3=1 /\ 3:r3=2 /\ 3:r5=0)
Generated assembler
_litmus_P3_0_: li 8,2
_litmus_P3_1_: stw 8,0(11)
_litmus_P3_2_: lwsync
_litmus_P3_3_: lwz 29,0(11)
_litmus_P3_4_: xor 7,29,29
_litmus_P3_5_: lwzx 30,7,9
_litmus_P2_0_: li 10,1
_litmus_P2_1_: stw 10,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 3,0(9)
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 29,0(11)
_litmus_P1_4_: xor 7,29,29
_litmus_P1_5_: lwzx 30,7,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 3,0(9)
Test lwswr000 Allowed
Histogram (112 states)
5 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
1 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
12 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
6 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
1 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
1 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
1 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
28 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
135 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
181 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
5 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
302 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
168 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
26 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
140 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
15 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
13 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
15 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
122 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
27 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
5 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
53 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
6 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
100 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
38 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
10 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
7 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
20 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
22 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
35 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
86 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
173 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
165 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
177 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
159 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
7498 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
383 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
351 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
12274 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
334 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
2084 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
216 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
2175 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
2483 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
2022 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
9406 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
425 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
1029 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
8983 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
1481 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
115 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
2343 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
12293 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
1516 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
1180 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
1999 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
350 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
13253 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
221 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
18067 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
50 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
12933 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
2919 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
15392 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
11443 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
2114 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
14498 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
38083 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
14505 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
15354 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
16077 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
1679 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
37940 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
15548 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
5958 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
36688 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
6227 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
35998 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
149920:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
9615 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
11318 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
179823:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
16355 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
381159:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
16598 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
17268 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
168519:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
7602 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
397378:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
14860 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
967377:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
158372:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
30842 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
276926:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
856530:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
428928:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
36162 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
1020348:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
667980:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
387838:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
808887:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
13125 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
155572:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
273529:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
1246331:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
361929:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
1531351:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
1067622:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
366053:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
828604:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
1689405:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
1067727:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 1:r3=2 /\ 1:r5=0 /\ 2:r3=1 /\ 3:r3=2 /\ 3:r5=0) is NOT validated
Hash=1fbd38850924063f409902cde5f1503b
Cycle=DpdR Fre LwSyncsWR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR
Relax lwswr000 No LwSyncsWR
Safe=Fre DpdR
Time lwswr000 2.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/lwswr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
lwswr001
"DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r6=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) ;
lwsync | lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | | xor r4,r3,r3 ;
lwzx r5,r4,r6 | | lwzx r5,r4,r6 ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 27,0(11)
_litmus_P2_4_: xor 7,27,27
_litmus_P2_5_: lwzx 29,7,9
_litmus_P1_0_: li 10,1
_litmus_P1_1_: stw 10,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 31,0(9)
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 7,27,27
_litmus_P0_5_: lwzx 29,7,9
Test lwswr001 Allowed
Histogram (24 states)
1 :>0:r3=1; 0:r5=0; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
5 :>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
1 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
6 :>0:r3=1; 0:r5=1; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
85 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
17 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
61606 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
14880 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
2224 :>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
996 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
131841:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
1919 :>0:r3=1; 0:r5=1; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
70540 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
390860:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
82438 :>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
11343 :>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
1763988:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
2997863:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
96879 :>0:r3=1; 0:r5=0; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
3328181:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
4626283:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
2777605:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
2617021:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
2023418:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
Ok
Witnesses
Positive: 17, Negative: 20999983
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 2:r3=2 /\ 2:r5=0) is validated
Hash=1f164e89ea4c9d76bdb41cd7afd883d1
Cycle=DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR
Relax lwswr001 Ok LwSyncsWR
Safe=Fre DpdR
Time lwswr001 2.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/lwswr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
lwswr002
"DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 29,0(11)
_litmus_P1_4_: xor 7,29,29
_litmus_P1_5_: lwzx 30,7,9
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 7,29,29
_litmus_P0_5_: lwzx 30,7,9
Test lwswr002 Allowed
Histogram (4 states)
385 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0;
1600601:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1;
15189021:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1;
15209993:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0;
Ok
Witnesses
Positive: 385, Negative: 31999615
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0) is validated
Hash=59460c908e3d6c81f3782b96886e012b
Cycle=DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR
Relax lwswr002 Ok LwSyncsWR
Safe=Fre DpdR
Time lwswr002 1.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/lwswr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
lwswr003
"DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=z; 2:r2=z; 2:r6=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) ;
lwsync | lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0 /\ 2:r3=1 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 27,0(11)
_litmus_P2_4_: xor 7,27,27
_litmus_P2_5_: lwzx 29,7,9
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 27,0(11)
_litmus_P1_4_: xor 7,27,27
_litmus_P1_5_: lwzx 29,7,9
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 7,27,27
_litmus_P0_5_: lwzx 29,7,9
Test lwswr003 Allowed
Histogram (8 states)
5 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=0;
2361332:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
4767423:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
124938:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
2245028:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
2320488:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=0;
4569619:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
4611167:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
Ok
Witnesses
Positive: 5, Negative: 20999995
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0 /\ 2:r3=1 /\ 2:r5=0) is validated
Hash=5ca1b488751415332d4775c3d78fc011
Cycle=DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR
Relax lwswr003 Ok LwSyncsWR
Safe=Fre DpdR
Time lwswr003 2.36
$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=
Thu Dec 24 10:38:09 NFT 2009