Thu Dec 31 14:59:24 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 (78 states)
5 :>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;
5 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
7 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
9 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
3219 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
3883 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
6543 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
10013 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
111729:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
2707 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
121192:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
8770 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
11862 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
31185 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
1336539:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3279 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
15077 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
10515 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
211687:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
56989 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
191064:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
391019:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1311939:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
6115190:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
5400690:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4328183:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4897670:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
7851250:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
2955218:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
7030069:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1500051:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
6281672:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
5362776:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4753383:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
269439:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2497716:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1105442:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
5421325:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
84883 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
2154755:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
65958 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
211779:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
128936:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
6276144:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
4034790:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2433946:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
7657268:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
20925344:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4761091:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
2918654:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
8344967:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
7650452:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2298299:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1613631:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
10333172:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
8752819:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
38939997:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
6447824:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2833601:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
284792:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
514808:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
11163421:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
10258008:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
1572620:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
28844821:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
3021846:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
5561479:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
9565948:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
37687458:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
27963524:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
21107741:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
9691984:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
113284773:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
37591734:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
75094964:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
38312455:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 184.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
4 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
4 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
6534 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
5545 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3624 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3520 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
3150 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3121 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
23910 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
30735 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
16036 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
60202 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
511929:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
598300:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
527121:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
475868:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
345844:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
741412:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
81993 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
91255 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
43562 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
293128:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
964983:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2119737:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1953529:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1650127:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
118073:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
172611:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1144060:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2333163:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1156707:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1427947:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
261743:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
10179527:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
7238378:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3718533:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
5907226:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
4404323:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
4328374:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
8139039:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1610171:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3892159:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2405638:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
753411:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
7070095:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
9460223:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5937248:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
8399980:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4383196:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2755470:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1283885:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
7267382:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
9599788:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2445327:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1587786:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
22179517:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
11739947:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4764372:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
36751942:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
6086530:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
26587530:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3963845:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3588908:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5107970:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
8066478:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
72218606:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
36743671:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
114890061:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
43858676:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
26720680:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
6733211:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
39545435:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
6068639:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
34447342:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 190.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
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;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
6 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
5 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3261 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2381 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
5628 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
25701 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
6040 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
18665 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3631 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
74357 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
45443 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
88059 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
119756:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
840329:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
34344 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
481946:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1314176:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
239927:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
479725:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
703435:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
334808:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2421378:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1421012:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
433641:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2993397:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1212262:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1281659:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
642258:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2385220:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3659001:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
7498291:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
5801562:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
4269191:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
7042145:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
6174794:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2973 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
75204 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
11106783:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
5857933:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3964632:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
263872:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
22295011:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1086164:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2182665:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
7547114:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1676000:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
9836814:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
174185:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4307064:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
7199389:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
4641904:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
9605116:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
35523410:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2590117:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2680773:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
8353966:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
8900492:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
33260088:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
25214779:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
39332250:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1742256:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
71480013:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1628471:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
5168621:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
5000145:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
6394329:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
36828667:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
9886454:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
4325984:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
116745077:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4359893:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
8158633:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
42449876:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
26095442:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 186.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
15 :>0:r3=1; 2:r1=2; x=2; y=2;
46 :>0:r3=0; 2:r1=1; x=2; y=2;
605121:>0:r3=1; 2:r1=0; x=1; y=2;
6739999:>0:r3=1; 2:r1=2; x=1; y=2;
292768:>0:r3=2; 2:r1=0; x=1; y=2;
460371:>0:r3=1; 2:r1=1; x=2; y=2;
3321892:>0:r3=1; 2:r1=1; x=1; y=2;
13549944:>0:r3=2; 2:r1=1; x=2; y=2;
2976512:>0:r3=2; 2:r1=1; x=1; y=2;
33617884:>0:r3=0; 2:r1=1; x=1; y=2;
120675145:>0:r3=2; 2:r1=0; x=2; y=2;
35199072:>0:r3=1; 2:r1=0; x=2; y=2;
76082739:>0:r3=0; 2:r1=2; x=1; y=2;
175817839:>0:r3=2; 2:r1=2; x=1; y=2;
108982550:>0:r3=0; 2:r1=0; x=2; y=2;
151294031:>0:r3=0; 2:r1=0; x=1; y=2;
70384072:>0:r3=2; 2:r1=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 118.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
261037:>0:r3=1; 2:r1=1; x=2; y=2;
969248:>0:r3=1; 2:r1=0; x=1; y=2;
6321051:>0:r3=2; 2:r1=1; x=1; y=2;
4094954:>0:r3=1; 2:r1=1; x=1; y=2;
10084813:>0:r3=2; 2:r1=1; x=2; y=2;
1451073:>0:r3=2; 2:r1=0; x=1; y=2;
31813208:>0:r3=0; 2:r1=1; x=1; y=2;
64906321:>0:r3=2; 2:r1=2; x=2; y=2;
32718924:>0:r3=1; 2:r1=0; x=2; y=2;
81208315:>0:r3=0; 2:r1=2; x=1; y=2;
80249455:>0:r3=0; 2:r1=0; x=2; y=2;
5073355:>0:r3=1; 2:r1=2; x=1; y=2;
178148945:>0:r3=0; 2:r1=0; x=1; y=2;
121695218:>0:r3=2; 2:r1=0; x=2; y=2;
181004083:>0:r3=2; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 114.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (15 states)
435526:>0:r3=1; 2:r1=1; x=2; y=2;
4690981:>0:r3=1; 2:r1=1; x=1; y=2;
6004377:>0:r3=1; 2:r1=2; x=1; y=2;
6748294:>0:r3=2; 2:r1=1; x=1; y=2;
12022951:>0:r3=2; 2:r1=1; x=2; y=2;
32435608:>0:r3=0; 2:r1=1; x=1; y=2;
840520:>0:r3=1; 2:r1=0; x=1; y=2;
76272948:>0:r3=0; 2:r1=2; x=1; y=2;
93084426:>0:r3=0; 2:r1=0; x=2; y=2;
34929876:>0:r3=1; 2:r1=0; x=2; y=2;
767912:>0:r3=2; 2:r1=0; x=1; y=2;
176967193:>0:r3=2; 2:r1=2; x=1; y=2;
163060751:>0:r3=0; 2:r1=0; x=1; y=2;
125703284:>0:r3=2; 2:r1=0; x=2; y=2;
66035353:>0:r3=2; 2:r1=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 117.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
85 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
44 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
189694:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
575924:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
538687:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
1986612:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
2751776:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
4992136:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
33532911:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
15071396:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
123147683:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
35138518:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
80017093:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
85547158:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
168803224:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
107270682:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
140436377:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 112.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
714967:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
570422:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
6671633:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
16626554:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
386696:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
5660325:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
32505464:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
4529809:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
33805785:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
101451147:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
70946928:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
153230961:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
124869786:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
170573885:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
77455634:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 111.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
23 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
66 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
433115:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
509126:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
4934505:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
5323453:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
35894504:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
149066330:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
3991211:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
35412055:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
533186:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
121854769:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
76727136:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
13893978:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
106642377:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
77969618:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
166814548:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 114.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
3053 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
3399 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3987 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2131 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2246 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
15234 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
83077 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
120480:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
785646:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
151052:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2234449:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
620476:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1932296:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
512376:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
678751:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1186034:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
464906:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4031383:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
792607:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1465783:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1142409:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1616493:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2304333:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2580183:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2425856:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
727896:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4935260:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3020068:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4474439:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3204986:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3052 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
39977533:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
410434:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
7696347:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
8108906:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1588354:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
9328527:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8877838:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
682744:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
8396663:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
8076372:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
12366211:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
276243:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
766692:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
125583:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
8450599:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4963856:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1515580:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
290886:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
28244799:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
27233543:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1547154:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
617794:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4064409:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
116452740:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
35175689:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
5162827:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
32380842:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2247882:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4717076:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5596416:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3783572:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4460236:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4060172:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2631490:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
12556278:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
8591767:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
32940056:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
39795314:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
34270778:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
64678390:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5367066:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 191.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (76 states)
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;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2983 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3974 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2435 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3086 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4281 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
16441 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2665 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
100750:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
839718:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2012356:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
62279 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
412473:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
90050 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
262538:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
164182:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
598737:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
496888:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1012427:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
261598:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1533507:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
623310:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
605335:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4101929:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
596682:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4148426:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
693382:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1146815:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
676117:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2157543:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
430019:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
7226018:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1800660:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1490692:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1521129:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
7993824:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3133999:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1221146:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
11430584:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1504311:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4248994:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1545117:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4142008:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2499837:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3379469:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
12010728:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
7828130:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2190381:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4057430:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
8259189:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4817678:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2482138:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
8880072:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2655838:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
8258243:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5078604:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
26776534:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
31285996:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5890463:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
8458255:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
8398482:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
39859692:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
65329615:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
118865186:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5811023:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
41165101:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
28656341:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
34826205:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
5769097:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3485190:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
35077860:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5134691:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
32491117:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 193.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (78 states)
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 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=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3540 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
4864 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
3547 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2459 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4707 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
40321 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2597 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
18539 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2307743:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
836663:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
259745:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
691121:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1001007:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
88508 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
156523:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1263370:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
249539:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
433965:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1782991:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1566530:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
588287:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2569068:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2576749:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
717816:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1604216:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1619014:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3540720:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
394437:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
608827:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3238471:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4388549:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
605474:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1516146:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
467695:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5327873:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1197103:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
594936:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4540681:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
8304553:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2553525:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
8525164:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
8135533:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
58957 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
11785991:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2326424:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3473118:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2651886:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5530174:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1541001:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
33846139:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5105519:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
7595740:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4662667:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
40396718:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
8253416:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
8905707:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
32972330:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4317284:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
11746907:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
30286513:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
8580109:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
6199693:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
26811379:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5246155:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
40177482:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
27555758:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
8064446:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
33234313:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
63645219:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
120128298:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
6248977:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4318553:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 189.14
$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=-s 4000
Thu Dec 31 15:29:49 GMT 2009