Wed Dec 23 08:49:01 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww000
"DpdR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwsww000 Allowed
Histogram (64 states)
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
10 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
23 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
6 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
16 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
505 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
408 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
1134 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
1818 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1179 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
36 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1448 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1389 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
459 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
666 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
772 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1847 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
6105 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
3731 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1472 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1288 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
8964 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
12262 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
37212 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
21277 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
42482 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
5049 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
102140:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4534 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
97327 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
4672 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
64824 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
58476 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
9683 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
174734:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
34198 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
11805 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
7504 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
178876:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
217623:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
106072:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
140711:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
94238 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1019605:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
72806 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
219375:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
449964:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
130897:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
441077:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
1506025:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
69601 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
349306:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
312796:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
1520022:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2009457:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
168460:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
1321196:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
33496 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1418244:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
5554143:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
1944549:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=80ef54f479052cd359e89f5454d47a1e
Cycle=DpdR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww000 No BCLwSyncsWW
Safe=Fre DpdR
Time bclwsww000 80.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww001
"SyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwsww001 Allowed
Histogram (64 states)
1 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
19 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
21 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
153 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
234 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
25 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
311 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3164 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
482 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
18 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
163 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
962 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
581 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
10236 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
47593 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
6649 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
619 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1096 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3324 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
19794 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
18480 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1238 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1929 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3384 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
477 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
6802 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
12498 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
63986 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
15728 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
26823 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
59496 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
71847 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
24022 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
62558 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
10339 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2608 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
76173 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
488523:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
130135:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
7425 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
372932:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
222383:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
27817 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
685467:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
224247:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
353008:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
181007:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
44048 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
144075:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
115168:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
360767:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
81883 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
49493 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1668646:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2054902:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1892259:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1310999:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1377145:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
5920544:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1733285:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=d7a0afd6c179f60d3613318a78cd4ff1
Cycle=SyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww001 No BCLwSyncsWW
Safe=Fre SyncdRR DpdR
Time bclwsww001 78.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww002
"LwSyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwsww002 Allowed
Histogram (65 states)
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
5 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
17 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
19 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
356 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
18 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
35 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
724 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
981 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
458 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1042 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1404 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2051 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4640 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
770 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1175 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1757 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2049 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2222 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1466 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
9114 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
20243 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
41234 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
7029 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
105469:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
90446 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
10019 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
120029:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
54472 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
126079:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
45686 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
72307 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
76892 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
22092 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1673192:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
167116:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
483776:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
116363:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
199228:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
527883:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10846 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
34493 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
6420 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
138914:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
230575:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
13324 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
10151 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
377093:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
10965 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1209998:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
186376:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
227479:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1774740:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
33924 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1690 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
308774:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1705012:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1755337:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1709902:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
5257426:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1006689:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=2096031f64300d4f53a5cb5973aae462
Cycle=LwSyncdRR Fre LwSyncsWW Rfe DpdR Fre LwSyncsWW Rfe
Relax bclwsww002 No BCLwSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bclwsww002 75.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww003
"DpdW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwsync | li r4,1 ;
lwz r3,0(r4) | li r3,2 | stwx r4,r3,r5 ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P0_0_: li r8,2
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stwx r8,r11,r2
Test bclwsww003 Allowed
Histogram (15 states)
6 :>0:r3=1; 2:r1=1; x=2; y=2;
38 :>0:r3=1; 2:r1=1; x=1; y=2;
9819 :>0:r3=2; 2:r1=1; x=2; y=2;
209676:>0:r3=1; 2:r1=0; x=2; y=2;
260075:>0:r3=2; 2:r1=1; x=1; y=2;
52653 :>0:r3=0; 2:r1=0; x=2; y=2;
269057:>0:r3=1; 2:r1=2; x=1; y=2;
832960:>0:r3=0; 2:r1=2; x=1; y=2;
290268:>0:r3=1; 2:r1=0; x=1; y=2;
542016:>0:r3=0; 2:r1=1; x=1; y=2;
1089766:>0:r3=2; 2:r1=0; x=1; y=2;
6837575:>0:r3=2; 2:r1=2; x=1; y=2;
6131558:>0:r3=2; 2:r1=0; x=2; y=2;
1715528:>0:r3=0; 2:r1=0; x=1; y=2;
1759005:>0:r3=2; 2:r1=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=e3e57d0873074b11a3ff2a904a902fe7
Cycle=DpdW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww003 No BCLwSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bclwsww003 32.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww004
"SyncdRW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P0_0_: li r8,2
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r10,0(r9)
_litmus_P2_1_: sync
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stw r8,0(r2)
Test bclwsww004 Allowed
Histogram (14 states)
32 :>0:r3=1; 2:r1=1; x=1; y=2;
59925 :>0:r3=1; 2:r1=0; x=2; y=2;
11979 :>0:r3=0; 2:r1=0; x=2; y=2;
4776 :>0:r3=2; 2:r1=1; x=2; y=2;
337662:>0:r3=1; 2:r1=2; x=1; y=2;
892323:>0:r3=2; 2:r1=2; x=2; y=2;
262370:>0:r3=2; 2:r1=1; x=1; y=2;
468999:>0:r3=0; 2:r1=1; x=1; y=2;
782245:>0:r3=0; 2:r1=2; x=1; y=2;
5161070:>0:r3=2; 2:r1=0; x=2; y=2;
1747492:>0:r3=0; 2:r1=0; x=1; y=2;
741981:>0:r3=1; 2:r1=0; x=1; y=2;
7806559:>0:r3=2; 2:r1=2; x=1; y=2;
1722587:>0:r3=2; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=674a905165ada38c8ec9e64bb80e09d0
Cycle=SyncdRW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww004 No BCLwSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bclwsww004 32.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww005
"LwSyncdRW Wse SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P0_0_: li r8,2
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r10,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stw r8,0(r2)
Test bclwsww005 Allowed
Histogram (15 states)
5 :>0:r3=1; 2:r1=1; x=2; y=2;
28 :>0:r3=1; 2:r1=1; x=1; y=2;
21032 :>0:r3=0; 2:r1=0; x=2; y=2;
11918 :>0:r3=2; 2:r1=1; x=2; y=2;
188776:>0:r3=2; 2:r1=1; x=1; y=2;
93925 :>0:r3=1; 2:r1=0; x=2; y=2;
293510:>0:r3=1; 2:r1=2; x=1; y=2;
768643:>0:r3=0; 2:r1=2; x=1; y=2;
1624070:>0:r3=2; 2:r1=2; x=2; y=2;
436363:>0:r3=0; 2:r1=1; x=1; y=2;
407364:>0:r3=1; 2:r1=0; x=1; y=2;
1988501:>0:r3=0; 2:r1=0; x=1; y=2;
6734624:>0:r3=2; 2:r1=2; x=1; y=2;
1263322:>0:r3=2; 2:r1=0; x=1; y=2;
6167919:>0:r3=2; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=115e6b5af21fe76663f5d1470d14d311
Cycle=LwSyncdRW Wse SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww005 No BCLwSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bclwsww005 32.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww006
"DpdR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwsync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r6,0(r9)
_litmus_P2_1_: xor r11,r6,r6
_litmus_P2_2_: lwzx r7,r11,r2
Test bclwsww006 Allowed
Histogram (15 states)
11 :>0:r3=1; 2:r1=1; 2:r4=0; y=2;
40 :>0:r3=1; 2:r1=1; 2:r4=1; y=2;
12512 :>0:r3=2; 2:r1=1; 2:r4=0; y=2;
39392 :>0:r3=1; 2:r1=0; 2:r4=0; y=2;
716228:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
274144:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
22816 :>0:r3=0; 2:r1=0; 2:r4=0; y=2;
3336354:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
201896:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
430616:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
1586113:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
1080259:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
6483753:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
5666037:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
149829:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=50e55c58a033380a8ea3e82bcced305e
Cycle=DpdR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww006 No BCLwSyncsWW
Safe=Fre SyncdWR DpdR
Time bclwsww006 30.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww007
"SyncdRR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz r8,0(r2)
Test bclwsww007 Allowed
Histogram (15 states)
5 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
58 :>0:r3=1; 2:r1=1; 2:r3=1; y=2;
5587 :>0:r3=2; 2:r1=1; 2:r3=0; y=2;
12583 :>0:r3=0; 2:r1=0; 2:r3=0; y=2;
638571:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
131989:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
21499 :>0:r3=1; 2:r1=0; 2:r3=0; y=2;
176412:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
1389655:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
256414:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
1035559:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
1292617:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
1788550:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
7272257:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
5978244:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=4f9d61dc3f842cf35a2345b9a3fbe558
Cycle=SyncdRR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww007 No BCLwSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bclwsww007 32.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww008
"LwSyncdRR Fre SyncdWR Fre LwSyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test bclwsww008 Allowed
Histogram (15 states)
15 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
19 :>0:r3=1; 2:r1=1; 2:r3=1; y=2;
12334 :>0:r3=2; 2:r1=1; 2:r3=0; y=2;
258455:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
36729 :>0:r3=1; 2:r1=0; 2:r3=0; y=2;
183302:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
287332:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
778402:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
388762:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
19754 :>0:r3=0; 2:r1=0; 2:r3=0; y=2;
6448071:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
1305140:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
916547:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
5640568:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
3724570:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=dbf7fab4a4b0d4506a0a82b8be671fd7
Cycle=LwSyncdRR Fre SyncdWR Fre LwSyncsWW Rfe
Relax bclwsww008 No BCLwSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bclwsww008 30.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww009
"SyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwsww009 Allowed
Histogram (63 states)
2 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>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=0; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
10 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
33 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
158 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
174 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
225 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
200 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
104 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
368 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
51934 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1139 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
18 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
391 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
7076 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
894 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
14372 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
12473 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
271 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
19385 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
6553 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
13649 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1066 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4243 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5691 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3232 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3999 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
3246 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5522 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
68525 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1483 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
9280 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
82193 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
49045 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
71423 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
416106:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
287275:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
173141:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
89618 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
167940:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
18727 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
197 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
164398:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
65791 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
94727 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
344105:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
218530:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
167878:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
33721 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1750093:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
359661:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
182520:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1883384:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
221398:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1770336:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2099825:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1588622:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1225417:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5840223:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
397979:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=11d5d9947606f505142ba330f1ff6395
Cycle=SyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe
Relax bclwsww009 No BCLwSyncsWW
Safe=Fre SyncdRR
Time bclwsww009 79.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww010
"LwSyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwsww010 Allowed
Histogram (68 states)
1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
38 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
19 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
95 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
90 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
23 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
278 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1364 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
530 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4193 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
446 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1606 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
26 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3425 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1028 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1414 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
415 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
35080 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4285 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
10351 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
8077 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4966 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1215 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
6964 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
6998 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1000 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
80150 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
14272 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1950 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
37798 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
84784 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17473 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
11443 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
88378 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
32898 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
39353 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
198 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
94535 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
163758:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
178251:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
24890 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
682914:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
227724:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
189342:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
53487 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
153003:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
508250:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
26179 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
71722 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2047905:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
641051:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
86649 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
312247:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
416120:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1671214:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1725709:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2303510:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1565849:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5050899:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1302151:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=d688877c8baf57ede314d1afec00160f
Cycle=LwSyncdRR Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe
Relax bclwsww010 No BCLwSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bclwsww010 80.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwsww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwsww011
"LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwsww011 Allowed
Histogram (64 states)
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
16 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
29 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
9 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
6 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
282 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
452 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
428 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
741 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
854 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
765 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
555 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1723 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3701 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1585 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
6351 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1384 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4378 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
3632 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5740 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
956 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1499 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
56248 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
22841 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
67477 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
60427 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
29953 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
125646:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1745 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5572 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
7999 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
395 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
21000 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
65789 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
56634 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
142089:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
7815 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
44805 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
159306:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
10846 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
64409 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
686767:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1735826:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
85812 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
611087:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
158602:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
160596:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
299038:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
47218 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
876185:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
38636 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1979450:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1648969:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
13245 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
155431:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
348739:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2065482:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1446964:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5155682:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1500182:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=773703b01275cf3bc683a284bc8915e5
Cycle=LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe
Relax bclwsww011 No BCLwSyncsWW
Safe=Fre LwSyncdRR
Time bclwsww011 78.08
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Wed Dec 23 09:00:04 CET 2009