Thu Dec 31 09:39:05 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)
15953359:>1:r1=0; x=1;
39085905:>1:r1=0; x=2;
24960736:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 52.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4009 :>1:r1=1; 3:r1=1; x=2; z=1;
2508 :>1:r1=1; 3:r1=1; x=1; z=2;
24041 :>1:r1=0; 3:r1=1; x=2; z=2;
11953 :>1:r1=1; 3:r1=0; x=2; z=2;
553900:>1:r1=1; 3:r1=0; x=1; z=2;
1204038:>1:r1=0; 3:r1=1; x=1; z=2;
2247934:>1:r1=1; 3:r1=1; x=1; z=1;
6772646:>1:r1=1; 3:r1=0; x=1; z=1;
6420665:>1:r1=0; 3:r1=1; x=1; z=1;
6361444:>1:r1=0; 3:r1=0; x=1; z=2;
1200555:>1:r1=1; 3:r1=0; x=2; z=1;
5013472:>1:r1=0; 3:r1=0; x=2; z=2;
7488220:>1:r1=0; 3:r1=0; x=2; z=1;
1724575:>1:r1=0; 3:r1=0; x=1; z=1;
970040:>1:r1=0; 3:r1=1; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 102.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2975 :>1:r1=1; 3:r1=0; x=2; z=2;
18181 :>1:r1=0; 3:r1=1; x=2; z=2;
3076 :>1:r1=1; 3:r1=1; x=1; z=2;
1986 :>1:r1=1; 3:r1=1; x=2; z=1;
664355:>1:r1=1; 3:r1=0; x=1; z=2;
765188:>1:r1=0; 3:r1=1; x=2; z=1;
1011547:>1:r1=0; 3:r1=1; x=1; z=2;
432370:>1:r1=1; 3:r1=0; x=2; z=1;
5338946:>1:r1=0; 3:r1=0; x=2; z=2;
1880368:>1:r1=1; 3:r1=1; x=1; z=1;
7836904:>1:r1=0; 3:r1=0; x=2; z=1;
6607444:>1:r1=0; 3:r1=0; x=1; z=2;
2414759:>1:r1=0; 3:r1=0; x=1; z=1;
6831839:>1:r1=1; 3:r1=0; x=1; z=1;
6190062:>1:r1=0; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 100.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1003 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
2068 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
6182 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
5216 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
438759:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1586821:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
430967:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
4099351:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
7936580:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
7871741:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
5707396:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
2353856:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
6271703:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1098020:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
2190337:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 93.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (38 states)
1 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
5 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
25 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
4 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
7 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
19 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
9 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
18 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
185 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
134 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
301 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
116 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
629 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
198 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
722 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
37653 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
381 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
66039 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
2038 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
48306 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
610906:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
58697 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
95954 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
383523:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
480831:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
864508:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
3493441:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
3035504:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
646940:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
827526:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3653925:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
6648154:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
3464202:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
7188811:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4565935:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
2339523:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
1484829:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 127.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3157 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
3211 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
10733 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
11777 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
613698:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
710526:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
2286622:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1364460:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
2156220:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
4029173:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
6586931:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
7154277:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
7745272:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1305526:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
6018417:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 90.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
5 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
43 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
138 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
2759 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
9589 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
158 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
68922 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
699 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1620 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
299 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
22243 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
3199 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
176668:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
58821 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
13361 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
344 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
33596 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
67825 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
3139 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
11920 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
31177 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
35846 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
60932 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
78538 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
49077 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
584738:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1304810:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
27097 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
477806:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
2062407:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
1045380:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
2680528:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
3545634:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
3630076:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
819852:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
6770885:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
388141:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
4800260:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
486247:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3269302:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
99031 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
7276888:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 140.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
461595:>2:r1=0; x=2; y=2;
268246:>2:r1=1; x=1; y=2;
464830:>2:r1=1; x=2; y=1;
11358520:>2:r1=0; x=1; y=2;
11007145:>2:r1=1; x=1; y=1;
3353108:>2:r1=0; x=1; y=1;
13086556:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 75.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
244091:>2:r1=1; x=1; y=2;
301706:>2:r1=0; x=2; y=2;
405371:>2:r1=1; x=2; y=1;
11421320:>2:r1=0; x=1; y=2;
3847037:>2:r1=0; x=1; y=1;
10892768:>2:r1=1; x=1; y=1;
12887707:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 76.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
253076:>2:r1=1; 2:r4=0; y=1;
454387:>2:r1=0; 2:r4=0; y=2;
431465:>2:r1=1; 2:r4=1; y=2;
11900109:>2:r1=0; 2:r4=0; y=1;
12372199:>2:r1=1; 2:r4=1; y=1;
11200615:>2:r1=0; 2:r4=1; y=2;
3388149:>2:r1=0; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 68.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
7 :>2:r1=1; 2:r4=2; x=1; y=2;
5 :>2:r1=2; 2:r4=1; x=2; y=1;
35 :>2:r1=0; 2:r4=2; x=2; y=1;
142 :>2:r1=0; 2:r4=2; x=1; y=1;
260 :>2:r1=2; 2:r4=1; x=1; y=1;
259 :>2:r1=0; 2:r4=1; x=1; y=2;
559 :>2:r1=0; 2:r4=1; x=1; y=1;
3740 :>2:r1=0; 2:r4=2; x=1; y=2;
152503:>2:r1=1; 2:r4=1; x=2; y=1;
2645155:>2:r1=0; 2:r4=0; x=2; y=1;
1054323:>2:r1=1; 2:r4=1; x=1; y=1;
4178716:>2:r1=2; 2:r4=2; x=1; y=2;
2303229:>2:r1=2; 2:r4=2; x=1; y=1;
10588251:>2:r1=0; 2:r4=0; x=1; y=1;
4715576:>2:r1=1; 2:r4=1; x=1; y=2;
11217989:>2:r1=2; 2:r4=2; x=2; y=1;
3139251:>2:r1=0; 2:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
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 78.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
284180:>2:r1=1; 2:r3=0; y=1;
241716:>2:r1=1; 2:r3=1; y=2;
550169:>2:r1=0; 2:r3=0; y=2;
11952946:>2:r1=0; 2:r3=0; y=1;
11841811:>2:r1=1; 2:r3=1; y=1;
11288332:>2:r1=0; 2:r3=1; y=2;
3840846:>2:r1=0; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 67.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
112 :>2:r1=0; 2:r3=1; x=2; y=1;
391 :>2:r1=2; 2:r3=1; x=2; y=1;
3501 :>2:r1=0; 2:r3=2; x=2; y=1;
5408 :>2:r1=2; 2:r3=1; x=1; y=1;
514 :>2:r1=1; 2:r3=2; x=1; y=2;
138212:>2:r1=1; 2:r3=1; x=2; y=1;
9956 :>2:r1=0; 2:r3=1; x=1; y=2;
21560 :>2:r1=0; 2:r3=2; x=1; y=1;
47054 :>2:r1=0; 2:r3=1; x=1; y=1;
32905 :>2:r1=0; 2:r3=2; x=1; y=2;
3850715:>2:r1=2; 2:r3=2; x=1; y=2;
2500821:>2:r1=0; 2:r3=0; x=2; y=1;
2415462:>2:r1=2; 2:r3=2; x=1; y=1;
4268482:>2:r1=1; 2:r3=1; x=1; y=2;
11083034:>2:r1=0; 2:r3=0; x=1; y=1;
1035146:>2:r1=1; 2:r3=1; x=1; y=1;
11227960:>2:r1=2; 2:r3=2; x=2; y=1;
3358767:>2:r1=0; 2:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
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 80.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
23460251:>1:r1=0; x=1;
31799616:>1:r1=0; x=2;
24740133:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 52.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1743 :>1:r1=1; 3:r1=1; x=2; z=1;
3669 :>1:r1=0; 3:r1=1; x=2; z=2;
1720 :>1:r1=1; 3:r1=1; x=1; z=2;
2901 :>1:r1=1; 3:r1=0; x=2; z=2;
743697:>1:r1=0; 3:r1=1; x=2; z=1;
616310:>1:r1=1; 3:r1=0; x=1; z=2;
2069203:>1:r1=1; 3:r1=1; x=1; z=1;
4725050:>1:r1=0; 3:r1=0; x=2; z=2;
7717885:>1:r1=0; 3:r1=0; x=2; z=1;
466874:>1:r1=1; 3:r1=0; x=2; z=1;
449760:>1:r1=0; 3:r1=1; x=1; z=2;
6801213:>1:r1=1; 3:r1=0; x=1; z=1;
7323546:>1:r1=0; 3:r1=0; x=1; z=2;
2402923:>1:r1=0; 3:r1=0; x=1; z=1;
6673506:>1:r1=0; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 100.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1701 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
2429 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
5653 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
3279 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
495498:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
576914:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
793012:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
761764:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1606115:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5770085:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
7364029:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
8101590:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
4446135:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
3101705:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
6970091:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 92.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (37 states)
2 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
3 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
4 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
2 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
6 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
18 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
7 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
132 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
5 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
259 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
735 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
81 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
264 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
812 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
490 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
327 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
1298 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
26034 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
33140 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
18005 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
254086:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
37654 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
516257:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
47453 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
494307:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
647139:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1419849:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
3104013:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3984932:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
919821:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
3121112:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
7301050:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
3678905:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
1260467:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
5043127:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1596729:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
6491475:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 130.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2567 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
2308 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
15444 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
3409 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
547243:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
605672:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1199757:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
610305:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
2210530:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
7708338:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
8431739:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
4042161:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
6465291:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
5715859:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
2439377:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 90.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
26 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
50 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
1012 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
3538 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
170 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
310 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
4 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
29717 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1055 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
272 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
127 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
30519 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
8636 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
10695 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
52602 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
3110 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
24668 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
36942 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
28693 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
18405 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
5252 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
58199 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
94163 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
133173:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
16761 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
32298 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
1066432:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
424491:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
732554:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
42204 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
1582524:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
615434:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3533834:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
3657695:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
293710:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
7153238:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
3275870:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1170775:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
7066332:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
5362141:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
2919497:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
512872:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 132.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
15634910:>1:r1=0; 1:r4=1;
36744989:>1:r1=0; 1:r4=0;
27620101:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 39.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6428 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
5595 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
29750 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
16502 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
569949:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
746675:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1416866:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
6804226:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
6660304:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
4176004:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
1680590:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
6487912:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
7180956:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
1474827:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
2743416:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 80.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (37 states)
1 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
6 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
3 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
8 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
32 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
139 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
8 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
118 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
471 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
6 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
45 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
82 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
988 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
169 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
74 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
580 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
45132 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
29567 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
38215 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
41077 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
223680:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
450417:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
1163506:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
730446:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
410771:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
3248829:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
3792501:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
3290831:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
4958693:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
639132:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
7584387:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2585856:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1080923:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
6566213:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
56569 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
3060523:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 118.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4268 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
21094 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
4392 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
9955 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
557036:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
839541:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
1096852:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
6480248:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
6850342:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
7596594:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
6328100:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
2763424:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
4707279:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
981025:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
1759850:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 75.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
8 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
1029 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
240 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
22 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
7816 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
271 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
72 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
154 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
1547 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
8418 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
607 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
211 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
30282 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
5967 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1439 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
35889 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
27875 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
21853 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
39769 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
8012 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
53107 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
33362 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
17446 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
53049 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
61760 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
60386 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
469605:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
721482:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
589925:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
3078858:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
632944:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
6539844:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
992326:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
255520:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
4884248:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
2324086:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1046239:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3851963:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
3102550:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
3321431:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
7718386:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 129.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (70 states)
1 :>1:r1=1; 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=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
26 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
13 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
12 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
14 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
8 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
27 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
2 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
14 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
32 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
9 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
116 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
38 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
9 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
27 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
9 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
5 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
9 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
29 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
138 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
73 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
21 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
23 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
17 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
71 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
79 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
110 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
182 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
23 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
141 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
99 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
36 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
21 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
19 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
2082 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
549 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
148 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
18012 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
167636:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
256261:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
32113 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
180377:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
13642 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
274533:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
2230097:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
248946:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
675461:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
678446:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
1600623:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
732951:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
3272634:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
2557338:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
3369730:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
3184381:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1915017:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
3467311:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
239864:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
2366651:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
381859:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
8846067:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
2151659:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
387040:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
708336:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
38772 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
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 176.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
3 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
4 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
6 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
14 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
2 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
6 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
70 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
118 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
72 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
304 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
81 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
40 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
125 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
186 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
282 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
183 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
162 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
159 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
2046 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
220 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
26391 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
225328:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
27907 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
33259 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
82290 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
82659 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
1202472:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
1589207:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
601001:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
853318:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
4050408:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
2907370:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
3122317:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
554113:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
1352737:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7070419:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
1035527:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
6861071:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
5198223:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
3119898:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
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 120.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (89 states)
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
5 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
1 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
16 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
47 :>1:r1=2; 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=1; x=1; y=1;
16 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
20 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
268 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
48 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
12 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
5398 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
149 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
159 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
75 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
957 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
7 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2900 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
39 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
388 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
819 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
9 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
74 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
1069 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
73 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
102 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
374 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
22 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
40 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
75 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
201 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1153 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
4580 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
64 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1444 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
748 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
575 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
99 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
88 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
1772 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
65655 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
4316 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
17433 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
12583 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1185 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
175174:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
26882 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
8965 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
212897:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
5692 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
13184 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
226774:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
33741 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
63247 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
99584 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
15226 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
211328:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
22709 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
684 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
124755:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
49157 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
323405:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
422098:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
83928 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
120050:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
631291:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
493667:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
443334:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
1619065:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
75064 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
3107328:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
303203:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
2052405:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
3088485:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
3578636:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
2354786:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
1972356:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
9136116:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
3206497:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
3462782:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
2110430:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 218.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
11328227:>1:r1=0; 1:r3=1;
38315602:>1:r1=0; 1:r3=0;
30356171:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 39.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4711 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
4347 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
28846 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
18104 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
753795:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
582344:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
2140490:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1152572:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1310810:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
6263068:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
6444247:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
7628813:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
4023471:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2544010:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
7100372:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 40000000
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 78.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
5 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
363 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
90 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1238 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
22 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
366 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
43 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
131 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
566 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
65849 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
13986 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
6500 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
22702 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
1159 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
23716 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
43172 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
16241 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
5353 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
30343 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
24848 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
38996 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
44895 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
3570 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
47005 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
20647 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
459012:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1894502:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
4324850:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
698855:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1396676:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3509174:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
7036 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
3028044:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
789849:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
6215646:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2583610:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
7264984:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
587759:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
5524517:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
179571:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1124108:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 124.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (105 states)
1 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
6 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
12 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
15 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
7 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
16 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
16 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
31 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
52 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
23 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
13 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1525 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
41 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
515 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
22 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
130 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
70 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
184 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1057 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
6753 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
26 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
604 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
4082 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
5 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
108 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
78 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
73 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
517 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
67 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1025 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
15 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
141 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
7561 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
396 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
752 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
526 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
38414 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
5065 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
903 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
3193 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3576 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
77 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
3222 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
884 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
100439:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2621 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
50070 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1116 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1315 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
89878 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
1593 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
164 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
14147 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1319 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
14584 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
32674 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
569 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
8359 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
12190 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
6938 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
3757 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
5580 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
4296 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
4620 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
172738:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
238049:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
11565 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
36678 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
60949 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
228909:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
60848 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
10773 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
20860 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
87739 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
14592 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
29073 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
41695 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
6952 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
56880 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
6977 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
43280 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
153128:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
516609:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
174956:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
152523:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
2228234:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
125449:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
154537:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
3183137:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
545767:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
615851:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
376450:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
3257107:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
2788153:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
2232388:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
3248916:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1708862:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
8401553:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
2669049:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1723823:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
400816:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
3252851:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
523253:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 240.91
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 40
Thu Dec 31 10:32:19 CET 2009