Tue Dec 29 09:12:08 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 4,10,9
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,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 4,10,9
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww000 Allowed
Histogram (47 states)
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
4 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
27 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
7 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
117 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
51 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
134 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
42 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
53 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
166 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
481 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
93 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
1104 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
3224 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
124 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
101 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
138 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
95 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
24636 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
28707 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
6666 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
206 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
103 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
515 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
10401 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4785784:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
28727 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
873627:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
97 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
45338 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
204 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
71342 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
91 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
936132:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
56793 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
12182 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
456056:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
305667320:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
974758:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
5134408:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
879925:>1:r1=0; 1:r4=0; 3:r1=0; 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 51.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 5,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,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 4,10,9
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww001 Allowed
Histogram (54 states)
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
6 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
7 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
10 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
14 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
6178 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
97 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
23 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
21 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
85 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
143 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1369 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
14906 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2777 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
50 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1303 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
574 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1161 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
68391 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1950 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
121027:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4263 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
821 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
4055 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
64 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
392 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
152284:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
161638:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
134230:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
807117:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1322 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
285781:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1455662:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
37771818:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
567318:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2359313:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2018 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
688472:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
551 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
36078592:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
212609:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
59793412:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
10478 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
192698:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1404935:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
177690054:>1:r1=0; 1:r4=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: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 52.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 5,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,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 4,10,9
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww002 Allowed
Histogram (48 states)
3 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
588 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
94 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
19 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
7 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
485 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
6 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
775 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
791 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
14732 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
99 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
7456 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
273 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2674 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
721 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
430 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
17789 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
10752 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
19396 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
750437:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
887780:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
316023:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
165 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
130 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
269 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
259636:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
8758 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
88 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
708303:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1210856:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2158130:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
555283:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
169116:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
44036777:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
523116:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
21953 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
244552:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
37975588:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
333 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
305642:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1455 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1906110:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
914490:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
34237591:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
192730318:>1:r1=0; 1:r4=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: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 54.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: xor 5,4,4
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,5,9
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww003 Allowed
Histogram (14 states)
14 :>0:r3=1; 2:r1=1; x=1; y=2;
9 :>0:r3=1; 2:r1=0; x=1; y=2;
18 :>0:r3=2; 2:r1=0; x=1; y=2;
11 :>0:r3=2; 2:r1=1; x=1; y=2;
492 :>0:r3=2; 2:r1=1; x=2; y=2;
223473:>0:r3=2; 2:r1=2; x=2; y=2;
240845:>0:r3=1; 2:r1=0; x=2; y=2;
53572247:>0:r3=2; 2:r1=0; x=2; y=2;
340586465:>0:r3=0; 2:r1=0; x=2; y=2;
1315095:>0:r3=0; 2:r1=0; x=1; y=2;
275 :>0:r3=0; 2:r1=1; x=1; y=2;
2008 :>0:r3=1; 2:r1=2; x=1; y=2;
385669:>0:r3=2; 2:r1=2; x=1; y=2;
3673379:>0:r3=0; 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 33.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww004 Allowed
Histogram (15 states)
44 :>0:r3=1; 2:r1=1; x=2; y=2;
2789 :>0:r3=1; 2:r1=1; x=1; y=2;
220798:>0:r3=2; 2:r1=1; x=2; y=2;
6717 :>0:r3=2; 2:r1=1; x=1; y=2;
803 :>0:r3=1; 2:r1=0; x=1; y=2;
52155 :>0:r3=1; 2:r1=2; x=1; y=2;
24643462:>0:r3=2; 2:r1=2; x=2; y=2;
24197533:>0:r3=2; 2:r1=2; x=1; y=2;
3088 :>0:r3=2; 2:r1=0; x=1; y=2;
810390:>0:r3=0; 2:r1=1; x=1; y=2;
50987146:>0:r3=0; 2:r1=2; x=1; y=2;
139627008:>0:r3=0; 2:r1=0; x=1; y=2;
126176142:>0:r3=0; 2:r1=0; x=2; y=2;
386223:>0:r3=1; 2:r1=0; x=2; y=2;
32885702:>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 33.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww005 Allowed
Histogram (15 states)
11 :>0:r3=1; 2:r1=1; x=2; y=2;
1099 :>0:r3=1; 2:r1=1; x=1; y=2;
19852 :>0:r3=2; 2:r1=1; x=1; y=2;
77425 :>0:r3=2; 2:r1=0; x=1; y=2;
918 :>0:r3=1; 2:r1=0; x=1; y=2;
52734508:>0:r3=0; 2:r1=0; x=1; y=2;
578031:>0:r3=0; 2:r1=1; x=1; y=2;
8904 :>0:r3=1; 2:r1=2; x=1; y=2;
3810521:>0:r3=2; 2:r1=2; x=1; y=2;
13391346:>0:r3=0; 2:r1=2; x=1; y=2;
1648357:>0:r3=2; 2:r1=1; x=2; y=2;
11326815:>0:r3=2; 2:r1=2; x=2; y=2;
228267530:>0:r3=0; 2:r1=0; x=2; y=2;
488089:>0:r3=1; 2:r1=0; x=2; y=2;
87646594:>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 32.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 4,10,9
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww006 Allowed
Histogram (15 states)
1 :>0:r3=1; 2:r1=1; 2:r4=0; y=2;
5 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
2 :>0:r3=1; 2:r1=0; 2:r4=1; y=2;
13 :>0:r3=2; 2:r1=1; 2:r4=1; y=2;
24 :>0:r3=1; 2:r1=1; 2:r4=1; y=2;
47703 :>0:r3=0; 2:r1=1; 2:r4=1; y=2;
46982 :>0:r3=2; 2:r1=1; 2:r4=0; y=2;
1483399:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
5518960:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
2099 :>0:r3=1; 2:r1=2; 2:r4=1; y=2;
1115069:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
270934185:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
130579:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
120406923:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
314056:>0:r3=2; 2:r1=2; 2:r4=0; 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 30.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww007 Allowed
Histogram (15 states)
16 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
35 :>0:r3=1; 2:r1=0; 2:r3=1; y=2;
411 :>0:r3=2; 2:r1=1; 2:r3=1; y=2;
120 :>0:r3=2; 2:r1=0; 2:r3=1; y=2;
486 :>0:r3=1; 2:r1=1; 2:r3=1; y=2;
15745 :>0:r3=1; 2:r1=2; 2:r3=1; y=2;
45084054:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
2618204:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
28471705:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
161179954:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
79432 :>0:r3=1; 2:r1=0; 2:r3=0; y=2;
90217554:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
3416997:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
12944848:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
55970439:>0:r3=2; 2:r1=2; 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 29.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test bcssww008 Allowed
Histogram (15 states)
16 :>0:r3=1; 2:r1=0; 2:r3=1; y=2;
69 :>0:r3=2; 2:r1=0; 2:r3=1; y=2;
20 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
192 :>0:r3=1; 2:r1=1; 2:r3=1; y=2;
70 :>0:r3=2; 2:r1=1; 2:r3=1; y=2;
1721827:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
47449811:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
14537 :>0:r3=1; 2:r1=2; 2:r3=1; y=2;
10863021:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
18691671:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
703679:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
29137582:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
76410 :>0:r3=1; 2:r1=0; 2:r3=0; y=2;
81375237:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
209965858:>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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 31.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 5,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 5,0(9)
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww009 Allowed
Histogram (60 states)
7 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
15675 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2645 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
8789 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
10437 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2483 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
7800 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2945 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
321 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
76 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
106704:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
217925:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4052 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
300213:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
399926:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
236623:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
265212:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4977969:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
89184 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
817 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
218 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
321242:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
146540:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
45350 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
446199:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5063671:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
10639861:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
373873:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
341977:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
17101402:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
508035:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1703776:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
17637221:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
86604 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
25380783:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1869449:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
23702118:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
70089 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
17296346:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
411179:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
200073:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5134414:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
259858:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
10137131:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
139169937:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
579743:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
16038604:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
358448:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
11870300:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
324817:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
6130915:>1:r1=2; 1:r3=2; 3:r1=2; 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 56.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 5,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 5,0(9)
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (59 states)
2 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
772 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
308 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
6 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
562 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
905 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
73 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
10946 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
533272:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
160 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
498587:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
613872:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
233 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
525 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
577 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
633851:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
155889:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
683945:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
16123450:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
414937:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
51456 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
129 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
20427 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
18378555:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
198110:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
35364 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
526934:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
9070969:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
170164:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3761875:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
94002 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
21021718:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2670370:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
157128149:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2950790:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
17408685:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
489054:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
315161:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
27068552:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
206217:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3749967:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
9360812:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
128786:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
440 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
14061 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3599 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
5420527:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3298001:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
228401:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
14486258:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
91466 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1978118:>1:r1=0; 1:r3=2; 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: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 56.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 5,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 5,0(9)
_litmus_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww011 Allowed
Histogram (54 states)
1 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
121 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1466 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2934 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
51 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5906 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
12722 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
59 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
11147 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
575 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
109 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
176 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
277195:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
38713 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
72299 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
244688:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
183205:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3266347:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
14559 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
294530:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4151082:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
66879 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
103554:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
289954:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4201923:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
281724:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
210 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
19870044:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
163841:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
140802:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
668089:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2099541:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
18630971:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
402081:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
134312:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3381943:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
26929 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
7263625:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
572372:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17350417:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
486998:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
8082628:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
42545 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
19028323:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
381513:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
8389062:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
523229:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17250776:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
158831468:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1649363:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
21106991:>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=7c8f7188794f6e0c8b799c86369a2299
Cycle=LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe
Relax bcssww011 No BCSyncsWW
Safe=Fre LwSyncdRR
Time bcssww011 53.95
$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: none */
/* 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 100000 -r 400
Tue Dec 29 09:20:47 GMT 2009