Thu Dec 24 23:03:24 CET 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_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz r5,0(r9)
_litmus_P1_4_: xor r11,r5,r5
_litmus_P1_5_: lwzx r6,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz r10,0(r2)
_litmus_P3_0_: li r10,2
_litmus_P3_1_: stw r10,0(r9)
_litmus_P3_2_: lwsync
_litmus_P3_3_: lwz r5,0(r9)
_litmus_P3_4_: xor r11,r5,r5
_litmus_P3_5_: lwzx r6,r11,r2
Test lwswr000 Allowed
Histogram (89 states)
1 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
2 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
1 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
8 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
3 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
40 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
2 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
53 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
73 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
55 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
7 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
10 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
109 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
27 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
6 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
2 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
20 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
123 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
484 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
67 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
45 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
164 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
192 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
471 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
110 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
31 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
69 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
117 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
15 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
680 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
455 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
2366 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
1 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
2008 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
3044 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
2222 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
9762 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
22145 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
1531 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
30217 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
49521 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
61 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
4832 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
140 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
26239 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
3483 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
62229 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
1928 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
242789:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
7930 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
82780 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
24108 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
64447 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
129161:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
115537:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
1245 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
114379:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
48797 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
1216 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
761965:>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
94528 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
423684:>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
22761 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
110580:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
23482 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
228665:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
2205 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
917597:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
182964:>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
547374:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
539494:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
557077:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
30500 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
140612:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
1958446:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
125290:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
386 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
147946:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
1834994:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
575781:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
1002053:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
23257 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
69701 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
975576:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
4530641:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
115585:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
898371:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
1180254:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
920671:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 78.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz r5,0(r9)
_litmus_P0_4_: xor r11,r5,r5
_litmus_P0_5_: lwzx r6,r11,r2
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz r10,0(r2)
_litmus_P2_0_: li r10,2
_litmus_P2_1_: stw r10,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz r5,0(r9)
_litmus_P2_4_: xor r11,r5,r5
_litmus_P2_5_: lwzx r6,r11,r2
Test lwswr001 Allowed
Histogram (18 states)
28 :>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
7 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
45 :>0:r3=1; 0:r5=1; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
6149 :>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
1231 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
1733907:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
1230514:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
141148:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
826598:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
671043:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
394244:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
109848:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
3650671:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
1204263:>0:r3=1; 0:r5=0; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
1549602:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
5897916:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
2507375:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
75411 :>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=1f164e89ea4c9d76bdb41cd7afd883d1
Cycle=DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR
Relax lwswr001 No LwSyncsWR
Safe=Fre DpdR
Time lwswr001 36.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz r5,0(r9)
_litmus_P0_4_: xor r11,r5,r5
_litmus_P0_5_: lwzx r6,r11,r2
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz r5,0(r9)
_litmus_P1_4_: xor r11,r5,r5
_litmus_P1_5_: lwzx r6,r11,r2
Test lwswr002 Allowed
Histogram (4 states)
2 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0;
15269559:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0;
14839562:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1;
9890877:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1;
Ok
Witnesses
Positive: 2, Negative: 39999998
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 22.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz r5,0(r9)
_litmus_P0_4_: xor r11,r5,r5
_litmus_P0_5_: lwzx r6,r11,r2
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz r5,0(r9)
_litmus_P1_4_: xor r11,r5,r5
_litmus_P1_5_: lwzx r6,r11,r2
_litmus_P2_0_: li r10,1
_litmus_P2_1_: stw r10,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz r5,0(r9)
_litmus_P2_4_: xor r11,r5,r5
_litmus_P2_5_: lwzx r6,r11,r2
Test lwswr003 Allowed
Histogram (7 states)
263473:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
233043:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=0;
2214335:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
5759250:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
5605890:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
130993:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
5793016:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0 /\ 2:r3=1 /\ 2:r5=0) is NOT validated
Hash=5ca1b488751415332d4775c3d78fc011
Cycle=DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR DpdR Fre LwSyncsWR
Relax lwswr003 No LwSyncsWR
Safe=Fre DpdR
Time lwswr003 28.97
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Thu Dec 24 23:06:11 CET 2009