Mon Jan 4 13:47:59 CET 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
Test bclwdww000 Allowed
Histogram (3 states)
10375049:>1:r1=0; x=1;
11696985:>1:r1=1; x=1;
17927966:>1:r1=0; x=2;
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 21.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r28,r27,r27
_litmus_P3_2_: li r11,1
_litmus_P3_3_: stwx r11,r28,r2
Test bclwdww001 Allowed
Histogram (15 states)
969041:>1:r1=0; 3:r1=0; x=1; z=1;
3177120:>1:r1=1; 3:r1=0; x=1; z=1;
3257353:>1:r1=0; 3:r1=1; x=1; z=1;
1270177:>1:r1=1; 3:r1=1; x=1; z=1;
4082098:>1:r1=0; 3:r1=0; x=2; z=1;
389788:>1:r1=1; 3:r1=0; x=2; z=1;
471131:>1:r1=0; 3:r1=1; x=2; z=1;
2095 :>1:r1=1; 3:r1=1; x=2; z=1;
3400153:>1:r1=0; 3:r1=0; x=1; z=2;
249294:>1:r1=1; 3:r1=0; x=1; z=2;
581500:>1:r1=0; 3:r1=1; x=1; z=2;
1178 :>1:r1=1; 3:r1=1; x=1; z=2;
2139032:>1:r1=0; 3:r1=0; x=2; z=2;
3117 :>1:r1=1; 3:r1=0; x=2; z=2;
6923 :>1:r1=0; 3:r1=1; x=2; z=2;
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 36.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r28,1
_litmus_P3_3_: stw r28,0(r2)
Test bclwdww002 Allowed
Histogram (15 states)
1085286:>1:r1=0; 3:r1=0; x=1; z=1;
3502311:>1:r1=1; 3:r1=0; x=1; z=1;
3304119:>1:r1=0; 3:r1=1; x=1; z=1;
835092:>1:r1=1; 3:r1=1; x=1; z=1;
3767092:>1:r1=0; 3:r1=0; x=2; z=1;
315603:>1:r1=1; 3:r1=0; x=2; z=1;
407910:>1:r1=0; 3:r1=1; x=2; z=1;
1119 :>1:r1=1; 3:r1=1; x=2; z=1;
3382874:>1:r1=0; 3:r1=0; x=1; z=2;
291588:>1:r1=1; 3:r1=0; x=1; z=2;
333037:>1:r1=0; 3:r1=1; x=1; z=2;
1142 :>1:r1=1; 3:r1=1; x=1; z=2;
2766186:>1:r1=0; 3:r1=0; x=2; z=2;
2855 :>1:r1=1; 3:r1=0; x=2; z=2;
3786 :>1:r1=0; 3:r1=1; x=2; z=2;
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 37.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r26,0(r9)
_litmus_P3_1_: xor r11,r26,r26
_litmus_P3_2_: lwzx r27,r11,r2
Test bclwdww003 Allowed
Histogram (15 states)
3568863:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
619702:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
233142:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
667 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1251840:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
3112216:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
3509907:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
1202764:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
2108801:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
4228 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1473 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
3772720:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
199721:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
413436:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
520 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
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 32.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: xor r11,r28,r28
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww004 Allowed
Histogram (38 states)
2057952:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1450382:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
62 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
164 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
284626:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
629251:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
9 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
128 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
34 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
117 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
320402:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3970436:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
3480347:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
20696 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
287 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
423784:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
403 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
1071 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
2 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
1361106:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
252758:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1702481:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
71413 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
665 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
42 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
1692237:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
66035 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
111 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
31 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
62 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
4 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1223138:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
300877:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
546670:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
12 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
60537 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
47 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
81621 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
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 34.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test bclwdww005 Allowed
Histogram (15 states)
3695743:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
378531:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
206832:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
568 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1235459:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
3242400:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
3488445:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1147673:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
2053722:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
3713 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
2378 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
3890690:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
254056:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
399346:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
444 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
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 32.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r28,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r28,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww006 Allowed
Histogram (42 states)
2322843:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
1373280:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
14383 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
3429 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
361811:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
541295:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
2045 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
13310 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
13124 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
4808 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
484272:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3489439:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
3305586:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
22347 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
40501 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
189932:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
928 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
621 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
21 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
86810 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
285 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
2003185:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
299323:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1538037:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
41694 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
9282 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
52 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1520774:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
20594 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
17960 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
614 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
5341 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
88 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1566946:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
189590:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
474220:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
1432 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
16349 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
6461 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
75 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
16912 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
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 35.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww007
"DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwsync | li r4,1 ;
li r3,1 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P0_0_: li r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: xor r27,r26,r26
_litmus_P2_2_: li r11,1
_litmus_P2_3_: stwx r11,r27,r2
Test bclwdww007 Allowed
Histogram (7 states)
1855921:>2:r1=0; x=1; y=1;
5178579:>2:r1=1; x=1; y=1;
6718266:>2:r1=0; x=2; y=1;
203075:>2:r1=1; x=2; y=1;
5648150:>2:r1=0; x=1; y=2;
88713 :>2:r1=1; x=1; y=2;
307296:>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=c71f30898deb2fe2dc12be48ca126717
Cycle=DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww007 No BCLwSyncdWW
Safe=Wse LwSyncdWW DpdW
Time bclwdww007 27.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li r28,1
_litmus_P2_3_: stw r28,0(r2)
Test bclwdww008 Allowed
Histogram (7 states)
1769542:>2:r1=0; x=1; y=1;
5413956:>2:r1=1; x=1; y=1;
6581705:>2:r1=0; x=2; y=1;
178841:>2:r1=1; x=2; y=1;
5805516:>2:r1=0; x=1; y=2;
93893 :>2:r1=1; x=1; y=2;
156547:>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 27.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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r25,0(r9)
_litmus_P2_1_: xor r11,r25,r25
_litmus_P2_2_: lwzx r26,r11,r2
Test bclwdww009 Allowed
Histogram (7 states)
5698875:>2:r1=0; 2:r4=0; y=1;
120606:>2:r1=1; 2:r4=0; y=1;
1305892:>2:r1=0; 2:r4=1; y=1;
5977969:>2:r1=1; 2:r4=1; y=1;
1181514:>2:r1=0; 2:r4=0; y=2;
5411398:>2:r1=0; 2:r4=1; y=2;
303746:>2:r1=1; 2:r4=1; y=2;
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 24.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r27,0(r2)
_litmus_P2_1_: xor r11,r27,r27
_litmus_P2_2_: lwzx r9,r11,r2
Test bclwdww010 Allowed
Histogram (18 states)
4981411:>2:r1=0; 2:r4=0; x=1; y=1;
182 :>2:r1=0; 2:r4=1; x=1; y=1;
836938:>2:r1=1; 2:r4=1; x=1; y=1;
62 :>2:r1=2; 2:r4=1; x=1; y=1;
151 :>2:r1=0; 2:r4=2; x=1; y=1;
1294938:>2:r1=2; 2:r4=2; x=1; y=1;
1757852:>2:r1=0; 2:r4=0; x=2; y=1;
16 :>2:r1=0; 2:r4=1; x=2; y=1;
67796 :>2:r1=1; 2:r4=1; x=2; y=1;
172 :>2:r1=2; 2:r4=1; x=2; y=1;
295 :>2:r1=0; 2:r4=2; x=2; y=1;
5597768:>2:r1=2; 2:r4=2; x=2; y=1;
1538638:>2:r1=0; 2:r4=0; x=1; y=2;
708 :>2:r1=0; 2:r4=1; x=1; y=2;
1867883:>2:r1=1; 2:r4=1; x=1; y=2;
170 :>2:r1=0; 2:r4=2; x=1; y=2;
80 :>2:r1=1; 2:r4=2; x=1; y=2;
2054940:>2:r1=2; 2:r4=2; x=1; y=2;
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 25.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r27,0(r2)
Test bclwdww011 Allowed
Histogram (7 states)
5827311:>2:r1=0; 2:r3=0; y=1;
99767 :>2:r1=1; 2:r3=0; y=1;
1974818:>2:r1=0; 2:r3=1; y=1;
5623142:>2:r1=1; 2:r3=1; y=1;
950855:>2:r1=0; 2:r3=0; y=2;
5425772:>2:r1=0; 2:r3=1; y=2;
98335 :>2:r1=1; 2:r3=1; y=2;
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 23.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r27,1
_litmus_P1_4_: stw r27,0(r2)
_litmus_P2_0_: lwz r28,0(r2)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r9,0(r2)
Test bclwdww012 Allowed
Histogram (18 states)
4576789:>2:r1=0; 2:r3=0; x=1; y=1;
2428 :>2:r1=0; 2:r3=1; x=1; y=1;
771576:>2:r1=1; 2:r3=1; x=1; y=1;
1008 :>2:r1=2; 2:r3=1; x=1; y=1;
2076 :>2:r1=0; 2:r3=2; x=1; y=1;
1410524:>2:r1=2; 2:r3=2; x=1; y=1;
2103224:>2:r1=0; 2:r3=0; x=2; y=1;
75 :>2:r1=0; 2:r3=1; x=2; y=1;
45092 :>2:r1=1; 2:r3=1; x=2; y=1;
219 :>2:r1=2; 2:r3=1; x=2; y=1;
1125 :>2:r1=0; 2:r3=2; x=2; y=1;
5810603:>2:r1=2; 2:r3=2; x=2; y=1;
943276:>2:r1=0; 2:r3=0; x=1; y=2;
645 :>2:r1=0; 2:r3=1; x=1; y=2;
1675906:>2:r1=1; 2:r3=1; x=1; y=2;
3508 :>2:r1=0; 2:r3=2; x=1; y=2;
366 :>2:r1=1; 2:r3=2; x=1; y=2;
2651560:>2:r1=2; 2:r3=2; x=1; y=2;
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 25.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
Test bclwdww013 Allowed
Histogram (3 states)
6046902:>1:r1=0; x=1;
14191819:>1:r1=1; x=1;
19761279:>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.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r28,1
_litmus_P3_3_: stw r28,0(r2)
Test bclwdww014 Allowed
Histogram (15 states)
1270083:>1:r1=0; 3:r1=0; x=1; z=1;
3172334:>1:r1=1; 3:r1=0; x=1; z=1;
3232325:>1:r1=0; 3:r1=1; x=1; z=1;
1278846:>1:r1=1; 3:r1=1; x=1; z=1;
4108636:>1:r1=0; 3:r1=0; x=2; z=1;
246342:>1:r1=1; 3:r1=0; x=2; z=1;
351827:>1:r1=0; 3:r1=1; x=2; z=1;
971 :>1:r1=1; 3:r1=1; x=2; z=1;
3622473:>1:r1=0; 3:r1=0; x=1; z=2;
223575:>1:r1=1; 3:r1=0; x=1; z=2;
217524:>1:r1=0; 3:r1=1; x=1; z=2;
625 :>1:r1=1; 3:r1=1; x=1; z=2;
2270822:>1:r1=0; 3:r1=0; x=2; z=2;
1644 :>1:r1=1; 3:r1=0; x=2; z=2;
1973 :>1:r1=0; 3:r1=1; x=2; z=2;
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 38.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r26,0(r9)
_litmus_P3_1_: xor r11,r26,r26
_litmus_P3_2_: lwzx r27,r11,r2
Test bclwdww015 Allowed
Histogram (15 states)
3511538:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
776976:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
259956:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
478 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1508286:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
3188582:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
3670536:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
809895:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
2094153:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
5251 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
873 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
3702772:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
182304:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
288073:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
327 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
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 32.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: xor r11,r28,r28
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww016 Allowed
Histogram (37 states)
2160306:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
1000676:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
566 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
747 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
449446:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
871007:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
13 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
45 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
343 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
321 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
564172:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
3249443:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
2681525:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
18690 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
436 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
331657:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
996 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
4340 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
2 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
2533823:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
291269:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1850184:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
40284 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
2066 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
10 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
1564934:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
12510 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
567 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
63 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
1669948:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
286667:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
370037:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
9 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
19761 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
43 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
23093 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
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 35.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test bclwdww017 Allowed
Histogram (15 states)
3841814:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
315730:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
197783:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
841 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1576231:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2738570:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
3763706:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1107811:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1970065:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
3327 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1479 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
3999555:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
206007:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
276394:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
687 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
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 32.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r28,1
_litmus_P1_3_: stw r28,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww018 Allowed
Histogram (42 states)
2356319:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
882685:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
19394 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
5859 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
340883:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
415175:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
1673 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
10711 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
15717 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
5949 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
553834:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3602229:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
4012765:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
11897 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
27648 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
213827:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
635 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
360 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
16 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
91388 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
317 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1610884:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
280083:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1678602:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
44619 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
7856 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
73 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1542893:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
15506 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
19738 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
1071 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
7471 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
181 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1591337:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
163761:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
427965:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
616 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
16454 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
3457 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
22 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
18129 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
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 35.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww019
"DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
Test bclwdww019 Allowed
Histogram (3 states)
19935380:>1:r1=0; 1:r4=0;
6450468:>1:r1=0; 1:r4=1;
13614152:>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 15.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww020
"DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: xor r11,r27,r27
_litmus_P3_2_: lwzx r30,r11,r2
Test bclwdww020 Allowed
Histogram (15 states)
3003593:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
16172 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
3101074:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
898157:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
5579 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
244031:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
4348 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
3634277:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
408765:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1070125:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
2921806:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
630936:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
4604 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
2862885:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
1193648:>1:r1=1; 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 27.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r26,0(r9)
_litmus_P1_1_: xor r11,r26,r26
_litmus_P1_2_: lwzx r27,r11,r2
_litmus_P2_0_: li r28,1
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: xor r11,r28,r28
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww021 Allowed
Histogram (38 states)
3752513:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
14443 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
2641334:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
1176574:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
60 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
78 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
66 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
250924:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
247 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
448031:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
428384:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
18 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
63 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
274 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
77 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
105 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
1909633:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
281689:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
738358:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
3486796:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
371101:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
1790289:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
20745 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
10 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
488 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
37116 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
1409276:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
9763 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
20 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
178 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
6 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
28 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
32888 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
1120996:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
77423 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
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 30.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww022
"LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r11,r27,r27
_litmus_P1_2_: lwzx r30,r11,r2
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww022 Allowed
Histogram (15 states)
2496716:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
8417 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
3258159:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
607578:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
5038 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
265094:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
2993 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
3884506:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
337511:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
1312604:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
3246877:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
565565:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
1752 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
2978253:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
1028937:>1:r1=1; 1:r4=1; 3:r1=1; 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 27.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r26,0(r9)
_litmus_P1_1_: xor r11,r26,r26
_litmus_P1_2_: lwzx r27,r11,r2
_litmus_P2_0_: li r28,1
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww023 Allowed
Histogram (42 states)
3819981:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
17133 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
2521547:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
1115310:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
2600 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
2629 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
547 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
223294:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
949 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
432472:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
466347:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
364 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
17 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
1158 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
3127 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
2752 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
29 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
1675 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
621 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1760217:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
277213:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
692055:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3474009:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
553867:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
1586588:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
21480 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
221 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
3107 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
42990 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
1470656:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
14477 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
546 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
3494 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
108 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
75 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
3405 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
47 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
42134 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
1318330:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
122421:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
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 29.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r28,0(r2)
_litmus_P1_1_: xor r11,r28,r28
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: xor r11,r28,r28
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww024 Allowed
Histogram (70 states)
3885604:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
269 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
456772:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
4 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
207 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
1190182:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
131 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
24 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
29 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
429199:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
215 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
263645:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
144 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
277602:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
2 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
77 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
31 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
167 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
49 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
26 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
702551:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
89 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
350987:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
44 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
168085:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1132455:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
54 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
134897:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
48 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
139584:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
1 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
23465 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
3729 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
28 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
211605:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
2 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
44 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
185 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
27 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
36 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1105121:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
3366 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
1693323:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
345 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
5 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1747737:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
697831:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
46435 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
1056 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1921698:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
20 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
9 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
1003 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
55045 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
14925 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
10 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
1833781:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
49 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
81 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
35 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
83657 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
104852:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
11 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
26 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
1317278:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; 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 32.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r28,0(r2)
_litmus_P1_1_: xor r11,r28,r28
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test bclwdww025 Allowed
Histogram (38 states)
3938746:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
40 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
363258:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
175 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
1676342:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
17307 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
1427 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
10 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
284405:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
2574190:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
52 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
308198:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
6 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
66 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
591563:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
884904:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
37 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
438464:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
54 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
126 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
3500302:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
445096:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
34468 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
8 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
64107 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
1957146:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
796 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
1654645:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
79 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
33 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1139503:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
33068 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
5 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
13784 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
77583 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
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 29.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r28,0(r2)
_litmus_P1_1_: xor r11,r28,r28
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww026 Allowed
Histogram (80 states)
4400227:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
289 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
341631:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
248 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
913462:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
11825 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
1065 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
4453 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
421800:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
152 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
212666:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
5 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
89 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
235627:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
2129 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
1479 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
585 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
9788 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
751 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1086 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
739529:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
96 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
296248:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
48 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
163461:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
953656:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
69 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
113600:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
54 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
141765:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
84 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
9 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
37 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
31544 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
4739 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
18 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
171375:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
567 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
150 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
1122 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
3921 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
178 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
250 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1213790:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
2591 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1367245:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
275 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
4 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1996036:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
895552:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
17642 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
924 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
1657268:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
548 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
3562 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
101920:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
10576 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
22 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
1807571:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
6827 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
220 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
7307 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
1632 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
26 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
5375 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
125179:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
89426 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
7 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
23 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1506554:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; 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: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 32.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww027
"LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
Test bclwdww027 Allowed
Histogram (3 states)
18228734:>1:r1=0; 1:r3=0;
10086921:>1:r1=0; 1:r3=1;
11684345:>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 16.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww028
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r4,1
_litmus_P2_1_: stw r4,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test bclwdww028 Allowed
Histogram (15 states)
2211719:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
10634 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
3492023:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
609523:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
4407 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
263967:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1542 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
4056540:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
361805:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1268264:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
3245369:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
330977:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1624 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
3074964:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1066642:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
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 27.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r28,0(r2)
_litmus_P2_0_: li r28,1
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww029 Allowed
Histogram (41 states)
3220963:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
5890 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2785637:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
947544:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
3800 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
13008 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
1907 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
291636:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
279 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
559555:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
471735:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
373 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
18 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
2322 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
10751 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
11912 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
41 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
12107 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
2476 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
2357886:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
174863:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
935153:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3407882:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
369518:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1744006:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
25368 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
122 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
5215 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
24624 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1291145:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
6777 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
585 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
12689 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
276 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
5 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
3980 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
37 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
28112 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1200509:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
69284 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
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 30.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,2
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r28,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r28,2
_litmus_P2_1_: stw r28,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r3,1
_litmus_P2_4_: stw r3,0(r2)
_litmus_P3_0_: lwz r28,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww030 Allowed
Histogram (100 states)
4162924:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
31204 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
321834:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
829 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
26087 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
1102382:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
12282 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
9 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
824 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
67 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
15 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
4031 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
481843:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
2689 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
228277:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
5573 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
4211 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
348465:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1562 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
16 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
934 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
9 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
5 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
594 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
6196 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
13 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
582 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
16 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
1015 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
930129:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
12226 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
288900:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
2537 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
4153 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
218924:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
876119:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
3335 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
95351 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
13194 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
465 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
90439 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
67 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
12 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
20232 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
32 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
9336 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
244 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
18 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
96304 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
381 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
218 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
8 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
2 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
800 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
3931 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
3 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
270 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
304 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1175953:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
8931 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1856371:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
14531 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
5422 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1454935:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1000436:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
160 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
14484 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1439 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
17028 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1415314:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1296 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
11 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
2716 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
122742:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
13 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
6599 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
356 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1752 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1789683:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
5087 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
125 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
14 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
6198 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1700 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
15 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
4 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
4684 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
150833:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
191 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
116289:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
3190 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2031 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1407024:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
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 32.33
$Revision: 3228 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 -O"
LITMUSOPTS=-r 20 -v
Mon Jan 4 14:03:12 CET 2010