Wed Dec 23 08:25:41 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)
19472514:>1:r1=0; x=2;
14194095:>1:r1=1; x=1;
6333391:>1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 19.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5427 :>1:r1=0; 3:r1=1; x=2; z=2;
1491 :>1:r1=1; 3:r1=1; x=1; z=2;
1539 :>1:r1=1; 3:r1=1; x=2; z=1;
3693 :>1:r1=1; 3:r1=0; x=2; z=2;
279168:>1:r1=1; 3:r1=0; x=1; z=2;
439944:>1:r1=0; 3:r1=1; x=1; z=2;
334876:>1:r1=0; 3:r1=1; x=2; z=1;
509342:>1:r1=1; 3:r1=0; x=2; z=1;
3231569:>1:r1=1; 3:r1=0; x=1; z=1;
3540810:>1:r1=0; 3:r1=0; x=1; z=2;
3834680:>1:r1=0; 3:r1=0; x=2; z=1;
3307375:>1:r1=0; 3:r1=1; x=1; z=1;
2092915:>1:r1=0; 3:r1=0; x=2; z=2;
1546149:>1:r1=1; 3:r1=1; x=1; z=1;
871022:>1:r1=0; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 41.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
777 :>1:r1=1; 3:r1=1; x=1; z=2;
733 :>1:r1=1; 3:r1=1; x=2; z=1;
1500 :>1:r1=1; 3:r1=0; x=2; z=2;
9552 :>1:r1=0; 3:r1=1; x=2; z=2;
302738:>1:r1=1; 3:r1=0; x=1; z=2;
449999:>1:r1=0; 3:r1=1; x=2; z=1;
511862:>1:r1=0; 3:r1=1; x=1; z=2;
4037133:>1:r1=0; 3:r1=0; x=2; z=1;
2897578:>1:r1=0; 3:r1=0; x=2; z=2;
1101447:>1:r1=0; 3:r1=0; x=1; z=1;
3065319:>1:r1=0; 3:r1=1; x=1; z=1;
3086710:>1:r1=0; 3:r1=0; x=1; z=2;
222975:>1:r1=1; 3:r1=0; x=2; z=1;
842386:>1:r1=1; 3:r1=1; x=1; z=1;
3469291:>1:r1=1; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 40.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3772 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
6030 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
2694 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
13614 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
782460:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
375254:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
270506:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
623004:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
3721772:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
3780332:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
982177:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
1888671:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
3321133:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1369719:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
2858862:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 40.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (40 states)
3 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
12 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
9 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
51 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
8 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
18 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
326 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
234 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
4 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
667 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
107 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
492 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
111 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
125 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
241 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
179 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
105 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
18766 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
112 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
15082 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
257 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
19829 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
252038:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
160 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
88903 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
589405:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
152084:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
122571:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
785732:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
347787:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
1690947:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3705072:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
1535835:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
324101:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
1634683:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1841868:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
425106:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3281374:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
2515292:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
650304:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 56.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1861 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1599 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
10722 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
3682 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
264052:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
457416:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
2131083:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
418736:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
571990:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
3903291:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
3131066:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
3516908:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
3379010:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
1024021:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1184563:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
1039 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
3277 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
23 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
19867 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
48 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
161 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
115 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1216 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
69 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
346 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
3492 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
39 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
10677 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
63359 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
13754 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
29916 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
6096 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
11571 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
1865 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
3886 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
16299 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
15904 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
204819:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
73728 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
114160:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
23622 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
600677:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
47361 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
253207:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1828912:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
267235:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1664456:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
2611155:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
1685139:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
3745074:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
1348411:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
490052:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3357893:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
1025575:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
443959:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
11545 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 56.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
91735 :>2:r1=1; x=2; y=1;
81028 :>2:r1=1; x=1; y=2;
327690:>2:r1=0; x=2; y=2;
5935700:>2:r1=0; x=1; y=2;
1998527:>2:r1=0; x=1; y=1;
5654504:>2:r1=1; x=1; y=1;
5910816:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 32.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
98706 :>2:r1=1; x=2; y=1;
6250010:>2:r1=0; x=2; y=1;
6015381:>2:r1=0; x=1; y=2;
2136413:>2:r1=0; x=1; y=1;
5091713:>2:r1=1; x=1; y=1;
35731 :>2:r1=1; x=1; y=2;
372046:>2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 28.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
278583:>2:r1=0; 2:r4=0; y=2;
170463:>2:r1=1; 2:r4=0; y=1;
5113639:>2:r1=0; 2:r4=1; y=2;
6345969:>2:r1=0; 2:r4=0; y=1;
5512784:>2:r1=1; 2:r4=1; y=1;
150453:>2:r1=1; 2:r4=1; y=2;
2428109:>2:r1=0; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 29.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww010
"DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | lwzx r4,r3,r2 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r2)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: lwzx r9,r11,r2
Test bclwdww010 Allowed
Histogram (18 states)
18 :>2:r1=0; 2:r4=1; x=2; y=1;
47 :>2:r1=0; 2:r4=2; x=2; y=1;
190 :>2:r1=0; 2:r4=1; x=1; y=2;
979 :>2:r1=2; 2:r4=1; x=2; y=1;
138 :>2:r1=0; 2:r4=2; x=1; y=2;
2709 :>2:r1=1; 2:r4=2; x=1; y=2;
1304 :>2:r1=2; 2:r4=1; x=1; y=1;
357 :>2:r1=0; 2:r4=1; x=1; y=1;
798611:>2:r1=0; 2:r4=0; x=2; y=1;
1089366:>2:r1=0; 2:r4=0; x=1; y=2;
2581714:>2:r1=1; 2:r4=1; x=1; y=2;
1127375:>2:r1=2; 2:r4=2; x=1; y=1;
2347526:>2:r1=2; 2:r4=2; x=1; y=2;
5722511:>2:r1=2; 2:r4=2; x=2; y=1;
5844783:>2:r1=0; 2:r4=0; x=1; y=1;
447857:>2:r1=1; 2:r4=1; x=1; y=1;
34402 :>2:r1=1; 2:r4=1; x=2; y=1;
113 :>2:r1=0; 2:r4=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 32.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
57085 :>2:r1=1; 2:r3=1; y=2;
209168:>2:r1=1; 2:r3=0; y=1;
331251:>2:r1=0; 2:r3=0; y=2;
5590089:>2:r1=0; 2:r3=1; y=2;
6429476:>2:r1=0; 2:r3=0; y=1;
5353689:>2:r1=1; 2:r3=1; y=1;
2029242:>2:r1=0; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 29.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
32 :>2:r1=0; 2:r3=1; x=2; y=1;
533 :>2:r1=2; 2:r3=1; x=2; y=1;
454 :>2:r1=1; 2:r3=2; x=1; y=2;
1195 :>2:r1=2; 2:r3=1; x=1; y=1;
8433 :>2:r1=0; 2:r3=1; x=1; y=2;
29382 :>2:r1=0; 2:r3=1; x=1; y=1;
1859 :>2:r1=0; 2:r3=2; x=2; y=1;
21863 :>2:r1=0; 2:r3=2; x=1; y=2;
818903:>2:r1=0; 2:r3=0; x=2; y=1;
2264162:>2:r1=2; 2:r3=2; x=1; y=2;
2301666:>2:r1=1; 2:r3=1; x=1; y=2;
1055818:>2:r1=2; 2:r3=2; x=1; y=1;
1337961:>2:r1=0; 2:r3=0; x=1; y=2;
5815482:>2:r1=2; 2:r3=2; x=2; y=1;
5867090:>2:r1=0; 2:r3=0; x=1; y=1;
436645:>2:r1=1; 2:r3=1; x=1; y=1;
26941 :>2:r1=1; 2:r3=1; x=2; y=1;
11581 :>2:r1=0; 2:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 32.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
10947868:>1:r1=0; x=1;
12698226:>1:r1=1; x=1;
16353906:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
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 21.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1154 :>1:r1=1; 3:r1=1; x=1; z=2;
900 :>1:r1=1; 3:r1=1; x=2; z=1;
1230 :>1:r1=1; 3:r1=0; x=2; z=2;
2448 :>1:r1=0; 3:r1=1; x=2; z=2;
243277:>1:r1=1; 3:r1=0; x=1; z=2;
205344:>1:r1=1; 3:r1=0; x=2; z=1;
212458:>1:r1=0; 3:r1=1; x=1; z=2;
340884:>1:r1=0; 3:r1=1; x=2; z=1;
2434046:>1:r1=0; 3:r1=0; x=2; z=2;
3973030:>1:r1=0; 3:r1=0; x=2; z=1;
1281688:>1:r1=0; 3:r1=0; x=1; z=1;
3470581:>1:r1=0; 3:r1=1; x=1; z=1;
3474583:>1:r1=0; 3:r1=0; x=1; z=2;
3328269:>1:r1=1; 3:r1=0; x=1; z=1;
1030108:>1:r1=1; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 41.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2821 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
12843 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
2415 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
2206 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
298268:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
377332:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
832857:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
2111989:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
2924716:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
986800:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
548639:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
3840904:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
3911013:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
1200283:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
2946914:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww016
"DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww016 Allowed
Histogram (37 states)
4 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
16 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
12 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
24 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
5 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
23 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
6 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
2 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
811 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
51 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
161 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
84 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
2374 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
528 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
224 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
262 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
15302 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
396 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
10023 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
14137 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
209691:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
20536 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
757512:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
1916577:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
370118:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
27675 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
243186:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
644736:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
3169736:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
383431:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
696895:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1869026:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
2741978:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1504801:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1862476:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
123239:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
3413942:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 53.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2226 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
9449 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
2439 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1627 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
270776:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
255441:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
371177:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
717690:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1938015:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
2979928:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
4010654:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
3498097:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1236239:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
1261646:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
3444596:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
16 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
315 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
10 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
39 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
80 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1320 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
357 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
83936 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
738 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
55 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
13412 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
11624 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
10493 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
1694 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
15210 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
2634 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
8314 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
22448 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
10864 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
4315 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
4513 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
29596 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
39214 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
276178:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
536 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
15645 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
8367 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
141927:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
172717:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
341861:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
827038:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
1396092:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
1581067:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
330180:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3748535:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
2759758:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
1692350:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
528082:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3492940:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
1894673:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
530856:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 61.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
9087323:>1:r1=0; 1:r4=1;
18399104:>1:r1=0; 1:r4=0;
12513573:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 19.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
8415 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
15072 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
4392 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
435172:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
6068 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
593430:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
280643:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
660600:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
3289381:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
2099626:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
3666861:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
972264:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
3454542:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
1382997:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
3130537:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 38.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
1 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
1 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
16 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
5 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
89 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
102 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
60 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
8 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
93 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
90 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
87 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
73 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
125 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
129 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
205 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
1043 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
54359 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
319 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
26667 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
16725 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
47163 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
126 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
332395:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
180921:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
272825:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
412293:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
1445157:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
522166:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
25670 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
411052:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1280794:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1395174:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
3051342:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
1528179:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
3686409:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2376362:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
763300:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
2168471:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 58.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2909 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
2227 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
4812 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
5288 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
282341:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
399530:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
588664:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
518989:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
3143178:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
3812607:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
1382649:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
3645029:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
2033770:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
1080882:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
3097125:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww023
"LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww023 Allowed
Histogram (42 states)
9 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
264 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
3 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
31 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
127 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
203 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
879 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
32 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
108 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
14924 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
22579 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
5266 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
5232 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
1122 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
29720 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
18010 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
10132 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
21866 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1028 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
1530 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
219059:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
29393 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
12356 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
4532 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
3911 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
14531 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
287599:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
15714 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
456206:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
157879:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1281606:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
29467 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
2091411:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
345085:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1489540:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
569777:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
2451062:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
1405837:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
3800804:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3082172:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1581293:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
537701:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 59.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (72 states)
1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
3 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
9 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
22 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
16 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
25 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
36 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
12 :>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;
3 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
12 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
44 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
40 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
20 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
88 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
64 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
40 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
7 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
18 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
65 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
177 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
14 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
112 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
124 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
99 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
53 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
11 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
64 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
757 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
13 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
12 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
28 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
338 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
192 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
13 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
8734 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
241 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
233 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
581 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
613 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
36867 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
12843 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
1845 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
89131 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
18262 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
97250 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
156820:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
158536:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
758881:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
415896:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
349349:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
1139380:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1565270:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
163706:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1499515:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
1449752:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
294410:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1903502:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
1798211:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
4280173:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
159445:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
277512:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
816808:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
969606:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
300602:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
156503:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
1116967:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 82.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (38 states)
1 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
5 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
6 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
33 :>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=1; y=2;
56 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
107 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
52 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
465 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
115 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
994 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
14260 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
66870 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
17029 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
209083:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
102953:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
22358 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
43 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
67670 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
288878:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
688190:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
552928:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
1610675:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
1339572:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
410502:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3051861:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
611233:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
3387032:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
1868838:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
2730959:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
2190740:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
766423:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 53.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (79 states)
1 :>1:r1=2; 1:r4=1; 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;
2 :>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=2;
1 :>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=2; x=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
5 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
11 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
50 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
11 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
60 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
25 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
11 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
29 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
30 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
36 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
55 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
136 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
376 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
74 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
20 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
731 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
75 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
3168 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
234 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
2336 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
1451 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
772 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
839 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
74 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
225 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
18582 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
821 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
5357 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
462 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
3097 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
480 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
10508 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
12 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
2427 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
5638 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
8454 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
8881 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
24673 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
29995 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
104340:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
31216 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
29775 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
119275:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
12785 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
82800 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
80669 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
138701:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
388802:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
791334:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
1856122:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
108322:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
153674:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1152096:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
975956:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
847680:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
1544881:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
305148:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1747920:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
1170075:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
1342734:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
96002 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
250207:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
1564950:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
4289653:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
324423:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
125116:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
218819:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
16283 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 84.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5617724:>1:r1=0; 1:r3=1;
19168402:>1:r1=0; 1:r3=0;
15213874:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 18.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2957 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
2708 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
12181 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
8728 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
324038:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
439755:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
642426:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
678362:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
2473540:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1219568:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
3194333:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3616898:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3216749:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
896450:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
3271307:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww029
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww029 Allowed
Histogram (42 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
14 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
294 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1276 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
32 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
39 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
15 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
8132 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
146 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
78 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
575 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
5865 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
487 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
14735 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
3239 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
2707 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
3116 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
8131 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
43562 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
2950 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
26504 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
12717 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
5631 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
13254 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
210941:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
10712 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
44156 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
289057:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
29342 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
509599:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1978524:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
628552:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
3570952:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
1172156:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
94011 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1863582:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1515149:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
702861:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3552606:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2734945:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
529370:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
409985:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 54.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
15 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
14 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
5 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
13 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
29 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
473 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
73 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
15 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
5 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
245 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
51 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
177 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
572 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2737 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
29 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
8 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
13236 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
3944 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
469 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
125 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
19 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
229 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
865 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1115 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
260 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
663 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
168 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
43 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
31 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
128 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2955 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
894 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
652 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
582 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
137 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
177 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
276 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
56188 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
31789 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
10 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
93 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
2128 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
4157 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1693 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
274 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
581 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
2290 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
7562 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
3114 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1857 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2503 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
7528 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
2779 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
3911 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
4328 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
14111 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
22915 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
4994 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
55236 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
719 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
21366 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
9887 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
123 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
24304 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
23050 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
1767 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
10642 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
22 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
32138 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
84937 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
66344 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
3100 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
13995 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
21117 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
57270 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
127418:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
65603 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
17207 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
16128 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
97269 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
261764:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
835839:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
89815 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
1942158:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1370919:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
926607:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
193254:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1321343:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
4372787:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
294364:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1980543:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
966525:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
909900:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
1314895:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1163170:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
363311:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
359415:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
132949:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
244516:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
31 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 114.61
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Wed Dec 23 08:49:01 CET 2009