Wed Dec 30 15:21:53 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww000
"DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW 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 ;
sync | lwzx r4,r3,r5 | sync | 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww000 Allowed
Histogram (76 states)
1 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
3 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
4100 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1618 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
6050 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1466 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
3597 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
3662 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
4362 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
3440 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
1420 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
25320 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
89754 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
371124:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
56578 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
9665 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
1366658:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
436111:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
887690:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
674128:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2573238:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
915774:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3537652:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2320828:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
4154155:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
2461152:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3221111:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
4389932:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
3169563:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1459 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
33479 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1392212:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
666343:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2818045:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
100230:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2081832:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
173278:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1394779:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2377760:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3845513:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3435488:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
10465275:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2097266:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1369170:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
138166:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1211094:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
570967:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2074110:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4556897:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
22009 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
34768 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
5182354:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
14452803:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
29356 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
4766638:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4823452:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
19788408:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
84726 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
639366:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3495364:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
75482 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
125833:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1101441:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
2448881:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
14081378:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
4285725:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
10597184:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
2415472:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
19461100:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
38818851:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
19452295:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4607018:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
20250818:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
57465753:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=9fe623fb41a5ce2e4216ef423b67f696
Cycle=DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww000 No BCSyncsWW
Safe=Fre DpdR
Time bcssww000 99.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww001
"SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW 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 ;
sync | lwzx r4,r3,r5 | sync | 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww001 Allowed
Histogram (73 states)
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1483 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2868 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1308 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1173 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1241 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
22115 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
43547 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
7757 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
11952 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
25637 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
16493 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
2379 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
50136 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
260505:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
128999:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
184177:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1054896:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
180951:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2004817:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
94224 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
57661 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1139960:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2159595:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
877567:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2345549:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3071325:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
626165:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3027742:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
17154900:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1189013:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1344678:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
705127:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
920264:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
406000:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
255316:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
453101:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
391906:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
278873:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2324197:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3991471:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
578941:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2383068:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2938866:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
252087:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
4051252:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
851389:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
613534:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
13281142:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1229609:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2010517:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
5189466:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
4178417:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1382824:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
13303608:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10859071:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1972003:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2448559:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
4650868:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3570898:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
18305761:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
3795772:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
35481348:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
19454407:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
18076542:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1744724:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3324710:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
21691333:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
57772863:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4968972:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3604735:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3118798:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
6096845:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 101.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww002
"LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW 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 ;
sync | lwzx r4,r3,r5 | sync | 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww002 Allowed
Histogram (78 states)
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2495 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1302 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1552 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1687 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1031 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
40086 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3113 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
10238 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
17928 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
25507 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
155905:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
628086:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1263843:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
53785 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2170216:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
342570:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
106050:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
819917:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
592108:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
43326 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1121712:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3080543:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1722767:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4123995:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
21442371:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3565717:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2997600:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
12785219:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
531963:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
174190:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
5713280:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3951642:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
13374 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2096676:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3072154:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
219197:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
88479 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
39549 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2010989:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2113217:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
10863434:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
696703:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
862831:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1398160:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
416053:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
376972:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
250935:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
5019098:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1159038:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3456788:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
18579263:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
19859729:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
58802795:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
890928:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2291633:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
4665691:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
4103988:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
12653392:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
243031:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
17982781:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
16800088:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
705209:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3608472:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3230741:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
4998735:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3729089:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1285432:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2592806:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2341848:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1577524:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
35109062:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2302360:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a2812688a109c131b01004a694cfdd81
Cycle=LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww002 No BCSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bcssww002 100.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww003
"DpdW Wse SyncdWR Fre SyncsWW 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 | sync | 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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww003 Allowed
Histogram (17 states)
13 :>0:r3=1; 2:r1=2; x=2; y=2;
30 :>0:r3=0; 2:r1=1; x=2; y=2;
314111:>0:r3=1; 2:r1=0; x=1; y=2;
3451564:>0:r3=1; 2:r1=2; x=1; y=2;
145390:>0:r3=2; 2:r1=0; x=1; y=2;
1878242:>0:r3=1; 2:r1=1; x=1; y=2;
267317:>0:r3=1; 2:r1=1; x=2; y=2;
1709513:>0:r3=2; 2:r1=1; x=1; y=2;
7020795:>0:r3=2; 2:r1=1; x=2; y=2;
17931440:>0:r3=1; 2:r1=0; x=2; y=2;
60279356:>0:r3=2; 2:r1=0; x=2; y=2;
17395699:>0:r3=0; 2:r1=1; x=1; y=2;
33850004:>0:r3=2; 2:r1=2; x=2; y=2;
75766571:>0:r3=0; 2:r1=0; x=1; y=2;
54329399:>0:r3=0; 2:r1=0; x=2; y=2;
37154766:>0:r3=0; 2:r1=2; x=1; y=2;
88505790:>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=316a93ca86d6e131419704cdf84a4e06
Cycle=DpdW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww003 No BCSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bcssww003 62.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww004
"SyncdRW Wse SyncdWR Fre SyncsWW 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 | sync | 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww004 Allowed
Histogram (15 states)
131234:>0:r3=1; 2:r1=1; x=2; y=2;
5991869:>0:r3=2; 2:r1=1; x=2; y=2;
744491:>0:r3=2; 2:r1=0; x=1; y=2;
546810:>0:r3=1; 2:r1=0; x=1; y=2;
3073748:>0:r3=1; 2:r1=2; x=1; y=2;
87233946:>0:r3=0; 2:r1=0; x=1; y=2;
18332498:>0:r3=1; 2:r1=0; x=2; y=2;
2195251:>0:r3=1; 2:r1=1; x=1; y=2;
3792876:>0:r3=2; 2:r1=1; x=1; y=2;
17680870:>0:r3=0; 2:r1=1; x=1; y=2;
91404721:>0:r3=2; 2:r1=2; x=1; y=2;
40910693:>0:r3=0; 2:r1=0; x=2; y=2;
37316718:>0:r3=0; 2:r1=2; x=1; y=2;
29947079:>0:r3=2; 2:r1=2; x=2; y=2;
60697196:>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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 62.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww005
"LwSyncdRW Wse SyncdWR Fre SyncsWW 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 | sync | 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww005 Allowed
Histogram (17 states)
1 :>0:r3=1; 2:r1=2; x=2; y=2;
3 :>0:r3=0; 2:r1=1; x=2; y=2;
697859:>0:r3=1; 2:r1=0; x=1; y=2;
4007625:>0:r3=1; 2:r1=2; x=1; y=2;
155945:>0:r3=1; 2:r1=1; x=2; y=2;
440325:>0:r3=2; 2:r1=0; x=1; y=2;
3852754:>0:r3=2; 2:r1=1; x=1; y=2;
2454495:>0:r3=1; 2:r1=1; x=1; y=2;
7716596:>0:r3=2; 2:r1=1; x=2; y=2;
17661815:>0:r3=1; 2:r1=0; x=2; y=2;
81170594:>0:r3=0; 2:r1=0; x=1; y=2;
15873645:>0:r3=0; 2:r1=1; x=1; y=2;
87750625:>0:r3=2; 2:r1=2; x=1; y=2;
46525110:>0:r3=0; 2:r1=0; x=2; y=2;
36761479:>0:r3=0; 2:r1=2; x=1; y=2;
31746050:>0:r3=2; 2:r1=2; x=2; y=2;
63185079:>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=585ce030a2274090c0b4fa0251d7b3ad
Cycle=LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww005 No BCSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bcssww005 66.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww006
"DpdR Fre SyncdWR Fre SyncsWW 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 | sync | 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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww006 Allowed
Histogram (17 states)
29 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
13 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
220129:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
2185714:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
317153:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
1265007:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
74074 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
17807660:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
16931333:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
838494:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
6660081:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
61333787:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
41540356:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
70037195:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
54043048:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
83576796:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
43169131:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=eea77ff32793e8bed4abb1ad0c914c0d
Cycle=DpdR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww006 No BCSyncsWW
Safe=Fre SyncdWR DpdR
Time bcssww006 65.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww007
"SyncdRR Fre SyncdWR Fre SyncsWW 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 | sync | 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww007 Allowed
Histogram (16 states)
5 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
211456:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
220936:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2510222:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
7328247:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2006797:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
2851817:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
39144806:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
16782930:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
62090949:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
75894790:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
85753624:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
17089219:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
226829:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
36258975:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
51628398:>0:r3=0; 2:r1=0; 2:r3=0; 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=66d340e023bd1d1ae19ed5903eb5d2ea
Cycle=SyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww007 No BCSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bcssww007 63.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww008
"LwSyncdRR Fre SyncdWR Fre SyncsWW 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 | sync | 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 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww008 Allowed
Histogram (17 states)
25 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
28 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
175283:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
214991:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
243867:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
1794811:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
2453917:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
2368425:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
6965386:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
15945770:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
15833740:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
62206725:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
39321348:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
41114176:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
82889306:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
54117415:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
74354787:>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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 64.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww009
"SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW 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 ;
sync | lwz r3,0(r4) | sync | 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_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 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww009 Allowed
Histogram (73 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1552 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2335 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
936 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
908 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8511 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1826 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
58978 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1558 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
70139 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
150741:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
522920:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
331674:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
682521:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
924407:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
660975:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
771527:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1096688:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
858848:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1954875:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2168456:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1215011:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
224027:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
382930:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
335750:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
269679:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1626750:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2293430:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
769438:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1739847:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2557570:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4461625:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4262828:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1163785:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3891430:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
769382:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
325873:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1388719:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2467654:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
13686240:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
153801:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
386356:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
330008:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
247254:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4091902:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4412256:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
853995:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
19512686:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
41673 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
16154953:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
535125:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1111170:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
15959897:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2568061:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
55140 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
6224719:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2183375:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2219738:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4624216:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
6200147:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1345182:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2687490:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4588950:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4616105:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2170649:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
14140971:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2143541:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
17237396:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16786943:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19504977:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2430066:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
32202349:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
58176565:>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=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 98.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww010
"LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW 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 ;
sync | lwz r3,0(r4) | sync | 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_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 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (75 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1330 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1953 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
949 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1970 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1300 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
8885 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1279 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
31666 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
322215:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
51342 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
401496:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
57325 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
135838:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
84110 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
138191:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1124357:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1002328:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
829458:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
270851:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
331814:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
906064:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1957673:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
323792:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
386716:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
898541:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1093113:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
239021:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4060149:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
228829:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
353028:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1826138:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1332833:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2562290:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1269382:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2081721:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2562140:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2967531:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2025682:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6323972:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4368663:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
328445:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
805123:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2192969:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2113978:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1514951:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3912027:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
840175:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
587994:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
785978:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
355402:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
31947837:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1696642:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3808423:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4576207:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2401711:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3987475:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
539179:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4165081:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
13204938:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16184243:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
15756970:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5953243:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2937089:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3666638:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17512424:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
17563374:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1314134:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
14199019:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
59393781:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
20491273:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19708409:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2988930:>1:r1=2; 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=fdf7665f1e0ce0f0c6d4d353ee548d9e
Cycle=LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww010 No BCSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bcssww010 101.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww011
"LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW 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 ;
sync | lwz r3,0(r4) | sync | 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_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 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww011 Allowed
Histogram (77 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
6 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1887 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1217 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
10046 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1153 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1625 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2117 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
30440 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
21616 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2543 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
464723:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
556337:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1276399:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
231673:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
133789:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
300522:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
297543:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
229721:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2350071:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
345477:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
132975:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
865890:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
655671:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
46687 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1392113:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4323916:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
857247:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
291283:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
707480:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4414412:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
362521:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
205758:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1338506:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1917071:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2353662:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
880470:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
696194:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3891857:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1229605:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
830413:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
297311:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
83018 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4183655:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
6014126:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2299844:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2275134:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
853937:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2583531:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1459409:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4315521:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1666025:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4189381:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1802839:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1413557:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2387699:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
13239025:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4487109:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
6007671:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4570299:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2700752:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2601144:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3085588:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
16149788:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
19587296:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
16553658:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
30977070:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
13688286:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
16383102:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
60206890:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
14993101:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3037160:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
19770957:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2483476:>1:r1=0; 1:r3=0; 3:r1=1; 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=7c8f7188794f6e0c8b799c86369a2299
Cycle=LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe
Relax bcssww011 No BCSyncsWW
Safe=Fre LwSyncdRR
Time bcssww011 101.79
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 30 15:38:23 GMT 2009