Sun Dec 27 15:43:44 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
Test bclwdww000 Allowed
Histogram (3 states)
13479015:>1:r1=0; x=1;
39543958:>1:r1=0; x=2;
26977027:>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 33.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r30,r27,r27
_litmus_P3_2_: li r11,1
_litmus_P3_3_: stwx r11,r30,r2
Test bclwdww001 Allowed
Histogram (15 states)
4532 :>1:r1=1; 3:r1=1; x=2; z=1;
7975 :>1:r1=1; 3:r1=0; x=2; z=2;
3917 :>1:r1=1; 3:r1=1; x=1; z=2;
12802 :>1:r1=0; 3:r1=1; x=2; z=2;
626932:>1:r1=1; 3:r1=0; x=1; z=2;
790162:>1:r1=0; 3:r1=1; x=2; z=1;
861442:>1:r1=0; 3:r1=1; x=1; z=2;
5676856:>1:r1=0; 3:r1=0; x=2; z=2;
6792238:>1:r1=1; 3:r1=0; x=1; z=1;
813379:>1:r1=1; 3:r1=0; x=2; z=1;
1847083:>1:r1=0; 3:r1=0; x=1; z=1;
6477988:>1:r1=0; 3:r1=0; x=1; z=2;
7355615:>1:r1=0; 3:r1=0; x=2; z=1;
1879760:>1:r1=1; 3:r1=1; x=1; z=1;
6849319:>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=d6ca5faa9797f1b1addda6b4fc107253
Cycle=DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww001 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww001 64.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r29,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r30,1
_litmus_P3_3_: stw r30,0(r2)
Test bclwdww002 Allowed
Histogram (15 states)
2268 :>1:r1=1; 3:r1=1; x=1; z=2;
2546 :>1:r1=1; 3:r1=1; x=2; z=1;
2843 :>1:r1=1; 3:r1=0; x=2; z=2;
8950 :>1:r1=0; 3:r1=1; x=2; z=2;
706105:>1:r1=0; 3:r1=1; x=2; z=1;
494526:>1:r1=1; 3:r1=0; x=1; z=2;
4471352:>1:r1=0; 3:r1=0; x=2; z=2;
6692178:>1:r1=1; 3:r1=0; x=1; z=1;
6324376:>1:r1=0; 3:r1=1; x=1; z=1;
819714:>1:r1=0; 3:r1=1; x=1; z=2;
1946807:>1:r1=0; 3:r1=0; x=1; z=1;
7228619:>1:r1=0; 3:r1=0; x=1; z=2;
626868:>1:r1=1; 3:r1=0; x=2; z=1;
2762786:>1:r1=1; 3:r1=1; x=1; z=1;
7910062:>1:r1=0; 3:r1=0; 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=f222837c1b9c320fc4731d82df04c0c8
Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww002 No BCLwSyncdWW
Safe=Wse LwSyncdRW DpdW
Time bclwdww002 62.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww003
"DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r11,r27,r27
_litmus_P3_2_: lwzx r30,r11,r2
Test bclwdww003 Allowed
Histogram (15 states)
4311 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
7000 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
12584 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
27201 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
632665:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1823065:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1462074:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1394979:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
7255927:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
5292634:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
7685950:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
3736956:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
6732729:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
3367772:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
564153:>1:r1=0; 3:r1=1; 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=13e9eff5346eb465cffd68e7d2363168
Cycle=DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww003 No BCLwSyncdWW
Safe=Fre Wse DpdW DpdR
Time bclwdww003 57.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r30,0(r2)
_litmus_P3_1_: xor r11,r30,r30
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww004 Allowed
Histogram (38 states)
4 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
32 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
3 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
5 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
103 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
285 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
34 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
66 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
1487 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
241 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
682 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
385 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
524 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
3204 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
5857 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1818 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
53106 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
47819 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
36665 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
1646 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
54912 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
494711:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
604818:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
139826:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
918682:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
2510269:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
2652319:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
3753798:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
624198:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
4452262:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
700465:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
911992:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3285076:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
7319036:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
5758303:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
4248350:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1417016:>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 63.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww005 Allowed
Histogram (15 states)
9165 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
4045 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
15256 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
662398:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
5267 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
604762:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
947897:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
1230040:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
6112950:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
4493004:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
7599420:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2147063:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
6752901:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2401145:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
7014687:>1:r1=0; 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=1b7673dab67cdeed3a93a9f78642c123
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww005 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRR DpdW
Time bclwdww005 58.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,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;
30 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
19 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
315 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
166 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
739 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
118 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
540 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
3236 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
196 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
20565 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
24689 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
2488 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
13198 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
7440 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
13162 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
21109 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
22484 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
27863 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
9790 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
99796 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
45268 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
1648 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
21411 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
46151 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
507158:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
370265:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
38510 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
73416 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
2706372:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
757578:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
2887268:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
3265088:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
395723:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
7518482:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
5329160:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
3274872:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
682001:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1091095:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
4894652:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
1302807:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
4523131:>1:r1=0; 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=355c23adb39c4f8a03f27206e6d5ad02
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww006 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR DpdW
Time bclwdww006 66.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r29,1
_litmus_P0_4_: stw r29,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: xor r30,r27,r27
_litmus_P2_2_: li r11,1
_litmus_P2_3_: stwx r11,r30,r2
Test bclwdww007 Allowed
Histogram (7 states)
157600:>2:r1=1; x=2; y=1;
3863021:>2:r1=0; x=1; y=1;
11676888:>2:r1=0; x=1; y=2;
12225097:>2:r1=0; x=2; y=1;
10955299:>2:r1=1; x=1; y=1;
205896:>2:r1=1; x=1; y=2;
916199:>2:r1=0; x=2; y=2;
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 48.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r29,1
_litmus_P0_4_: stw r29,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li r30,1
_litmus_P2_3_: stw r30,0(r2)
Test bclwdww008 Allowed
Histogram (7 states)
164748:>2:r1=1; x=1; y=2;
221073:>2:r1=1; x=2; y=1;
768031:>2:r1=0; x=2; y=2;
12140394:>2:r1=0; x=1; y=2;
3876152:>2:r1=0; x=1; y=1;
10176470:>2:r1=1; x=1; y=1;
12653132:>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 48.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r29,1
_litmus_P0_4_: stw r29,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: xor r11,r26,r26
_litmus_P2_2_: lwzx r27,r11,r2
Test bclwdww009 Allowed
Histogram (7 states)
304221:>2:r1=1; 2:r4=0; y=1;
1974284:>2:r1=0; 2:r4=0; y=2;
4513927:>2:r1=0; 2:r4=1; y=1;
12327346:>2:r1=0; 2:r4=0; y=1;
10010279:>2:r1=1; 2:r4=1; y=1;
179061:>2:r1=1; 2:r4=1; y=2;
10690882:>2:r1=0; 2:r4=1; y=2;
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 43.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r30,0(r2)
_litmus_P2_1_: xor r11,r30,r30
_litmus_P2_2_: lwzx r9,r11,r2
Test bclwdww010 Allowed
Histogram (17 states)
1 :>2:r1=1; 2:r4=2; x=1; y=2;
6 :>2:r1=2; 2:r4=1; x=2; y=1;
25 :>2:r1=2; 2:r4=1; x=1; y=1;
74 :>2:r1=0; 2:r4=2; x=2; y=1;
158 :>2:r1=0; 2:r4=1; x=1; y=1;
107 :>2:r1=0; 2:r4=2; x=1; y=1;
1499 :>2:r1=0; 2:r4=1; x=1; y=2;
286 :>2:r1=0; 2:r4=2; x=1; y=2;
1798686:>2:r1=0; 2:r4=0; x=2; y=1;
135912:>2:r1=1; 2:r4=1; x=2; y=1;
5277557:>2:r1=1; 2:r4=1; x=1; y=2;
2716501:>2:r1=0; 2:r4=0; x=1; y=2;
11227952:>2:r1=2; 2:r4=2; x=2; y=1;
4214520:>2:r1=2; 2:r4=2; x=1; y=2;
2153927:>2:r1=2; 2:r4=2; x=1; y=1;
749952:>2:r1=1; 2:r4=1; x=1; y=1;
11722837:>2:r1=0; 2:r4=0; x=1; y=1;
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 45.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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r29,1
_litmus_P0_4_: stw r29,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test bclwdww011 Allowed
Histogram (7 states)
272555:>2:r1=1; 2:r3=0; y=1;
4645988:>2:r1=0; 2:r3=1; y=1;
11149144:>2:r1=0; 2:r3=1; y=2;
12471543:>2:r1=0; 2:r3=0; y=1;
10183739:>2:r1=1; 2:r3=1; y=1;
67255 :>2:r1=1; 2:r3=1; y=2;
1209776:>2:r1=0; 2:r3=0; y=2;
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 42.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: lwz r30,0(r2)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r9,0(r2)
Test bclwdww012 Allowed
Histogram (18 states)
92 :>2:r1=0; 2:r3=1; x=2; y=1;
1921 :>2:r1=2; 2:r3=1; x=1; y=1;
605 :>2:r1=2; 2:r3=1; x=2; y=1;
26812 :>2:r1=0; 2:r3=2; x=2; y=1;
1994 :>2:r1=1; 2:r3=2; x=1; y=2;
4559 :>2:r1=0; 2:r3=1; x=1; y=2;
15036 :>2:r1=0; 2:r3=2; x=1; y=2;
33509 :>2:r1=0; 2:r3=1; x=1; y=1;
29159 :>2:r1=0; 2:r3=2; x=1; y=1;
4039011:>2:r1=1; 2:r3=1; x=1; y=2;
2062742:>2:r1=2; 2:r3=2; x=1; y=1;
1930473:>2:r1=0; 2:r3=0; x=1; y=2;
5606695:>2:r1=2; 2:r3=2; x=1; y=2;
11710821:>2:r1=2; 2:r3=2; x=2; y=1;
1818977:>2:r1=0; 2:r3=0; x=2; y=1;
627575:>2:r1=1; 2:r3=1; x=1; y=1;
57744 :>2:r1=1; 2:r3=1; x=2; y=1;
12032275:>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 43.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r3,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
Test bclwdww013 Allowed
Histogram (3 states)
12248071:>1:r1=0; x=1;
28432280:>1:r1=1; x=1;
39319649:>1:r1=0; x=2;
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 35.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,2
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r3,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r29,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r30,1
_litmus_P3_3_: stw r30,0(r2)
Test bclwdww014 Allowed
Histogram (15 states)
2060 :>1:r1=1; 3:r1=0; x=2; z=2;
1815 :>1:r1=1; 3:r1=1; x=1; z=2;
1614 :>1:r1=1; 3:r1=1; x=2; z=1;
5838 :>1:r1=0; 3:r1=1; x=2; z=2;
488857:>1:r1=1; 3:r1=0; x=1; z=2;
793385:>1:r1=0; 3:r1=1; x=2; z=1;
455628:>1:r1=1; 3:r1=0; x=2; z=1;
514250:>1:r1=0; 3:r1=1; x=1; z=2;
4682894:>1:r1=0; 3:r1=0; x=2; z=2;
6284287:>1:r1=1; 3:r1=0; x=1; z=1;
7258088:>1:r1=0; 3:r1=0; x=1; z=2;
2555123:>1:r1=0; 3:r1=0; x=1; z=1;
6688786:>1:r1=0; 3:r1=1; x=1; z=1;
2133368:>1:r1=1; 3:r1=1; x=1; z=1;
8134007:>1:r1=0; 3:r1=0; 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=d40b4d76f7e7419bc76f118bb3639055
Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww014 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww014 62.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r3,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r11,r27,r27
_litmus_P3_2_: lwzx r30,r11,r2
Test bclwdww015 Allowed
Histogram (15 states)
4726 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
4024 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
22533 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
7220 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
621103:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
607588:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
996315:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1219561:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
2344447:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
6469066:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
7482896:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
7296579:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
4652373:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
2244148:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
6027421:>1:r1=1; 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=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 58.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r29,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r30,0(r2)
_litmus_P3_1_: xor r11,r30,r30
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww016 Allowed
Histogram (38 states)
4 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
11 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
9 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
21 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
37 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
87 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
7 :>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;
451 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
645 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
142 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
674 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
2868 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
1468 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
19243 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
922 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
769 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
21135 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
6837 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
38952 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
1312 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
81427 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
881830:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
594879:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
491447:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
42431 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
1535621:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
2943417:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
6688298:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
899559:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
4090517:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
4232752:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
352709:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
6166879:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
3215863:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1312837:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
4991132:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1382804:>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=cda2e0cac993408d5ce399f8c3bf25da
Cycle=DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww016 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpsR
Time bclwdww016 63.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r3,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww017 Allowed
Histogram (15 states)
4466 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
3490 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
12930 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
3180 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
583249:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
590431:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
621794:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1280608:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
7179702:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
7670084:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
4912365:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
5898805:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
2348268:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
6642432:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2248196:>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 58.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r29,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r30,1
_litmus_P1_3_: stw r30,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww018 Allowed
Histogram (41 states)
18 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
85 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
172 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
206 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
1512 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
40 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
104 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
411 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
1506 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
2400 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
19838 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
2393 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
5449 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
514 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1001 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
5818 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
38423 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
5020 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
30853 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
10984 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
16447 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
8021 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
27487 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
5297 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
6330 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
49939 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
243724:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
427857:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
438413:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1533349:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
732340:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
3529368:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
3067168:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
7778070:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
705260:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
7409982:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
5430431:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
3025099:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
1240626:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3309632:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
888413:>1:r1=1; 3:r1=1; 3:r3=1; 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=090f9e7edaad20d00811f89adff27ed2
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww018 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdRW
Time bclwdww018 67.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
Test bclwdww019 Allowed
Histogram (3 states)
21462731:>1:r1=1; 1:r4=1;
39450125:>1:r1=0; 1:r4=0;
19087144:>1:r1=0; 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 30.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r11,r27,r27
_litmus_P3_2_: lwzx r30,r11,r2
Test bclwdww020 Allowed
Histogram (15 states)
8249 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
4818 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
23220 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
16310 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
644454:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
670761:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1329875:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
5697774:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
6637280:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
2590291:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
6250782:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
6950549:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
1173051:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
1895268:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
6107318:>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 53.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r30,0(r2)
_litmus_P3_1_: xor r11,r30,r30
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww021 Allowed
Histogram (42 states)
3 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
12 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
13 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
12 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
174 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
50 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
1323 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
17 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
283 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
2323 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
23 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
397 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
198 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
81 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
195 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
342 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
324 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
2112 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
1132 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
173 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
810 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
151982:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
29174 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
27709 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
163967:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
51997 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
173797:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
658476:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
580428:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1087095:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
852557:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
3509276:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
5142505:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
2466053:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1322474:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
3265114:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
3047029:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
7006528:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
7686010:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
2044401:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
723429:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; 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 61.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww022 Allowed
Histogram (15 states)
4543 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
3576 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
28619 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
10315 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
464727:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
788542:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
4872695:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
1042432:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
5969324:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
1095882:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
6305490:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
2566951:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
7743284:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
7054488:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
2049132:>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 55.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww023 Allowed
Histogram (42 states)
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
29 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
1201 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
46 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
333 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
29 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
3853 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
424 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
95 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
357 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
8045 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
10267 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
7196 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
260 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
1246 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
50565 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
11151 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
42542 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1357 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
8049 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
2088 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
99827 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
3188 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
14448 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
562995:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
65803 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1035944:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
242012:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
87500 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
661251:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
2217351:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
703788:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
3337454:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
7149940:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3816287:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
4706687:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
2941021:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1139034:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
7232496:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
2899290:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
926528:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
8021 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; 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 63.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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r30,0(r2)
_litmus_P1_1_: xor r11,r30,r30
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r30,0(r2)
_litmus_P3_1_: xor r11,r30,r30
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww024 Allowed
Histogram (78 states)
1 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
5 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
4 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
4 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
17 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
16 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
10 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
30 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
35 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
6 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
13 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
28 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
35 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
42 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
159 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
94 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
265 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
99 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
278 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
53 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
51 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
125 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
194 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
76 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
475 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
359 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
112 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
138 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
438 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
137 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
1413 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
167 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
53 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
145 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
92 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
2556 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
68 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
4403 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
234 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
20708 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
13804 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
406 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
1861 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
214 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
104 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
2270 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
60553 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
1055 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
753 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
230887:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
230039:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
1883282:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
276849:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
441869:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
821863:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
921935:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
322641:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1985153:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
2611984:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
3197416:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
3605891:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
3792529:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
2998170:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
249494:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
3349432:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
7327832:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
643614:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
543132:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1605174:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
2215067:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
303984:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
251219:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
76378 :>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 66.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r30,0(r2)
_litmus_P1_1_: xor r11,r30,r30
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww025 Allowed
Histogram (38 states)
5 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
56 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
186 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
13 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
107 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
44 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
166 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
12 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
298 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
133 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
143 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
39 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
160 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
1506 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
36247 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
677 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
809 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
92638 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
24873 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
70932 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
604660:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
32460 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
177680:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
1944188:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
950226:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3688400:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
623559:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
2361992:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
852186:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
5156428:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
3299181:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
7025896:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
1392886:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7733215:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
849441:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
3078550:>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 59.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r30,0(r2)
_litmus_P1_1_: xor r11,r30,r30
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww026 Allowed
Histogram (85 states)
1 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
6 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
5 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
9 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
57 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
36 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
23 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
35 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
77 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
43 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
55 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
36 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
231 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
947 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
19 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
59 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
69 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
513 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
151 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
393 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
421 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
86 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
1553 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
843 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
21 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
801 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
257 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
414 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
883 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
93 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
64 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
37 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
226 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1545 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1814 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
7903 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
2740 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
20797 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
7541 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
16171 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
39812 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
7779 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
1440 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
17126 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
7155 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
10449 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
160551:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1830 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
7293 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
14001 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
50962 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
2223 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
3439 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
144161:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
524782:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
308067:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
648078:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
3013263:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
288686:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
452930:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
673448:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
605720:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
3500572:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
1797818:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
3382212:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1455805:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
343145:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
3643246:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
2118407:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
2676652:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
2635175:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
9149558:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
325720:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
206291:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
1715204:>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 71.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
Test bclwdww027 Allowed
Histogram (3 states)
12025506:>1:r1=0; 1:r3=1;
39874319:>1:r1=0; 1:r3=0;
28100175:>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 32.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww028 Allowed
Histogram (15 states)
4459 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
5255 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
15941 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
3809 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
865087:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
426604:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
815978:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
914889:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
6193109:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
4992422:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
8040995:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
2796554:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
7004765:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1844308:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
6075825:>1:r1=0; 1:r3=1; 3:r1=1; 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 55.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww029 Allowed
Histogram (42 states)
25 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
189 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
41 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
4102 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
1312 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
218 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
5201 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
54 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1188 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2934 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
245 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
5369 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
354 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
12584 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
925 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
1235 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
7415 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
21793 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
10091 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
592319:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
6132 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
89285 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
66688 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
10365 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
45781 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
518589:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
18019 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1049085:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1243562:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
2828731:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2342673:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
903695:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
3379027:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
6904538:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
5296356:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
1361455:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
8234242:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
4134316:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
104353:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
795503:>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 63.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,2
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r30,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r4,2
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r3,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww030 Allowed
Histogram (102 states)
1 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
5 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
28 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
2 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
5 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
8 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
57 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
7 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
8 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
22 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
70 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
11 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
117 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
133 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
24 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
211 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
3209 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
13 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
15 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
30 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
2390 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1870 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
5 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
688 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
876 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
4012 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
945 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1671 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1558 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
996 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
200 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
558 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
602 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
222 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
688 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1577 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1136 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1323 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
199 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1315 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
8806 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
27998 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
501 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
7539 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
548 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
10447 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
12649 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
926 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
34163 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
16791 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
6713 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
19218 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1252 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
27183 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
8719 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
6173 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
7849 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
45396 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
20438 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
2198 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
35564 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
289319:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
8770 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
3553 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
3748 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
879956:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
14680 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
18529 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
14404 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
189707:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
334126:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1876508:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
443954:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
240879:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
1805799:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
2431557:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
2581406:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3494048:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
3480755:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1604292:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
369307:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
622650:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
3154733:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3556215:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
620927:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1799897:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
9247606:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
176980:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
179310:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
228476:>1:r1=1; 1:r3=1; 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: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 75.77
$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 -O */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 -O"
LITMUSOPTS=-r 40 -v
Sun Dec 27 16:12:19 CET 2009