Tue Dec 22 19:17:40 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww000
"DpdR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww000 Allowed
Histogram (79 states)
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
13 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
10 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
9 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
7 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
9 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
9 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
495 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
605 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
241 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
230 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
429 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
4407 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1005 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
923 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
2642 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
20115 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
75348 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
6536 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
77920 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
2375 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
12190 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
16179 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
4520 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
186380:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
12511 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
41419 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
13468 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
21923 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
16549 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
161177:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
389531:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
12130 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
1160035:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1303635:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1138185:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1508751:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
101890:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1684967:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
840954:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
1736515:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
395614:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
40191 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
144582:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
119502:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2103210:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
1187833:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
1266024:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
143533:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
810152:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
94178 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
2217316:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1101823:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
117909:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1169650:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2180712:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
472706:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
2247121:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
441699:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
6055229:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
1468811:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
940653:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1118037:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
6296846:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
2282767:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
17993649:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1001985:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
6059083:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
25581926:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
17819313:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
21322594:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
13208409:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2142981:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
21241252:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
25412460:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
12918625:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
50920745:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
6278325:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
53126314:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
Ok
Witnesses
Positive: 7, Negative: 319999993
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0) is validated
Hash=80ef54f479052cd359e89f5454d47a1e
Cycle=DpdR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww000 Ok BCLwSyncsWW
Safe=Fre DpdR
Time bclwsww000 96.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww001
"SyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww001 Allowed
Histogram (78 states)
2 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
6 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
219 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
403 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1284 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
481 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3606 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1062 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
381 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
800 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
16500 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
13744 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
6120 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4656 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
8249 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
31906 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
28196 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
31168 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
136541:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
58549 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
160431:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
231855:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
21926 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
42319 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
26000 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
48620 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
89342 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
9276 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
76422 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
121007:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
96965 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1915609:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
446120:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
336508:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
529823:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1288400:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
297352:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1313467:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1016323:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2257559:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2427147:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1619311:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1209263:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2111328:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
170346:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
331451:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
134699:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
93990 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1826730:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
447612:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
819338:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1245052:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1231476:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
943868:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
5477458:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
626564:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1291811:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1751149:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
5914756:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
17055815:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2019232:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
760127:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
23547043:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3545461:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
13028099:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5070577:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
21381213:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
18022660:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
4757665:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
47627931:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
24638247:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
20309374:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
23695260:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
54198736:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
Ok
Witnesses
Positive: 3, Negative: 319999997
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=d7a0afd6c179f60d3613318a78cd4ff1
Cycle=SyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww001 Ok BCLwSyncsWW
Safe=Fre SyncdRR DpdR
Time bclwsww001 95.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww002
"LwSyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww002 Allowed
Histogram (79 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
6 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
9 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
11 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
12 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
456 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
364 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
234 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2217 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
357 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
678 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1055 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3467 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
24816 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1295 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
4587 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3547 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
87617 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
19644 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
10688 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
17287 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
6758 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
16548 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
34640 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
108557:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
8510 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
48131 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
120991:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
65503 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
326322:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
174887:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
45159 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
535837:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
28581 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
286406:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
101973:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
130027:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
952214:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
336605:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
491653:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
81826 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
95670 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
790147:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1396945:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1249323:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
201323:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1237287:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
897563:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1541253:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1114387:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
994836:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1987318:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1074139:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
874801:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3177535:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
6039955:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1785630:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5644647:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1847284:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
305220:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1832852:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2379400:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1273169:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
13077971:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
448258:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
26025897:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1579631:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
5551678:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
6403955:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
20408380:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
21420933:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
15990029:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
23592036:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
55835095:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
16659939:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
47863076:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
23322957:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
Ok
Witnesses
Positive: 6, Negative: 319999994
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=2096031f64300d4f53a5cb5973aae462
Cycle=LwSyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww002 Ok BCLwSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bclwsww002 97.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww003
"DpdW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwsync | li r4,1 ;
lwz r3,0(r4) | li r3,2 | stwx r4,r3,r5 ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww003 Allowed
Histogram (18 states)
19 :>0:r3=0; 2:r1=2; x=2; y=2;
12 :>0:r3=0; 2:r1=1; x=2; y=2;
820 :>0:r3=1; 2:r1=2; x=2; y=2;
85618 :>0:r3=1; 2:r1=0; x=1; y=2;
469489:>0:r3=2; 2:r1=0; x=1; y=2;
240256:>0:r3=1; 2:r1=1; x=1; y=2;
13991 :>0:r3=1; 2:r1=1; x=2; y=2;
980978:>0:r3=1; 2:r1=2; x=1; y=2;
924146:>0:r3=2; 2:r1=1; x=1; y=2;
8372872:>0:r3=0; 2:r1=1; x=1; y=2;
1818363:>0:r3=2; 2:r1=1; x=2; y=2;
6578552:>0:r3=1; 2:r1=0; x=2; y=2;
50869250:>0:r3=0; 2:r1=0; x=2; y=2;
44742583:>0:r3=2; 2:r1=2; x=2; y=2;
71897511:>0:r3=0; 2:r1=0; x=1; y=2;
72619075:>0:r3=2; 2:r1=0; x=2; y=2;
90563140:>0:r3=2; 2:r1=2; x=1; y=2;
49823325:>0:r3=0; 2:r1=2; x=1; y=2;
Ok
Witnesses
Positive: 19, Negative: 399999981
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is validated
Hash=e3e57d0873074b11a3ff2a904a902fe7
Cycle=DpdW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww003 Ok BCLwSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bclwsww003 78.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww004
"SyncdRW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww004 Allowed
Histogram (15 states)
11238 :>0:r3=1; 2:r1=1; x=2; y=2;
1624620:>0:r3=2; 2:r1=1; x=2; y=2;
833012:>0:r3=1; 2:r1=2; x=1; y=2;
2160708:>0:r3=2; 2:r1=1; x=1; y=2;
405587:>0:r3=1; 2:r1=1; x=1; y=2;
203921:>0:r3=1; 2:r1=0; x=1; y=2;
1647357:>0:r3=2; 2:r1=0; x=1; y=2;
6345016:>0:r3=0; 2:r1=1; x=1; y=2;
40598561:>0:r3=0; 2:r1=0; x=2; y=2;
6118404:>0:r3=1; 2:r1=0; x=2; y=2;
86789470:>0:r3=0; 2:r1=0; x=1; y=2;
37476145:>0:r3=2; 2:r1=2; x=2; y=2;
72632943:>0:r3=2; 2:r1=0; x=2; y=2;
49037238:>0:r3=0; 2:r1=2; x=1; y=2;
94115780:>0:r3=2; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=674a905165ada38c8ec9e64bb80e09d0
Cycle=SyncdRW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww004 No BCLwSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bclwsww004 77.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww005
"LwSyncdRW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww005 Allowed
Histogram (15 states)
15130 :>0:r3=1; 2:r1=1; x=2; y=2;
192594:>0:r3=1; 2:r1=0; x=1; y=2;
888614:>0:r3=1; 2:r1=2; x=1; y=2;
1129940:>0:r3=2; 2:r1=0; x=1; y=2;
458215:>0:r3=1; 2:r1=1; x=1; y=2;
2480328:>0:r3=2; 2:r1=1; x=2; y=2;
2055881:>0:r3=2; 2:r1=1; x=1; y=2;
6761693:>0:r3=0; 2:r1=1; x=1; y=2;
39578434:>0:r3=2; 2:r1=2; x=2; y=2;
48511312:>0:r3=0; 2:r1=0; x=2; y=2;
6326580:>0:r3=1; 2:r1=0; x=2; y=2;
77996692:>0:r3=0; 2:r1=0; x=1; y=2;
91360803:>0:r3=2; 2:r1=2; x=1; y=2;
48263133:>0:r3=0; 2:r1=2; x=1; y=2;
73980651:>0:r3=2; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=115e6b5af21fe76663f5d1470d14d311
Cycle=LwSyncdRW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww005 No BCLwSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bclwsww005 77.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww006
"DpdR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwsync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww006 Allowed
Histogram (18 states)
18 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
68 :>0:r3=0; 2:r1=2; 2:r4=0; y=2;
3946 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
550799:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
33868 :>0:r3=1; 2:r1=1; 2:r4=0; y=2;
1131355:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
52372681:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
100818:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
358349:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
72653914:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
73422883:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
1636000:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
6674965:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
48562712:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
6674853:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
179072:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
83314851:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
52328848:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
Ok
Witnesses
Positive: 68, Negative: 399999932
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0) is validated
Hash=50e55c58a033380a8ea3e82bcced305e
Cycle=DpdR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww006 Ok BCLwSyncsWW
Safe=Fre SyncdWR DpdR
Time bclwsww006 77.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww007
"SyncdRR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww007 Allowed
Histogram (15 states)
14893 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
872533:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
81168 :>0:r3=1; 2:r1=0; 2:r3=1; y=2;
402342:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
409329:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
1693514:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
1711905:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
6119417:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
6119374:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
72965566:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
49643875:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
45982297:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
85668344:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
51859992:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
76455451:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=4f9d61dc3f842cf35a2345b9a3fbe558
Cycle=SyncdRR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww007 No BCLwSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bclwsww007 79.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww008
"LwSyncdRR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bclwsww008 Allowed
Histogram (18 states)
10 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
39 :>0:r3=0; 2:r1=2; 2:r3=0; y=2;
2732 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
30011 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
457571:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
503082:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
95406 :>0:r3=1; 2:r1=0; 2:r3=1; y=2;
1090000:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
1672597:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
2393792:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
6933051:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
6761741:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
84967229:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
73771040:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
76500393:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
51395449:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
46842010:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
46583847:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
Ok
Witnesses
Positive: 39, Negative: 399999961
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is validated
Hash=dbf7fab4a4b0d4506a0a82b8be671fd7
Cycle=LwSyncdRR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww008 Ok BCLwSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bclwsww008 79.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww009
"SyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww009 Allowed
Histogram (72 states)
216 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
235 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
231 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
201 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
674 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
4113 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
13131 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
5199 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
591 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
13582 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
31383 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
175515:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
33787 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
144022:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
182923:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
389076:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
93465 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
104404:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
41971 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
44624 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
97821 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
99613 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
232755:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
86396 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
12896 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
101947:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
187807:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
12807 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
96227 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
627281:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1988892:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
105909:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
124546:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
819197:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1067176:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1064204:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1764719:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2953904:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
389007:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1954208:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
88324 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1957832:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1118323:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
387261:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
380607:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4037135:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1038606:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1272160:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
4575612:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1231707:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
680661:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1074006:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
909419:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1159551:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2492849:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
98195 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2083946:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1815028:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
21215374:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
17393592:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2561834:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3133165:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
21480672:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4160828:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
22684583:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
22773296:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
44466133:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4636898:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17431750:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
21562003:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
21815300:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
53216695:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=11d5d9947606f505142ba330f1ff6395
Cycle=SyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe
Relax bclwsww009 No BCLwSyncsWW
Safe=Fre SyncdRR
Time bclwsww009 93.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww010
"LwSyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww010 Allowed
Histogram (76 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
223 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
186 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
185 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3314 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
228 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9948 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
656 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2505 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
20664 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
178653:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
10497 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
11177 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
623 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
110995:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
42284 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
13604 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
98196 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
84592 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
110472:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
86250 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
89882 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
77228 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
144730:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
307779:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
10085 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
104181:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
201328:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
87037 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
107850:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
80262 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
42966 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1268755:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
173580:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
395149:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
998302:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
319764:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1099524:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1021135:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
117514:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
608032:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1086924:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1100226:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1751073:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
791126:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
784932:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1665114:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2740369:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
382752:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
992380:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4793119:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2411400:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1754175:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2861665:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
5050742:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1734172:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5207167:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1925316:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2340457:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
22687075:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1669586:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4769839:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
767947:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1009634:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
16197721:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
19999805:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
24307439:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20217037:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
22704334:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17488267:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
44798793:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
21506772:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
54462300:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=d688877c8baf57ede314d1afec00160f
Cycle=LwSyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe
Relax bclwsww010 No BCLwSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bclwsww010 95.67
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww011
"LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bclwsww011 Allowed
Histogram (78 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
8 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
75 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
14 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
14 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
180 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
262 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
400 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
819 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1263 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
415 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
953 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
14003 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
9223 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
10159 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
13294 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
9221 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
13789 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
246632:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
217527:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
95775 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
110333:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
46553 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
194610:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
103203:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
101344:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
86988 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
68017 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
46906 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
119296:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1058669:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
719882:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
127846:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1935902:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
12593 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
228182:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1202226:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
119439:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1892962:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
87432 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
930801:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
362475:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2022954:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
404396:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
907771:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1089703:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1207219:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1885042:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
103825:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
747806:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
998111:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
168339:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1177529:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5036842:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
393443:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
946704:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2613943:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
404589:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4958587:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2741248:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2559558:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2889670:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1296729:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
22845981:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
22064964:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5051837:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1919545:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4965665:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19928922:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1946362:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
16334789:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19223512:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16238623:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
23010107:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
43666718:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
22054492:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
56004788:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
Ok
Witnesses
Positive: 1, Negative: 319999999
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=773703b01275cf3bc683a284bc8915e5
Cycle=LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe
Relax bclwsww011 Ok BCLwSyncsWW
Safe=Fre LwSyncdRR
Time bclwsww011 94.49
$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=
Tue Dec 22 19:35:03 GMT 2009