Wed Dec 23 18:59:00 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww000
"DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
Test bclwdww000 Allowed
Histogram (3 states)
408049:>1:r1=0; x=1;
623830:>1:r1=1; x=1;
968121:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 2000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=c704ed5593f60a49b6fe2873fbc99877
Cycle=DpdW Wse LwSyncdWW Rfe
Relax bclwdww000 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww000 1.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww001
"DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: li r8,1
_litmus_P3_3_: stwx r8,r11,r2
Test bclwdww001 Allowed
Histogram (15 states)
51 :>1:r1=1; 3:r1=1; x=1; z=2;
146 :>1:r1=0; 3:r1=1; x=2; z=2;
371 :>1:r1=1; 3:r1=0; x=2; z=2;
56 :>1:r1=1; 3:r1=1; x=2; z=1;
2439 :>1:r1=0; 3:r1=1; x=1; z=2;
5301 :>1:r1=1; 3:r1=0; x=1; z=2;
21838 :>1:r1=0; 3:r1=1; x=2; z=1;
32569 :>1:r1=1; 3:r1=0; x=2; z=1;
140742:>1:r1=0; 3:r1=0; x=2; z=2;
160348:>1:r1=0; 3:r1=0; x=1; z=2;
192287:>1:r1=1; 3:r1=0; x=1; z=1;
56487 :>1:r1=0; 3:r1=0; x=1; z=1;
184814:>1:r1=0; 3:r1=0; x=2; z=1;
30934 :>1:r1=1; 3:r1=1; x=1; z=1;
171617:>1:r1=0; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d6ca5faa9797f1b1addda6b4fc107253
Cycle=DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww001 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww001 2.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww002
"LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | li r3,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r10,1
_litmus_P3_3_: stw r10,0(r2)
Test bclwdww002 Allowed
Histogram (15 states)
11 :>1:r1=1; 3:r1=1; x=1; z=2;
63 :>1:r1=1; 3:r1=0; x=2; z=2;
58 :>1:r1=1; 3:r1=1; x=2; z=1;
562 :>1:r1=0; 3:r1=1; x=2; z=2;
31890 :>1:r1=0; 3:r1=1; x=2; z=1;
10864 :>1:r1=1; 3:r1=0; x=1; z=2;
120154:>1:r1=0; 3:r1=0; x=2; z=2;
13142 :>1:r1=1; 3:r1=0; x=2; z=1;
153793:>1:r1=0; 3:r1=1; x=1; z=1;
39253 :>1:r1=0; 3:r1=1; x=1; z=2;
213924:>1:r1=0; 3:r1=0; x=2; z=1;
47856 :>1:r1=0; 3:r1=0; x=1; z=1;
141918:>1:r1=0; 3:r1=0; x=1; z=2;
82244 :>1:r1=1; 3:r1=1; x=1; z=1;
144268:>1:r1=1; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=f222837c1b9c320fc4731d82df04c0c8
Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww002 No BCLwSyncdWW
Safe=Wse LwSyncdRW DpdW
Time bclwdww002 2.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww003
"DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww003 Allowed
Histogram (15 states)
136 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
237 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
252 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
7403 :>1:r1=1; 3:r1=0; 3:r4=1; z=2;
332 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
4150 :>1:r1=0; 3:r1=1; 3:r4=1; z=2;
12256 :>1:r1=0; 3:r1=1; 3:r4=0; z=1;
6124 :>1:r1=1; 3:r1=0; 3:r4=0; z=1;
184688:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
149667:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
79711 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
199456:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
173849:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
48215 :>1:r1=1; 3:r1=1; 3:r4=1; z=1;
133524:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=13e9eff5346eb465cffd68e7d2363168
Cycle=DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww003 No BCLwSyncdWW
Safe=Fre Wse DpdW DpdR
Time bclwdww003 2.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww004
"DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww004 Allowed
Histogram (39 states)
1 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
1 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
4 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
7 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
3 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
12 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
10 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
26 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
60 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
81 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
66 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
23 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
70 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
116 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
79 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
67 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
484 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
70 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
149 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
1358 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
3159 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
4925 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
10777 :>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
25330 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
6086 :>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
13117 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
21188 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
29559 :>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
80676 :>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
32013 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
80688 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
183618:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
80739 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
66467 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
205866:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
136919:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
16172 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
13 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=819caebc895b4fb2e9c9cb702b8483e8
Cycle=DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww004 No BCLwSyncdWW
Safe=Fre Wse DpsR DpdW
Time bclwdww004 2.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww005
"LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww005 Allowed
Histogram (15 states)
25 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
31 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
70 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
232 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
16002 :>1:r1=1; 3:r1=0; 3:r3=1; z=2;
45980 :>1:r1=1; 3:r1=0; 3:r3=0; z=1;
16643 :>1:r1=0; 3:r1=1; 3:r3=0; z=1;
129168:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
164613:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
13387 :>1:r1=0; 3:r1=1; 3:r3=1; z=2;
162467:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
175712:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
68165 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
51262 :>1:r1=1; 3:r1=1; 3:r3=1; z=1;
156243:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1b7673dab67cdeed3a93a9f78642c123
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww005 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRR DpdW
Time bclwdww005 2.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww006
"LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | lwz r3,0(r2) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww006 Allowed
Histogram (40 states)
2 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
4 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
3 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
17 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
11 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
19 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
242 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
66 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
410 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
68 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1311 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
925 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
378 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
902 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
2498 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
1030 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
2242 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
92 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
408 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1635 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
848 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
9428 :>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
227 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
15845 :>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
3039 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
4665 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
5913 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
31124 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
16966 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
126970:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
80873 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
163472:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
94624 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
46251 :>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
57853 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
25864 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
141870:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
116570:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
44525 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
810 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=355c23adb39c4f8a03f27206e6d5ad02
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww006 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR DpdW
Time bclwdww006 2.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww007
"DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | li r4,1 ;
li r3,1 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_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 bclwdww007 Allowed
Histogram (7 states)
2790 :>2:r1=1; x=2; y=1;
1707 :>2:r1=1; x=1; y=2;
11728 :>2:r1=0; x=2; y=2;
307681:>2:r1=0; x=1; y=2;
90716 :>2:r1=0; x=1; y=1;
278220:>2:r1=1; x=1; y=1;
307158:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=c71f30898deb2fe2dc12be48ca126717
Cycle=DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww007 No BCLwSyncdWW
Safe=Wse LwSyncdWW DpdW
Time bclwdww007 1.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww008
"LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | li r3,1 ;
li r3,1 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_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 bclwdww008 Allowed
Histogram (7 states)
2927 :>2:r1=1; x=2; y=1;
14582 :>2:r1=0; x=2; y=2;
313527:>2:r1=0; x=1; y=2;
294833:>2:r1=0; x=2; y=1;
267663:>2:r1=1; x=1; y=1;
1254 :>2:r1=1; x=1; y=2;
105214:>2:r1=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=82e869524c51deb209a9e10f0c829a0c
Cycle=LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww008 No BCLwSyncdWW
Safe=Wse LwSyncdWW LwSyncdRW
Time bclwdww008 1.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww009
"DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | lwzx r4,r3,r5 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_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 bclwdww009 Allowed
Histogram (7 states)
5519 :>2:r1=1; 2:r4=0; y=1;
19282 :>2:r1=0; 2:r4=0; y=2;
299486:>2:r1=0; 2:r4=1; y=2;
315688:>2:r1=0; 2:r4=0; y=1;
274230:>2:r1=1; 2:r4=1; y=1;
1606 :>2:r1=1; 2:r4=1; y=2;
84189 :>2:r1=0; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=2e3c762333e6fd2b122415c163d1229a
Cycle=DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww009 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpdR
Time bclwdww009 1.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww010
"DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | lwzx r4,r3,r2 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r2)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: lwzx r9,r11,r2
Test bclwdww010 Allowed
Histogram (18 states)
61 :>2:r1=2; 2:r4=1; x=2; y=1;
16 :>2:r1=0; 2:r4=2; x=2; y=1;
1 :>2:r1=0; 2:r4=1; x=2; y=1;
49 :>2:r1=0; 2:r4=1; x=1; y=2;
126 :>2:r1=0; 2:r4=1; x=1; y=1;
861 :>2:r1=1; 2:r4=2; x=1; y=2;
334 :>2:r1=2; 2:r4=1; x=1; y=1;
86 :>2:r1=0; 2:r4=2; x=1; y=2;
16935 :>2:r1=0; 2:r4=0; x=2; y=1;
28613 :>2:r1=1; 2:r4=1; x=1; y=1;
282137:>2:r1=2; 2:r4=2; x=2; y=1;
54691 :>2:r1=0; 2:r4=0; x=1; y=2;
123666:>2:r1=1; 2:r4=1; x=1; y=2;
65541 :>2:r1=2; 2:r4=2; x=1; y=1;
291402:>2:r1=0; 2:r4=0; x=1; y=1;
133494:>2:r1=2; 2:r4=2; x=1; y=2;
1913 :>2:r1=1; 2:r4=1; x=2; y=1;
74 :>2:r1=0; 2:r4=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3b6264a86335c33f3b93e442e8f4ad38
Cycle=DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww010 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpsR
Time bclwdww010 1.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww011
"LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_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 bclwdww011 Allowed
Histogram (7 states)
13187 :>2:r1=0; 2:r3=0; y=2;
7075 :>2:r1=1; 2:r3=0; y=1;
100340:>2:r1=0; 2:r3=1; y=1;
317770:>2:r1=0; 2:r3=0; y=1;
266967:>2:r1=1; 2:r3=1; y=1;
1356 :>2:r1=1; 2:r3=1; y=2;
293305:>2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=cf3c12d91d4069a3e06aed8f569c6ba5
Cycle=LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww011 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW LwSyncdRR
Time bclwdww011 1.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww012
"LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r8,0(r2)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r9,0(r2)
Test bclwdww012 Allowed
Histogram (18 states)
6 :>2:r1=0; 2:r3=1; x=2; y=1;
38 :>2:r1=0; 2:r3=2; x=2; y=1;
95 :>2:r1=1; 2:r3=2; x=1; y=2;
129 :>2:r1=2; 2:r3=1; x=2; y=1;
109 :>2:r1=2; 2:r3=1; x=1; y=1;
2989 :>2:r1=0; 2:r3=2; x=1; y=2;
3321 :>2:r1=0; 2:r3=1; x=1; y=1;
459 :>2:r1=0; 2:r3=1; x=1; y=2;
1261 :>2:r1=1; 2:r3=1; x=2; y=1;
106557:>2:r1=1; 2:r3=1; x=1; y=2;
16571 :>2:r1=0; 2:r3=0; x=2; y=1;
61986 :>2:r1=2; 2:r3=2; x=1; y=1;
76594 :>2:r1=0; 2:r3=0; x=1; y=2;
279954:>2:r1=2; 2:r3=2; x=2; y=1;
302237:>2:r1=0; 2:r3=0; x=1; y=1;
123014:>2:r1=2; 2:r3=2; x=1; y=2;
23368 :>2:r1=1; 2:r3=1; x=1; y=1;
1312 :>2:r1=0; 2:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=e7d627c7adc87ac2502ce1f2b46f87c5
Cycle=LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww012 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdWW
Time bclwdww012 1.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww013
"LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | li r3,1 ;
li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
Test bclwdww013 Allowed
Histogram (3 states)
606767:>1:r1=1; x=1;
842839:>1:r1=0; x=2;
550394:>1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 2000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=4d1c1648955365c08b4c97b22a8d5408
Cycle=LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww013 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww013 1.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww014
"LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | li r3,1 ;
li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r10,1
_litmus_P3_3_: stw r10,0(r2)
Test bclwdww014 Allowed
Histogram (15 states)
72 :>1:r1=1; 3:r1=0; x=2; z=2;
84 :>1:r1=0; 3:r1=1; x=2; z=2;
42 :>1:r1=1; 3:r1=1; x=2; z=1;
50 :>1:r1=1; 3:r1=1; x=1; z=2;
9527 :>1:r1=1; 3:r1=0; x=2; z=1;
3898 :>1:r1=1; 3:r1=0; x=1; z=2;
1740 :>1:r1=0; 3:r1=1; x=1; z=2;
17768 :>1:r1=0; 3:r1=1; x=2; z=1;
135383:>1:r1=0; 3:r1=0; x=2; z=2;
78441 :>1:r1=0; 3:r1=0; x=1; z=1;
172539:>1:r1=0; 3:r1=0; x=1; z=2;
189595:>1:r1=0; 3:r1=0; x=2; z=1;
178454:>1:r1=1; 3:r1=0; x=1; z=1;
30123 :>1:r1=1; 3:r1=1; x=1; z=1;
182284:>1:r1=0; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d40b4d76f7e7419bc76f118bb3639055
Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww014 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww014 2.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww015
"DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww015 Allowed
Histogram (15 states)
62 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
75 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
50 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
54 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
11252 :>1:r1=1; 3:r1=0; 3:r4=1; z=2;
11550 :>1:r1=0; 3:r1=1; 3:r4=1; z=2;
11681 :>1:r1=0; 3:r1=1; 3:r4=0; z=1;
85369 :>1:r1=0; 3:r1=0; 3:r4=0; z=2;
127371:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
59671 :>1:r1=1; 3:r1=0; 3:r4=0; z=1;
46239 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
190238:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
166942:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
121353:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
168093:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 2.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww016
"DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww016 Allowed
Histogram (32 states)
1 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
1 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
23 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
10 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
23 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
5 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
17 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
3 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
28 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
113 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
465 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
38 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
562 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
346 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
14863 :>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
763 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
1447 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
13964 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
18630 :>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
54571 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
9357 :>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
74149 :>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
81576 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
93120 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
24843 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
82482 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
43399 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
154590:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
139520:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
29433 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
161657:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=cda2e0cac993408d5ce399f8c3bf25da
Cycle=DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww016 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpsR
Time bclwdww016 2.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww017
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww017 Allowed
Histogram (15 states)
51 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
52 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
184 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
233 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
8391 :>1:r1=0; 3:r1=1; 3:r3=1; z=2;
5609 :>1:r1=1; 3:r1=0; 3:r3=1; z=2;
12887 :>1:r1=0; 3:r1=1; 3:r3=0; z=1;
28553 :>1:r1=1; 3:r1=0; 3:r3=0; z=1;
142737:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
74416 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
187852:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
178093:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
112670:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
70828 :>1:r1=1; 3:r1=1; 3:r3=1; z=1;
177444:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=bc3782a4ff957f30ebb76bfb73a82170
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww017 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW LwSyncdRR
Time bclwdww017 2.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww018
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r2) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww018 Allowed
Histogram (39 states)
3 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
9 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
28 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
191 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
158 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
5 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
5 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
84 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1099 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
596 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
149 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1143 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
2961 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
234 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
3 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
572 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
314 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
70 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
407 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
315 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
480 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
3411 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
2067 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
20815 :>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
11152 :>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
67257 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
5979 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
7781 :>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
917 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
20967 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
68525 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
28463 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
139179:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
156584:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
85600 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
164124:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
35279 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
133534:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
39540 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=090f9e7edaad20d00811f89adff27ed2
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww018 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdRW
Time bclwdww018 3.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww019
"DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
Test bclwdww019 Allowed
Histogram (3 states)
392778:>1:r1=0; 1:r4=1;
910520:>1:r1=0; 1:r4=0;
696702:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 2000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=76deedad5ea71bc51dc86d1d5214c15b
Cycle=DpdR Fre LwSyncdWW Rfe
Relax bclwdww019 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww019 1.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww020
"DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 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,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,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 r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww020 Allowed
Histogram (15 states)
322 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
701 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
293 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
260 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
14356 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
6213 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
3590 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
19287 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
176801:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
170651:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
171055:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
67663 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
157554:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
156987:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
54267 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=95bd88b4aecb95238880fff470fdbcc8
Cycle=DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww020 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww020 2.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww021
"DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | 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,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,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 r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww021 Allowed
Histogram (35 states)
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
5 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
15 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
33 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
10 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
16 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
5 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
110 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
10 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
42 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
63 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
119 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
99 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
959 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
196 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
4681 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
113 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
22052 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
5146 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
27371 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
2335 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
32324 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
9619 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
181459:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
87136 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
68108 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
81044 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
124511:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
67223 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
31152 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
170483:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
40922 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
28426 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
14210 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26c4ea0f855245b74a15911ba593704d
Cycle=DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww021 No BCLwSyncdWW
Safe=Fre DpsR DpdR
Time bclwdww021 2.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww022
"LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 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,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,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 r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww022 Allowed
Histogram (15 states)
77 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
267 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
714 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
81 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
11699 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
3429 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
16462 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
165107:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
149714:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
208657:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
207159:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
76187 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
64857 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
18005 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
77585 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=18c468c9529c924b0b9eadcf19d0bf8c
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww022 No BCLwSyncdWW
Safe=Fre LwSyncdRR DpdR
Time bclwdww022 2.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww023
"LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | 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(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,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 r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww023 Allowed
Histogram (38 states)
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
10 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
9 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
15 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
14 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
127 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
19 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
66 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
83 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
105 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
146 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
418 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1408 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
644 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
286 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
401 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
662 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
2614 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1176 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
4851 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
14589 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
652 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
29118 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
8045 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
5289 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
35342 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
96675 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
70881 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
25008 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
74350 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
31851 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
164528:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
66860 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
182068:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
134062:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
14236 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
33389 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=cc14d1f72457a494131d0111d5791792
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww023 No BCLwSyncdWW
Safe=Fre LwSyncsRR DpdR
Time bclwdww023 2.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww024
"DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r2 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww024 Allowed
Histogram (52 states)
1 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
1 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
10 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
30 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
7 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
26 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
19 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
38 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
44 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
16 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
54 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
45 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
72 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
390 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
64 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
815 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
432 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
1270 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
579 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
13347 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
2026 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
13670 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
26904 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
13949 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
39015 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
8325 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
16236 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
41611 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
17991 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
14413 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
63975 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
55693 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
49391 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
134363:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
63682 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
50480 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
112612:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
20730 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
24830 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
8580 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
204240:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=d9cb89dae7c1c7340715ada64130ec5d
Cycle=DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww024 No BCLwSyncdWW
Safe=Fre DpsR
Time bclwdww024 3.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww025
"LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww025 Allowed
Histogram (32 states)
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
9 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
4 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
4 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
15 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
379 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
53 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
1689 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
1529 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
24253 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
3028 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
2914 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
2634 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
20753 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
22792 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
49065 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
85271 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
139264:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
110489:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
119429:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
148567:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
30858 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
154440:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
10645 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
66470 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
5430 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=9e35ea0c011a355376ee19a400e99599
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww025 No BCLwSyncdWW
Safe=Fre LwSyncdRR DpsR
Time bclwdww025 2.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww026
"LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww026 Allowed
Histogram (64 states)
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
3 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
9 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
5 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
24 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
23 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
10 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
15 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
33 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
24 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
13 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
14 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
241 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
713 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
197 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
15 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
140 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1038 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
88 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
1018 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
831 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
1000 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
5201 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
1048 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
43 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
4850 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1611 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
1154 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
3279 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
98 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
6707 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
1599 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
19968 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
1159 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
11176 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
17665 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
20664 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
7127 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
5643 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
34066 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
98891 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
65518 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
69729 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
52211 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
64474 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
125243:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
211206:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
25798 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
53953 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
19468 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
27682 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
27366 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
7600 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2328 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1d532d0bb6dcdffd3b5563101102cb60
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww026 No BCLwSyncdWW
Safe=Fre LwSyncsRR DpsR
Time bclwdww026 3.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww027
"LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
Test bclwdww027 Allowed
Histogram (3 states)
279303:>1:r1=0; 1:r3=1;
957698:>1:r1=0; 1:r3=0;
762999:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 2000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=9db44a87c6f0512eb7b557fa626432dc
Cycle=LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww027 No BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww027 1.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww028
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 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,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww028 Allowed
Histogram (15 states)
12 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
25 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
303 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1350 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
18498 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
29524 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
14992 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
45286 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
163743:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
168575:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
169893:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
146607:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
156704:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
26225 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
58263 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=55921b82d0e8bcbda1b708c97c7b56b3
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww028 No BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww028 2.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww029
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | 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(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww029 Allowed
Histogram (38 states)
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
3 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
31 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
4 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
42 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
7 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
356 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
187 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
144 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
622 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
150 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
991 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
481 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
2601 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
529 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
983 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
201 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1103 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
9595 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
2684 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
2126 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
3169 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
18946 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
9420 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
2868 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
48287 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
26009 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
140480:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
168245:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
47405 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
82329 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
81116 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
130633:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
33420 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
138883:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
3708 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
42236 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=ed3e4f2d7ea7b66a761b0ef9aadf9b30
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww029 No BCLwSyncdWW
Safe=Fre LwSyncsRR LwSyncdRR
Time bclwdww029 2.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww030
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r2) | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww030 Allowed
Histogram (94 states)
1 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
3 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
2 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
26 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
16 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
5 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
6 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
6 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
10 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
20 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
10 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
41 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
24 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
3 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
91 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
27 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
135 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
13 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
18 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
18 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
15 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
49 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
152 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
64 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
70 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
92 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
31 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
106 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
172 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
13 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
118 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
112 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
293 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
26 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
159 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
714 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
880 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
166 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
147 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
824 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1042 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
40 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
56 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
286 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1703 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
138 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1322 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
716 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
984 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
272 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
150 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1416 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
4027 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
882 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
24 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1003 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
6224 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
2500 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1285 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
22427 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
1535 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
22805 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
618 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
7302 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
6464 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
63285 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
33657 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
8765 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
36490 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
10307 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
17093 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
14045 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
118009:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
17700 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
51778 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
80946 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
101631:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
64529 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
212790:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
57613 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
14694 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
6732 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
6 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=affa727dfb200dd46b9b0942598eb58d
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe
Relax bclwdww030 No BCLwSyncdWW
Safe=Fre LwSyncsRR
Time bclwdww030 5.19
$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=
Wed Dec 23 19:00:10 CET 2009