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