Wed Dec 30 10:12:16 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)
25461961:>1:r1=1; x=1;
39032745:>1:r1=0; x=2;
15505294:>1:r1=0; 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 51.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2887 :>1:r1=1; 3:r1=1; x=1; z=2;
3514 :>1:r1=1; 3:r1=1; x=2; z=1;
25605 :>1:r1=0; 3:r1=1; x=2; z=2;
13360 :>1:r1=1; 3:r1=0; x=2; z=2;
2157282:>1:r1=1; 3:r1=1; x=1; z=1;
1175449:>1:r1=0; 3:r1=1; x=1; z=2;
628737:>1:r1=1; 3:r1=0; x=1; z=2;
1158217:>1:r1=1; 3:r1=0; x=2; z=1;
6766909:>1:r1=1; 3:r1=0; x=1; z=1;
4988900:>1:r1=0; 3:r1=0; x=2; z=2;
6499075:>1:r1=0; 3:r1=1; x=1; z=1;
6458242:>1:r1=0; 3:r1=0; x=1; z=2;
7456522:>1:r1=0; 3:r1=0; x=2; z=1;
1749076:>1:r1=0; 3:r1=0; x=1; z=1;
916225:>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.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
14535 :>1:r1=0; 3:r1=1; x=2; z=2;
2977 :>1:r1=1; 3:r1=1; x=1; z=2;
2586 :>1:r1=1; 3:r1=0; x=2; z=2;
2269 :>1:r1=1; 3:r1=1; x=2; z=1;
415775:>1:r1=1; 3:r1=0; x=2; z=1;
778708:>1:r1=0; 3:r1=1; x=2; z=1;
1023705:>1:r1=0; 3:r1=1; x=1; z=2;
603631:>1:r1=1; 3:r1=0; x=1; z=2;
1892337:>1:r1=1; 3:r1=1; x=1; z=1;
6927745:>1:r1=1; 3:r1=0; x=1; z=1;
6653230:>1:r1=0; 3:r1=0; x=1; z=2;
5114293:>1:r1=0; 3:r1=0; x=2; z=2;
7952511:>1:r1=0; 3:r1=0; x=2; z=1;
2329768:>1:r1=0; 3:r1=0; x=1; z=1;
6285930:>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 99.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
747 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
2591 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
6728 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
4424 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
349431:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
541178:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1583168:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1194656:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
2467757:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
8069763:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
5850156:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
7872304:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
3695817:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
6358535:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
2002745:>1:r1=0; 3:r1=0; 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 95.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
7 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
2 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
18 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
24 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
18 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
102 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
15 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
74 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
9 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
699 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
517 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
392 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
187 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
575 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
42325 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
164 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
1793 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
65046 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
60025 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
424780:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
66765 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
999052:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
550280:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
342264:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
80988 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
2276011:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
3146674:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
603163:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
7017626:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
3716109:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
3642688:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3481341:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
842715:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
6438603:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
4654561:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1544386:>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 131.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1040 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
698 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
6612 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
408108:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
7397 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
544915:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1274112:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
2080892:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1110340:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
8099079:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
7209029:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
6749451:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2483465:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
3883694:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
6141168:>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 92.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
23 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
2400 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
7674 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
146 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
189 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
117 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
257 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
475 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
59823 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
2491 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
2999 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
13151 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
1498 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
47434 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
176869:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
59471 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
18421 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
30280 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
57182 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
35009 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
34367 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
90182 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
57881 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
90105 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
9556 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
51759 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
951186:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
463964:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
341017:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
539438:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
502919:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
6683650:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
4674019:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
2606569:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
3636081:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
3597687:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
779585:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3274329:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
2473301:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
1184739:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
7441756:>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 138.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
271448:>2:r1=1; x=1; y=2;
521859:>2:r1=0; x=2; y=2;
417640:>2:r1=1; x=2; y=1;
11402267:>2:r1=0; x=1; y=2;
10957944:>2:r1=1; x=1; y=1;
3481033:>2:r1=0; x=1; y=1;
12947809:>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 76.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
251727:>2:r1=1; x=1; y=2;
265696:>2:r1=0; x=2; y=2;
389543:>2:r1=1; x=2; y=1;
11016474:>2:r1=1; x=1; y=1;
12949526:>2:r1=0; x=2; y=1;
11353919:>2:r1=0; x=1; y=2;
3773115:>2:r1=0; x=1; 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 75.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
545664:>2:r1=1; 2:r4=1; y=2;
277153:>2:r1=1; 2:r4=0; y=1;
451440:>2:r1=0; 2:r4=0; y=2;
12444225:>2:r1=1; 2:r4=1; y=1;
3491291:>2:r1=0; 2:r4=1; y=1;
10945255:>2:r1=0; 2:r4=1; y=2;
11844972:>2:r1=0; 2:r4=0; 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.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6 :>2:r1=2; 2:r4=1; x=2; y=1;
12 :>2:r1=1; 2:r4=2; x=1; y=2;
55 :>2:r1=0; 2:r4=2; x=2; y=1;
286 :>2:r1=2; 2:r4=1; x=1; y=1;
138 :>2:r1=0; 2:r4=2; x=1; y=1;
524 :>2:r1=0; 2:r4=1; x=1; y=1;
223 :>2:r1=0; 2:r4=1; x=1; y=2;
2846 :>2:r1=0; 2:r4=2; x=1; y=2;
2755968:>2:r1=0; 2:r4=0; x=2; y=1;
4682522:>2:r1=1; 2:r4=1; x=1; y=2;
2280964:>2:r1=2; 2:r4=2; x=1; y=1;
159509:>2:r1=1; 2:r4=1; x=2; y=1;
4271083:>2:r1=2; 2:r4=2; x=1; y=2;
10552338:>2:r1=0; 2:r4=0; x=1; y=1;
1094904:>2:r1=1; 2:r4=1; x=1; y=1;
11310121:>2:r1=2; 2:r4=2; x=2; y=1;
2888501:>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 77.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
342899:>2:r1=1; 2:r3=0; y=1;
195990:>2:r1=1; 2:r3=1; y=2;
706772:>2:r1=0; 2:r3=0; y=2;
12263632:>2:r1=0; 2:r3=0; y=1;
11392258:>2:r1=1; 2:r3=1; y=1;
11160943:>2:r1=0; 2:r3=1; y=2;
3937506:>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 66.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
123 :>2:r1=0; 2:r3=1; x=2; y=1;
6033 :>2:r1=2; 2:r3=1; x=1; y=1;
613 :>2:r1=1; 2:r3=2; x=1; y=2;
3953 :>2:r1=0; 2:r3=2; x=2; y=1;
377 :>2:r1=2; 2:r3=1; x=2; y=1;
50788 :>2:r1=0; 2:r3=2; x=1; y=2;
121316:>2:r1=1; 2:r3=1; x=2; y=1;
8759 :>2:r1=0; 2:r3=1; x=1; y=2;
64494 :>2:r1=0; 2:r3=1; x=1; y=1;
32766 :>2:r1=0; 2:r3=2; x=1; y=1;
4024106:>2:r1=1; 2:r3=1; x=1; y=2;
3383260:>2:r1=0; 2:r3=0; x=1; y=2;
2577247:>2:r1=0; 2:r3=0; x=2; y=1;
990320:>2:r1=1; 2:r3=1; x=1; y=1;
3972648:>2:r1=2; 2:r3=2; x=1; y=2;
2373048:>2:r1=2; 2:r3=2; x=1; y=1;
11281806:>2:r1=2; 2:r3=2; x=2; y=1;
11108343:>2:r1=0; 2:r3=0; x=1; y=1;
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.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)
24938160:>1:r1=1; x=1;
33397166:>1:r1=0; x=2;
21664674:>1:r1=0; 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.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1951 :>1:r1=1; 3:r1=1; x=2; z=1;
2079 :>1:r1=1; 3:r1=1; x=1; z=2;
2132 :>1:r1=1; 3:r1=0; x=2; z=2;
3442 :>1:r1=0; 3:r1=1; x=2; z=2;
444028:>1:r1=0; 3:r1=1; x=1; z=2;
557361:>1:r1=1; 3:r1=0; x=1; z=2;
696390:>1:r1=0; 3:r1=1; x=2; z=1;
4323418:>1:r1=0; 3:r1=0; x=2; z=2;
412296:>1:r1=1; 3:r1=0; x=2; z=1;
6496021:>1:r1=1; 3:r1=0; x=1; z=1;
6722983:>1:r1=0; 3:r1=1; x=1; z=1;
7950710:>1:r1=0; 3:r1=0; x=2; z=1;
7379654:>1:r1=0; 3:r1=0; x=1; z=2;
2469324:>1:r1=1; 3:r1=1; x=1; z=1;
2538211:>1:r1=0; 3:r1=0; 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 99.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6703 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
2296 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
4100 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
2615 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
540975:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
780272:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
592555:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
5672824:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
8197946:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
4111267:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
7160834:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
7175020:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
3108956:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
754077:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1889560:>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=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 89.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (36 states)
3 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
5 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
1 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
6 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
12 :>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;
13 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
101 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
230 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
100 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
189 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
220 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
666 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
1825 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
644 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
292 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
46800 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
21153 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
307988:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
28648 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
484597:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
53651 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
550252:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
44232 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
1429244:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
737300:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
3968870:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
889425:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
6373906:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
3215658:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
3345769:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
7282000:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
3658554:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
4809586:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1489385:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
1258657:>1:r1=0; 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 128.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
710 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
574 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1583 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
5255 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
604673:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
390249:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
3327066:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
5705557:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
444247:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
6949209:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
3072088:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
7854218:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
8672462:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1199166:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1772943:>1:r1=1; 3:r1=1; 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 92.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
696 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
49 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
2871 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
30 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
591 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
92 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
187 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
27787 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
363 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
2659 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1011 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
20551 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
16561 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
10068 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
6636 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
176296:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
75944 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
53594 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
31690 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
34261 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
29994 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
48792 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
31144 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
35267 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
25895 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
360310:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
9937 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
263621:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
2959386:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
710010:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
1165533:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
1368876:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
616064:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
7074330:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
3088307:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
7405465:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
5434221:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
3688949:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
1129913:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3636258:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
455788:>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 133.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
15485774:>1:r1=0; 1:r4=1;
36802726:>1:r1=0; 1:r4=0;
27711500:>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 40.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
7321 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
15254 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
8214 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
31736 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
488880:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
867637:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1336188:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
6477200:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
1454328:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
6229611:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
7179481:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
4540065:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
1778445:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
2718040:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
6867600:>1:r1=1; 1:r4=1; 3:r1=0; 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 81.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (36 states)
2 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
37 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
8 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
12 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
13 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
207 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
153 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
914 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
117 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
306 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
89 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
3901 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
38804 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
644 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
68254 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
45929 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
120 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
287319:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
65566 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
632161:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
572497:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
1234798:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
795852:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
3979406:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
3349136:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
3175665:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
2615839:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
720435:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
924504:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
4617934:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
2507345:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
6893872:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
72703 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
7395453:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; 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 117.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3516 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
11699 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
4118 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
20228 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
799669:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
598967:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
1143836:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
6437917:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
1144814:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
6526536:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
1775517:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
2580804:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
4580912:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
7509369:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
6862098:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
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 77.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
69 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
310 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
17 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
1547 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
160 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
10430 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
338 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
50 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
191 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
2054 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
32622 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1881 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
43503 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
7880 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
58405 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
9654 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
17004 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
58040 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
38930 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
37496 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
20364 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
95440 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
7090 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
18617 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
279131:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
29261 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
524144:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
1498 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
788486:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
644949:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
503194:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
7276266:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
4905505:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
2852839:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
3632673:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
2416548:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
967516:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3535960:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
2450149:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
976588:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
7753200:>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 126.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (71 states)
1 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
12 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
9 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
6 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
1 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
15 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
18 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
9 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
5 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
4 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
24 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
15 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
24 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
13 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
27 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
5 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
71 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
16 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
71 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
6 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
45 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
31 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
3 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
30 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
104 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
84 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
75 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
25 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
56 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
20 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
86 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
21 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
2166 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
25 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
262 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
46782 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
54672 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
17112 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
25514 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
229185:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
282790:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
249315:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
861974:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
505951:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
1704485:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
239905:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
240565:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
3688654:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
363410:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
2773199:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
260230:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
2424395:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
1539933:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
3867994:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
2134070:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
711009:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
555281:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1964784:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
887901:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
2892456:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
2760820:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
8714202:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
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 182.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
4 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
4 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
3 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
17 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
341 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
26 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
44 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
82 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
94 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
224 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
108 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
264 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
185 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
85 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
2535 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
175 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
63 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
147 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
29650 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
22075 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
32713 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
206382:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
528951:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
76917 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
1145140:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
67831 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
782355:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
2852699:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
607001:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
1898122:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
931231:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
1331901:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7133425:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
3163492:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
5389152:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
6428532:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
4247835:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
3120181:>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 121.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (92 states)
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
6 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
14 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
28 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
24 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
21 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
14 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
13 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
119 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
203 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
19 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
239 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
3492 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2511 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
239 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
512 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1089 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
8 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
5315 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
26 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
454 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
311 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
59 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
49 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1113 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
3386 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
3275 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
51 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
28 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1089 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
133 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
90 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
512 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
7744 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
791 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
8622 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
13633 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1258 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
20303 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
89 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
27782 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
127 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
12522 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
207260:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
7103 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
5039 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
74482 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
44263 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
119 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
186574:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
27692 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
197159:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
12660 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
161335:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
96792 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
689721:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
31958 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
52283 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
89435 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
2005063:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
586097:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
154285:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
2010651:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
552217:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
2867333:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
3417411:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
345118:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
2035224:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
432491:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
3739857:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
2992064:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
324433:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
2093350:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
9211830:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
1635549:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
72316 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
3310415:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
213071:>1:r1=2; 1:r4=2; 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 215.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
27274302:>1:r1=1; 1:r3=1;
37958017:>1:r1=0; 1:r3=0;
14767681:>1:r1=0; 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 40.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5133 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
10703 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
5926 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
23224 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
586017:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
822538:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1442838:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
2558208:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
6700409:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1962114:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
7355705:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
4455765:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
6298827:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1407088:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
6365505:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
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 77.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
35 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
19 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
72 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
511 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
310 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1659 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1186 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
14970 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
144 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
55958 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
10031 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
4162 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
1468 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
158 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
33480 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
9412 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
26175 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
6353 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
21633 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
44802 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
72902 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
35854 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
91196 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
53154 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
64014 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1148149:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
491652:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
602382:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
207571:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
771211:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1695207:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
4354190:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
3572606:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3032458:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
7061702:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
2607456:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1370326:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
6437346:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
5261950:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
811886:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
24246 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 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 128.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=1; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
6 :>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=2; x=1; y=2;
22 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
11 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
65 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
7 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
16 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
19 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
12 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
19 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
16 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
19 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
39 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
3 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
40 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
281 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
115 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
938 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
109 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2030 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
34 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
4758 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1330 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
114 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
71 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
726 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
56 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
74 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1159 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
636 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
560 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
14 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
7050 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
43965 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
2407 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2912 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
1865 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
100 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
744 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
182 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
2985 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
335 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1524 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
9920 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
944 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
475 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1060 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
2165 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
12847 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
2071 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
108044:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
4786 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
7413 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
25423 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1143 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
8643 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
6559 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
11499 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
41955 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
4424 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
31428 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
4709 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
47849 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
16841 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
122137:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
22790 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
10599 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1543 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
115726:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
29092 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
24021 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
58968 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
131801:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
62831 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
180410:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
122312:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
157370:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
146912:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
158419:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
271204:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
157078:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
540831:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
182192:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
511752:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
141856:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
90101 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
352108:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
3193301:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
594144:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
2396706:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
445758:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1911619:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
3107090:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
2174264:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
2462251:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3271210:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
8874362:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
2544093:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
73706 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
3145742:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1786126:>1:r1=2; 1:r3=2; 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 242.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
Wed Dec 30 11:05:39 CET 2009