Sat Dec 26 16:41:46 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 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_: sync
_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_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww000 Allowed
Histogram (77 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1468 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
2063 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
2823 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3034 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
5823 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
2196 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
10912 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
6822 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
16736 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
7444 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1881 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
101263:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
162841:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
770963:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
43743 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
55551 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
46200 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
102162:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
3183001:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1855987:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
310325:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
771830:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
82965 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
2583786:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
780791:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1886950:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
236401:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2096600:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2688489:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3157690:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
513408:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3717247:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
325502:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1197781:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2991232:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
4039354:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
50523 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
566268:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
136984:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
681170:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
973864:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
3571335:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
171923:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
137865:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
5072243:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
4211171:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1438965:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1697099:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
2096220:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
242895:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
4952083:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3071865:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
1427685:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
20372553:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
1077931:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
4503791:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1939614:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2535852:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2657251:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
20458072:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
750323:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
19049520:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
14700344:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
4397616:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
19225938:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
12185008:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
14654196:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
4862300:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4379626:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
51623287:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
12488127:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
43875223:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=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: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 86.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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_: 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_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww001 Allowed
Histogram (74 states)
1 :>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;
2238 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2346 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1430 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1825 :>1:r1=1; 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;
27660 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
8467 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
47150 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
103349:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2466 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
16040 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
521670:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1142962:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
478674:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
76324 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
170151:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
85496 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
40030 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
903499:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
162913:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
372962:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
818926:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1027268:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
214205:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
594149:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
224365:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
803821:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
281659:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
774219:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
290693:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1022959:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2043011:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2250015:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3705545:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
4172640:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1752392:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2059554:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
5735824:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2946280:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
569170:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
303521:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3254295:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2027936:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
3219571:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
435171:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2329600:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1531477:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1781388:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3589752:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
5813758:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2321661:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2882224:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
5237926:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1257892:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3019349:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
4491897:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
17646732:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
16492661:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2431057:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
5265272:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
18242807:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
13562375:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1304151:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
53626290:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
722556:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
4877313:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
11984704:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
20423399:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
14334643:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
18875672:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
38687143:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2570162:>1:r1=2; 1:r4=0; 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=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 83.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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_: 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_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww002 Allowed
Histogram (75 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>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;
4203 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1393 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1617 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1521 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
8239 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2043 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1567 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
11981 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
11288 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
569419:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
72193 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1143277:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
368165:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
161220:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1087955:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
27472 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
279515:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
283320:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
104302:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
28490 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
731676:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
178387:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1165710:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
64211 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
909060:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
208797:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2016166:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
324523:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2016100:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3391873:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1057381:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
268008:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1099052:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2544005:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1351596:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1913509:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
516495:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
664879:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
398594:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
168802:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2517409:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
293581:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
5349794:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3660928:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2652581:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2663573:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
788773:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4752014:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2002932:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2653041:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1472660:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1683894:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
18973432:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3910169:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2891647:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2893691:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
5097556:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3697791:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
17916548:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
13183915:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
11680217:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5018535:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
4575503:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
4291318:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
5490637:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
13636855:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
20030868:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
19861610:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1812410:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
54455796:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
38722664:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
16209650:>1:r1=2; 1:r4=2; 3:r1=0; 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 84.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww003 Allowed
Histogram (17 states)
3 :>0:r3=1; 2:r1=2; x=2; y=2;
17 :>0:r3=0; 2:r1=1; x=2; y=2;
638457:>0:r3=1; 2:r1=0; x=1; y=2;
322213:>0:r3=1; 2:r1=1; x=2; y=2;
547762:>0:r3=2; 2:r1=0; x=1; y=2;
4343998:>0:r3=2; 2:r1=1; x=1; y=2;
10948079:>0:r3=2; 2:r1=1; x=2; y=2;
4071469:>0:r3=1; 2:r1=1; x=1; y=2;
4995144:>0:r3=1; 2:r1=2; x=1; y=2;
29376586:>0:r3=2; 2:r1=2; x=2; y=2;
21098826:>0:r3=0; 2:r1=1; x=1; y=2;
36789000:>0:r3=0; 2:r1=2; x=1; y=2;
58315447:>0:r3=2; 2:r1=0; x=2; y=2;
17913872:>0:r3=1; 2:r1=0; x=2; y=2;
71313322:>0:r3=0; 2:r1=0; x=1; y=2;
51892060:>0:r3=0; 2:r1=0; x=2; y=2;
87433745:>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 46.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww004 Allowed
Histogram (15 states)
4824619:>0:r3=1; 2:r1=2; x=1; y=2;
151607:>0:r3=1; 2:r1=1; x=2; y=2;
3899736:>0:r3=1; 2:r1=1; x=1; y=2;
7547815:>0:r3=2; 2:r1=1; x=2; y=2;
17109189:>0:r3=1; 2:r1=0; x=2; y=2;
762565:>0:r3=1; 2:r1=0; x=1; y=2;
913095:>0:r3=2; 2:r1=0; x=1; y=2;
89740177:>0:r3=2; 2:r1=2; x=1; y=2;
18450837:>0:r3=0; 2:r1=1; x=1; y=2;
6076600:>0:r3=2; 2:r1=1; x=1; y=2;
62402778:>0:r3=2; 2:r1=0; x=2; y=2;
35805389:>0:r3=0; 2:r1=2; x=1; y=2;
26022950:>0:r3=2; 2:r1=2; x=2; y=2;
42689613:>0:r3=0; 2:r1=0; x=2; y=2;
83603030:>0:r3=0; 2:r1=0; 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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 50.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww005 Allowed
Histogram (16 states)
1 :>0:r3=0; 2:r1=1; x=2; y=2;
436941:>0:r3=1; 2:r1=0; x=1; y=2;
449182:>0:r3=2; 2:r1=0; x=1; y=2;
227040:>0:r3=1; 2:r1=1; x=2; y=2;
17876465:>0:r3=0; 2:r1=1; x=1; y=2;
4328461:>0:r3=1; 2:r1=2; x=1; y=2;
7829736:>0:r3=2; 2:r1=1; x=2; y=2;
5080084:>0:r3=2; 2:r1=1; x=1; y=2;
29891207:>0:r3=2; 2:r1=2; x=2; y=2;
16394805:>0:r3=1; 2:r1=0; x=2; y=2;
3843430:>0:r3=1; 2:r1=1; x=1; y=2;
49506813:>0:r3=0; 2:r1=0; x=2; y=2;
36271606:>0:r3=0; 2:r1=2; x=1; y=2;
78884297:>0:r3=0; 2:r1=0; x=1; y=2;
62973238:>0:r3=2; 2:r1=0; x=2; y=2;
86006694:>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=585ce030a2274090c0b4fa0251d7b3ad
Cycle=LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww005 No BCSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bcssww005 49.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww006 Allowed
Histogram (17 states)
10 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
23 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
408890:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
541870:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
255258:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
9843196:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
17743967:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
2636845:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
35957283:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
34868973:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
66357465:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
6120068:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
15947329:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
3986187:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
74327064:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
48982482:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
82023090:>0:r3=2; 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 49.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww007 Allowed
Histogram (16 states)
1 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
387404:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
730524:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
4746473:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
537992:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
6251095:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
17262873:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
30380396:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
10390313:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
34540112:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
16982976:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
43808209:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
4835622:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
82614591:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
78671480:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
67859939:>0:r3=2; 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 48.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: sync
_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 bcssww008 Allowed
Histogram (17 states)
1 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
6 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
351005:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
540194:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
4676407:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
9339802:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
516880:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
16862339:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
32909545:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
36992939:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
48387184:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
15583657:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
5358128:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
81294823:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
4534609:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
76398556:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
66253925:>0:r3=2; 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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 48.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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 (72 states)
1574 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1325 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1155 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1933 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1581 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
7610 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1234 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
30116 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
46623 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
487826:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
44112 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
373225:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
297936:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
387713:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
289845:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
258639:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
150131:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
361721:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
643996:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
256078:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
246944:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
78611 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1644489:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1752420:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1299092:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1429543:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4930230:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
290816:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1064125:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1269174:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
555651:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
715063:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
832645:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
697186:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2428585:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
866601:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1647921:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4677542:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1037046:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4713380:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
860757:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
208601:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2717599:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
874755:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
147374:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4731243:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
563024:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5205671:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3061425:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4024405:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3085087:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3746648:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2135443:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1656842:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2434698:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
315691:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2184046:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3705651:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2561642:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1441063:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3883069:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
18076038:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5075232:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
17868528:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
20562596:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
14796306:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
14493666:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16326086:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19666872:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
54373639:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
37181619:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16213247:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 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 86.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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 (72 states)
2359 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1705 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1345 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2506 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1601 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1315 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
17199 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
9544 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
27580 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
716871:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
146054:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
138754:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
534033:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
273229:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
40264 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1417843:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1865778:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
238483:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
902879:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
404661:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
915390:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
721905:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
284437:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
279004:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
887985:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
270716:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1867571:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
595196:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
300264:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2224352:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1064340:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5240372:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
409844:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2380415:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
303586:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
376998:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2686595:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1839299:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2731993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3996353:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2241485:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3113622:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
667438:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
273057:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1136421:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
5183257:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3147939:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2205503:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5105837:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
675227:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1330157:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
5110294:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
5018966:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4138828:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
919738:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
16977491:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4050468:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1460882:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
15664761:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17659279:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5038956:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4189950:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1375173:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
14599192:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
20321653:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1791896:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
15361820:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
14825105:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
59292 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
55343406:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
35646319:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19245970:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; 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 86.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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 (73 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2016 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1446 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1348 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1466 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1238 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
8244 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2492 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
632257:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
11360 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
308428:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
45747 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
22297 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
413452:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
380409:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
308956:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
141191:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
710391:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2020675:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
278468:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
273501:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
517981:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1743502:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2398856:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
263611:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1459298:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
22061 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
420490:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
827327:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
584037:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1535099:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2390255:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
300579:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
284156:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
972986:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
5685025:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
772376:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3683726:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3925839:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1384493:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
682117:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2535521:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1597668:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
134952:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1053069:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
14873302:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
648670:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
314249:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1115054:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1311731:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3301807:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4569634:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2621420:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1561043:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5070621:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2192095:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
944776:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
5361423:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1981883:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
14475423:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5027824:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3948534:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17638530:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
15845071:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4474662:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20151372:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19582176:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17905518:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
15646533:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
55701344:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3183774:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
36247856:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3563268:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 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 84.32
$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=-s 100000 -r 400
Sat Dec 26 16:55:14 GMT 2009