Thu Dec 24 09:39:14 GMT 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 10,2
_litmus_P3_1_: stw 10,0(11)
_litmus_P3_2_: lwsync
_litmus_P3_3_: lwz 30,0(11)
_litmus_P3_4_: xor 8,30,30
_litmus_P3_5_: lwzx 31,8,9
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 6,0(9)
_litmus_P1_0_: li 10,2
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 30,0(11)
_litmus_P1_4_: xor 8,30,30
_litmus_P1_5_: lwzx 31,8,9
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 5,0(9)
Test lwswr000 Allowed
Histogram (130 states)
32 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
13 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
6 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
4 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
30 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
9 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
2 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
77 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
3 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
22 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
10 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
15 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
80 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
6 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
33 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
26 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
428 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
30 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
851 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
387 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
137 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
895 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
292 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
455 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
31 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
20 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
76 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
33 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
524 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
36855 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
1568 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
321 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
2109 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
205 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
1174 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
208 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
1980 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
1217 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
1115 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
28707 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
38234 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
28411 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
22885 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
27367 :>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
251706:>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
18736 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
2059 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
2526 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
33446 :>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
476853:>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
397374:>0:r3=1; 1:r3=1; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
459 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
1873 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
312770:>0:r3=2; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
191 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
716 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
226282:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=1; y=2;
302110:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=0; x=2; y=2;
466311:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=2; y=1;
453 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
1978 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
396098:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=0; x=1; y=1;
2061 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
21588 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
12603 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
60778 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
14096 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
16513 :>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
50017 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
45235 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
155853:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
14719 :>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
57469 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
23946 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
43120 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
56676 :>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
45126 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
62165 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
11828 :>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
8144 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
8291 :>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
955896:>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
2750332:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
156563:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
781747:>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
691889:>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
792281:>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
800444:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
824496:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=1; x=2; y=2;
44254 :>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
837068:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=1; x=2; y=1;
752039:>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
744797:>0:r3=1; 1:r3=1; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
940772:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
898147:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=2; x=1; y=2;
2311 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
2143103:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=2; 3:r3=2; 3:r5=1; x=1; y=2;
891241:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=2; x=1; y=1;
2214586:>0:r3=1; 1:r3=1; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
3044867:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
848518:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=1; 3:r5=2; x=2; y=1;
1007883:>0:r3=2; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
4169569:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
53842 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
11638 :>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
5593581:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=2;
941700:>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
5803893:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
3961584:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
2355816:>0:r3=2; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
7462588:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
3064925:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
699677:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=2; 3:r3=2; 3:r5=2; x=2; y=2;
2941385:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
2709362:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=2;
14624725:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
6618188:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
32271623:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
19769606:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
2363756:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=1; 3:r5=1; x=1; y=1;
18421191:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=1; y=1;
16891431:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=1;
6607116:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=2;
18446382:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=1;
17049968:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=1; x=1; y=2;
28318270:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=2;
31988764:>0:r3=1; 1:r3=2; 1:r5=1; 2:r3=1; 3:r3=2; 3:r5=0; x=2; y=1;
18970139:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=1; x=2; y=2;
7441417:>0:r3=1; 1:r3=2; 1:r5=2; 2:r3=1; 3:r3=2; 3:r5=2; x=2; y=1;
14525578:>0:r3=1; 1:r3=2; 1:r5=0; 2:r3=1; 3:r3=2; 3:r5=2; x=1; y=1;
Ok
Witnesses
Positive: 137, Negative: 319999863
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 validated
Hash=1fbd38850924063f409902cde5f1503b
Cycle=DpdR Fre LwSyncsWR Fre LwSyncsWR DpdR Fre LwSyncsWR Fre LwSyncsWR
Relax lwswr000 Ok LwSyncsWR
Safe=Fre DpdR
Time lwswr000 138.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 10,2
_litmus_P2_1_: stw 10,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 30,0(11)
_litmus_P2_4_: xor 8,30,30
_litmus_P2_5_: lwzx 31,8,9
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
Test lwswr001 Allowed
Histogram (24 states)
3 :>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
36 :>0:r3=1; 0:r5=1; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
156 :>0:r3=1; 0:r5=0; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
135 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
2219 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
757 :>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
16838 :>0:r3=1; 0:r5=1; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
12914 :>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
2209099:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=0; y=1;
41729 :>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
266572:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
114314:>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
2032710:>0:r3=1; 0:r5=2; 1:r3=2; 2:r3=2; 2:r5=0; y=2;
7356158:>0:r3=1; 0:r5=0; 1:r3=2; 2:r3=2; 2:r5=1; y=2;
9457790:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
165442:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
8234976:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=1; 2:r5=1; y=1;
54638807:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
40187365:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
41658806:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=2;
89724695:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
54567747:>0:r3=1; 0:r5=1; 1:r3=1; 2:r3=2; 2:r5=1; y=2;
53898184:>0:r3=1; 0:r5=0; 1:r3=1; 2:r3=2; 2:r5=1; y=1;
35412548:>0:r3=1; 0:r5=2; 1:r3=1; 2:r3=2; 2:r5=0; y=1;
Ok
Witnesses
Positive: 757, Negative: 399999243
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 82.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 10,1
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 30,0(11)
_litmus_P1_4_: xor 8,30,30
_litmus_P1_5_: lwzx 31,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
Test lwswr002 Allowed
Histogram (4 states)
243423:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0;
5001385:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1;
317172807:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0;
317582385:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1;
Ok
Witnesses
Positive: 243423, Negative: 639756577
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 76.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 10,1
_litmus_P2_1_: stw 10,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: lwz 30,0(11)
_litmus_P2_4_: xor 8,30,30
_litmus_P2_5_: lwzx 31,8,9
_litmus_P1_0_: li 10,1
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: lwz 30,0(11)
_litmus_P1_4_: xor 8,30,30
_litmus_P1_5_: lwzx 31,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
Test lwswr003 Allowed
Histogram (8 states)
944 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=0;
913482:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
92564469:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
91653927:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=1;
40799900:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=0;
40554774:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1; 2:r3=1; 2:r5=0;
41293545:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
92218959:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0; 2:r3=1; 2:r5=1;
Ok
Witnesses
Positive: 944, Negative: 399999056
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 78.59
$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: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Thu Dec 24 09:45:30 GMT 2009