Tue Dec 29 15:29: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 r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,r2
Test bclwdww000 Allowed
Histogram (3 states)
20864770:>1:r1=0; x=1;
25052872:>1:r1=1; x=1;
34082358:>1:r1=0; x=2;
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.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r11,0(r9)
_litmus_P3_1_: xor r10,r11,r11
_litmus_P3_2_: li r8,1
_litmus_P3_3_: stwx r8,r10,r2
Test bclwdww001 Allowed
Histogram (15 states)
11776 :>1:r1=0; 3:r1=1; x=2; z=2;
3107 :>1:r1=1; 3:r1=1; x=2; z=1;
6007 :>1:r1=1; 3:r1=0; x=2; z=2;
3187 :>1:r1=1; 3:r1=1; x=1; z=2;
647652:>1:r1=1; 3:r1=0; x=1; z=2;
967219:>1:r1=0; 3:r1=1; x=1; z=2;
877177:>1:r1=0; 3:r1=1; x=2; z=1;
795035:>1:r1=1; 3:r1=0; x=2; z=1;
6823042:>1:r1=0; 3:r1=0; x=1; z=2;
6549186:>1:r1=1; 3:r1=0; x=1; z=1;
1587920:>1:r1=0; 3:r1=0; x=1; z=1;
4437615:>1:r1=0; 3:r1=0; x=2; z=2;
7590672:>1:r1=0; 3:r1=0; x=2; z=1;
2820347:>1:r1=1; 3:r1=1; x=1; z=1;
6880058:>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 63.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r11,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)
2968 :>1:r1=1; 3:r1=1; x=2; z=1;
3151 :>1:r1=1; 3:r1=0; x=2; z=2;
2869 :>1:r1=1; 3:r1=1; x=1; z=2;
10551 :>1:r1=0; 3:r1=1; x=2; z=2;
595684:>1:r1=1; 3:r1=0; x=1; z=2;
533441:>1:r1=1; 3:r1=0; x=2; z=1;
794564:>1:r1=0; 3:r1=1; x=2; z=1;
851461:>1:r1=0; 3:r1=1; x=1; z=2;
4862758:>1:r1=0; 3:r1=0; x=2; z=2;
6993623:>1:r1=1; 3:r1=0; x=1; z=1;
6683846:>1:r1=0; 3:r1=1; x=1; z=1;
1969610:>1:r1=0; 3:r1=0; x=1; z=1;
6847587:>1:r1=0; 3:r1=0; x=1; z=2;
7491932:>1:r1=0; 3:r1=0; x=2; z=1;
2355955:>1:r1=1; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=f222837c1b9c320fc4731d82df04c0c8
Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww002 No BCLwSyncdWW
Safe=Wse LwSyncdRW DpdW
Time bclwdww002 63.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww003
"DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r11,0(r9)
_litmus_P3_1_: xor r8,r11,r11
_litmus_P3_2_: lwzx r10,r8,r2
Test bclwdww003 Allowed
Histogram (15 states)
10935 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
6074 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
7889 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
12543 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
654702:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1840444:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1568205:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
5677507:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
7709875:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
6765942:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1549985:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
4514869:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
6016691:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
2997297:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
667042:>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 58.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww004
"DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r2 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r9,0(r2)
_litmus_P3_1_: xor r10,r9,r9
_litmus_P3_2_: lwzx r11,r10,r2
Test bclwdww004 Allowed
Histogram (35 states)
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
4 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
24 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
27 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
152 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
457 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
156 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
8 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
42 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
437 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
85 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
106 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
200 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
715 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
49390 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
47566 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
1842 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
39261 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
24565 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
77782 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
475720:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
3127535:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
800437:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
692421:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
6184340:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
2391899:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
1323595:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
3795094:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1061125:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
2810845:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
7483611:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4998402:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
3711467:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
420096:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
480593:>1:r1=1; 3:r1=2; 3:r4=2; y=2; 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 60.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test bclwdww005 Allowed
Histogram (15 states)
5250 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
3413 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
13233 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
9153 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
554208:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
652938:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
912991:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
6433466:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
7147262:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
7471336:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1847454:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
4722136:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
6492593:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2663546:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1071021:>1:r1=1; 3:r1=0; 3:r3=0; 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.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r10,r11,r11
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r10,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww006 Allowed
Histogram (41 states)
387 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
25 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
337 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
1212 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
49 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
2734 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
300 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
225 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1947 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
2379 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
417 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
4489 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
1854 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
3972 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
15557 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
7767 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
41683 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
9796 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
11082 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
53090 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
50746 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
32791 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
16153 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
548102:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
8219 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
45307 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
466060:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
896067:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
3364793:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
286701:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
598949:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3329650:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
2385959:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
64842 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
845798:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3392093:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
2842084:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
7711379:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
7139762:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
4894786:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
920457:>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=355c23adb39c4f8a03f27206e6d5ad02
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww006 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR DpdW
Time bclwdww006 64.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: xor r10,r11,r11
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stwx r8,r10,r2
Test bclwdww007 Allowed
Histogram (7 states)
245070:>2:r1=1; x=2; y=1;
920539:>2:r1=0; x=2; y=2;
3250120:>2:r1=0; x=1; y=1;
12066970:>2:r1=0; x=2; y=1;
11343349:>2:r1=1; x=1; y=1;
239940:>2:r1=1; x=1; y=2;
11934012:>2:r1=0; x=1; 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 44.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li r10,1
_litmus_P2_3_: stw r10,0(r2)
Test bclwdww008 Allowed
Histogram (7 states)
162328:>2:r1=1; x=2; y=1;
12169197:>2:r1=0; x=2; y=1;
11668762:>2:r1=0; x=1; y=2;
4387467:>2:r1=0; x=1; y=1;
11060532:>2:r1=1; x=1; y=1;
169140:>2:r1=1; x=1; y=2;
382574:>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=82e869524c51deb209a9e10f0c829a0c
Cycle=LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww008 No BCLwSyncdWW
Safe=Wse LwSyncdWW LwSyncdRW
Time bclwdww008 44.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: xor r8,r11,r11
_litmus_P2_2_: lwzx r10,r8,r2
Test bclwdww009 Allowed
Histogram (7 states)
1924596:>2:r1=0; 2:r4=0; y=2;
394947:>2:r1=1; 2:r4=0; y=1;
4135427:>2:r1=0; 2:r4=1; y=1;
12072728:>2:r1=0; 2:r4=0; y=1;
10714103:>2:r1=1; 2:r4=1; y=1;
305183:>2:r1=1; 2:r4=1; y=2;
10453016:>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.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r9,0(r2)
_litmus_P2_1_: xor r10,r9,r9
_litmus_P2_2_: lwzx r11,r10,r2
Test bclwdww010 Allowed
Histogram (16 states)
3 :>2:r1=2; 2:r4=1; x=2; y=1;
4 :>2:r1=2; 2:r4=1; x=1; y=1;
75 :>2:r1=0; 2:r4=2; x=2; y=1;
528 :>2:r1=0; 2:r4=2; x=1; y=2;
958 :>2:r1=0; 2:r4=2; x=1; y=1;
917 :>2:r1=0; 2:r4=1; x=1; y=2;
3910 :>2:r1=0; 2:r4=1; x=1; y=1;
4609258:>2:r1=1; 2:r4=1; x=1; y=2;
2250292:>2:r1=0; 2:r4=0; x=2; y=1;
2159271:>2:r1=2; 2:r4=2; x=1; y=1;
11647279:>2:r1=2; 2:r4=2; x=2; y=1;
5201443:>2:r1=2; 2:r4=2; x=1; y=2;
11137801:>2:r1=0; 2:r4=0; x=1; y=1;
913532:>2:r1=1; 2:r4=1; x=1; y=1;
119093:>2:r1=1; 2:r4=1; x=2; y=1;
1955636:>2:r1=0; 2:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3b6264a86335c33f3b93e442e8f4ad38
Cycle=DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww010 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpsR
Time bclwdww010 44.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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r2)
Test bclwdww011 Allowed
Histogram (7 states)
289493:>2:r1=1; 2:r3=0; y=1;
10577220:>2:r1=0; 2:r3=1; y=2;
4921190:>2:r1=0; 2:r3=1; y=1;
12450565:>2:r1=0; 2:r3=0; y=1;
10447147:>2:r1=1; 2:r3=1; y=1;
96872 :>2:r1=1; 2:r3=1; y=2;
1217513:>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.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: lwz r9,0(r2)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r11,0(r2)
Test bclwdww012 Allowed
Histogram (18 states)
128 :>2:r1=0; 2:r3=1; x=2; y=1;
85033 :>2:r1=1; 2:r3=2; x=1; y=2;
9125 :>2:r1=0; 2:r3=2; x=1; y=2;
3677 :>2:r1=2; 2:r3=1; x=1; y=1;
13239 :>2:r1=0; 2:r3=2; x=1; y=1;
10667 :>2:r1=0; 2:r3=1; x=1; y=1;
4152 :>2:r1=0; 2:r3=2; x=2; y=1;
6231 :>2:r1=2; 2:r3=1; x=2; y=1;
1868 :>2:r1=0; 2:r3=1; x=1; y=2;
2327891:>2:r1=0; 2:r3=0; x=1; y=2;
2161808:>2:r1=2; 2:r3=2; x=1; y=1;
4984452:>2:r1=1; 2:r3=1; x=1; y=2;
2033489:>2:r1=0; 2:r3=0; x=2; y=1;
693278:>2:r1=1; 2:r3=1; x=1; y=1;
11419501:>2:r1=2; 2:r3=2; x=2; y=1;
4543457:>2:r1=2; 2:r3=2; x=1; y=2;
89920 :>2:r1=1; 2:r3=1; x=2; y=1;
11612084:>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 45.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,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)
25657672:>1:r1=0; x=1;
32841206:>1:r1=0; x=2;
21501122:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=4d1c1648955365c08b4c97b22a8d5408
Cycle=LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww013 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww013 34.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,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 r11,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)
2829 :>1:r1=1; 3:r1=1; x=1; z=2;
2242 :>1:r1=1; 3:r1=0; x=2; z=2;
2583 :>1:r1=1; 3:r1=1; x=2; z=1;
4521 :>1:r1=0; 3:r1=1; x=2; z=2;
697069:>1:r1=0; 3:r1=1; x=2; z=1;
545118:>1:r1=0; 3:r1=1; x=1; z=2;
547011:>1:r1=1; 3:r1=0; x=1; z=2;
4757312:>1:r1=0; 3:r1=0; x=2; z=2;
6632225:>1:r1=1; 3:r1=0; x=1; z=1;
6759863:>1:r1=0; 3:r1=1; x=1; z=1;
7993649:>1:r1=0; 3:r1=0; x=2; z=1;
7020407:>1:r1=0; 3:r1=0; x=1; z=2;
2189860:>1:r1=0; 3:r1=0; x=1; z=1;
414865:>1:r1=1; 3:r1=0; x=2; z=1;
2430446:>1:r1=1; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d40b4d76f7e7419bc76f118bb3639055
Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww014 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww014 63.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,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 r11,0(r9)
_litmus_P3_1_: xor r8,r11,r11
_litmus_P3_2_: lwzx r10,r8,r2
Test bclwdww015 Allowed
Histogram (15 states)
6700 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
6707 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
5422 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
14864 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
732943:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
631280:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1304402:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
4527681:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
1703092:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
7208283:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
5424655:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1755538:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
5931556:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
2827787:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
7919090:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 59.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,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 r9,0(r2)
_litmus_P3_1_: xor r10,r9,r9
_litmus_P3_2_: lwzx r11,r10,r2
Test bclwdww016 Allowed
Histogram (38 states)
2 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
5 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
8 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
10 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
9 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
30 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
14 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
114 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
119 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
1048 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
116 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
108 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
116 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
2925 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
223 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
980 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
36370 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
25837 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
28433 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
56935 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
30236 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
400925:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
443545:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
680763:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
3375214:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3085586:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1670235:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
1452065:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
1075012:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
4038334:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
7070640:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
3526170:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
6898774:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4886756:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
776569:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
435772:>1:r1=1; 3:r1=2; 3:r4=2; y=2; 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 61.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww017
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r11,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 r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test bclwdww017 Allowed
Histogram (15 states)
3866 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
5621 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
12699 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
4965 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
677074:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
677686:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
7379385:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1133073:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
5940439:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
7587831:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2206450:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
4998346:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
6431274:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2326842:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
614449:>1:r1=0; 3:r1=1; 3:r3=0; 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.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww018 Allowed
Histogram (41 states)
16 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
300 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
390 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
1484 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
81 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
7540 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
351 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
25 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
470 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
14463 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
2532 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1847 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
5845 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
395 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
11020 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
13427 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
2425 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
35800 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
3234 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
12719 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
28317 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
388220:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
43899 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
36023 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
210549:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
30002 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
26308 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
789331:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
424376:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1441454:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
668796:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3573975:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
1254515:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
2925494:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
2763164:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
3676213:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
7328350:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
8012750:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
5389134:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
867117:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
7649 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=090f9e7edaad20d00811f89adff27ed2
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww018 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdRW
Time bclwdww018 64.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r8,r11,r11
_litmus_P1_2_: lwzx r10,r8,r2
Test bclwdww019 Allowed
Histogram (3 states)
14852952:>1:r1=0; 1:r4=1;
39099104:>1:r1=0; 1:r4=0;
26047944:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 80000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=76deedad5ea71bc51dc86d1d5214c15b
Cycle=DpdR Fre LwSyncdWW Rfe
Relax bclwdww019 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww019 30.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r8,r11,r11
_litmus_P1_2_: lwzx r10,r8,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 r11,0(r9)
_litmus_P3_1_: xor r8,r11,r11
_litmus_P3_2_: lwzx r10,r8,r2
Test bclwdww020 Allowed
Histogram (15 states)
10829 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
15876 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
11492 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
24595 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
784244:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1412883:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
553817:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
1632477:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
6317401:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
6909843:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
1775095:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
5079835:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
6213545:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
3119659:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
6138409:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=95bd88b4aecb95238880fff470fdbcc8
Cycle=DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww020 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww020 55.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r8,r11,r11
_litmus_P1_2_: lwzx r10,r8,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 r9,0(r2)
_litmus_P3_1_: xor r10,r9,r9
_litmus_P3_2_: lwzx r11,r10,r2
Test bclwdww021 Allowed
Histogram (35 states)
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
6 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
14 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
14 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
31 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
267 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
38 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
20 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
290 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
33 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
93 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
97 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
1427 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
91 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
656 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
99336 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
117558:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
608032:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
51058 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
34366 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
83973 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
641100:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
3853996:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
353843:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1012060:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
2448864:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
757341:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
2755535:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
4657180:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
2882139:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
977456:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
6900321:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
3038048:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
953290:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
7771426:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26c4ea0f855245b74a15911ba593704d
Cycle=DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww021 No BCLwSyncdWW
Safe=Fre DpsR DpdR
Time bclwdww021 59.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r8,r11,r11
_litmus_P1_2_: lwzx r10,r8,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 r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test bclwdww022 Allowed
Histogram (15 states)
6212 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
5465 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
8586 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
20854 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
877381:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
1297750:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
505031:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
5145249:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
7113313:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
6401426:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
1872183:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
5877200:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
6865838:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
2488206:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
1515306:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=18c468c9529c924b0b9eadcf19d0bf8c
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww022 No BCLwSyncdWW
Safe=Fre LwSyncdRR DpdR
Time bclwdww022 55.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: xor r8,r11,r11
_litmus_P1_2_: lwzx r10,r8,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww023 Allowed
Histogram (42 states)
3 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
27 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
222 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
507 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
43 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
1735 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
1425 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
6294 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
387 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
1651 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
2006 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
200 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
998 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
8748 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
2532 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
8803 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
31170 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
11376 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
19997 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
4116 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
59704 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
11104 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
16888 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
3894 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
975231:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
582282:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
138261:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
312966:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
152036:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
2926743:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
2405047:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
3950185:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
82489 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
7606732:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
705756:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
3059674:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
2958635:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1034967:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
6569813:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
4789903:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
898589:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
656861:>1:r1=0; 1:r4=1; 3:r1=1; 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 62.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,0(r2)
_litmus_P1_1_: xor r10,r9,r9
_litmus_P1_2_: lwzx r11,r10,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 r9,0(r2)
_litmus_P3_1_: xor r10,r9,r9
_litmus_P3_2_: lwzx r11,r10,r2
Test bclwdww024 Allowed
Histogram (67 states)
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
1 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
5 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
2 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
11 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
2 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
7 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
12 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
28 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
11 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
64 :>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;
13 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
168 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
20 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
86 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
21 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
8 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
15 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
40 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
5 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
43 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
300 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
6 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
59 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
56 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
239 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
140 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
76 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
53 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
1360 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
1047 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
296836:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
39 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
23486 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
27089 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
54812 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
52813 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
313087:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
502337:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
358731:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
283334:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
3474870:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
294711:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1910247:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
1582586:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
707376:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
2522253:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
2117445:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
258382:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
3420374:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
3293287:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
3593661:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
2458262:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
508951:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
9027810:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
1686157:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
239001:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
247195:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
740915:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=d9cb89dae7c1c7340715ada64130ec5d
Cycle=DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww024 No BCLwSyncdWW
Safe=Fre DpsR
Time bclwdww024 64.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,0(r2)
_litmus_P1_1_: xor r10,r9,r9
_litmus_P1_2_: lwzx r11,r10,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 r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test bclwdww025 Allowed
Histogram (36 states)
1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
6 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
4 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
26 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
80 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
99 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
37 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
92 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
16 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
43 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
12 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
1366 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
649 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
101 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
31086 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
25198 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
293 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
45785 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
186684:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
619739:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
100227:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
687547:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
2156390:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
94353 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
2525112:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
843833:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3187673:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
859702:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
4064130:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
1272682:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7240881:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
5118628:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
7023306:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
824895:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
3089321:>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 57.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,0(r2)
_litmus_P1_1_: xor r10,r9,r9
_litmus_P1_2_: lwzx r11,r10,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww026 Allowed
Histogram (74 states)
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
9 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
23 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
26 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
8 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
27 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
26 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
86 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
9 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
17 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
47 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
105 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
10 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
60 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
129 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
305 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
61 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
128 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
1608 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
3886 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
3175 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
17 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
875 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
835 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
426 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
786 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
1978 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1355 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1243 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
2118 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
1669 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
15026 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
2596 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1922 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
7676 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
13615 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
31351 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
4951 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
8111 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
222789:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
201145:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
54041 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
42123 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
19487 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
22932 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
59455 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
469558:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
16222 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
265314:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
686985:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1721329:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
250268:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
2429443:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
334844:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
2710470:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
698900:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
3318155:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1788474:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
1616711:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
3021802:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3531489:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
3695289:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
2235043:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
584488:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
557544:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
8716806:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
358928:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
230045:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
33607 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=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: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 66.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,0(r2)
Test bclwdww027 Allowed
Histogram (3 states)
22982711:>1:r1=0; 1:r3=1;
20739711:>1:r1=1; 1:r3=1;
36277578:>1:r1=0; 1:r3=0;
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 31.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,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 r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test bclwdww028 Allowed
Histogram (15 states)
3998 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
4163 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
14147 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
569053:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
13075 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1153910:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
718977:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1216886:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
6564717:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
4521891:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
7431540:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
2234987:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
6939886:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
2255681:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
6357089:>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 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 r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww029 Allowed
Histogram (42 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
8 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
49 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
249 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
272 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2564 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
1289 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
145 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
8330 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
4125 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
2170 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
3663 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
9771 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
372 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
714 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
19935 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
19578 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
27184 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
14209 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
2623 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
29819 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
17686 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
4487 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
626212:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
11674 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
692867:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
226192:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
87523 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
24987 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1958439:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
851538:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
7200088:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3025360:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
89183 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
2628801:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1276202:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
6717932:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2930939:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
4580847:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
5129665:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
917229:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
855079:>1:r1=0; 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 61.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r11,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 r9,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r11,0(r2)
Test bclwdww030 Allowed
Histogram (103 states)
1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
11 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2 :>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=2; y=1;
16 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
7 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
14 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
183 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
72 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
8 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
15 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
7 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
72 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
140 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
9 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
11 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
966 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
49 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
10 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
897 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
101 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
169 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
27 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
5 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
19 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
10 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
538 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
28 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
65 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
6251 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
83 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
738 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
2814 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
6008 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1069 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
606 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
18963 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
2825 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
14177 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1821 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
2165 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
25487 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1410 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
40 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1465 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
50022 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
925 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1438 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
1818 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
972 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2867 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
9388 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
2004 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1579 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
7588 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
8216 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
19611 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
2296 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
37982 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
11741 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2653 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
23186 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
2775 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1897 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
30844 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
1472 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
187763:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
192 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
18174 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
44930 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
36214 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
207152:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
18757 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
321785:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1581 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
43630 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
3059963:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
213084:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
1736669:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
21006 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
2923060:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1831584:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
459364:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
463618:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1579484:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
697820:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
4003594:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
641137:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
215048:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
2376851:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3983678:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
312062:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
2532820:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
1853378:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
9528489:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
196544:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
178106:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
1785 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=affa727dfb200dd46b9b0942598eb58d
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe
Relax bclwdww030 No BCLwSyncdWW
Safe=Fre LwSyncsRR
Time bclwdww030 76.44
$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 -O2 */
/* 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 -O2"
LITMUSOPTS=-r 40
Tue Dec 29 15:57:49 CET 2009