Tue Jan 5 18:07:21 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)
5593839:>1:r1=0; x=1;
14410321:>1:r1=1; x=1;
19995840:>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 14.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
23495 :>1:r1=0; 3:r1=0; x=1; z=1;
1694379:>1:r1=1; 3:r1=0; x=1; z=1;
1823376:>1:r1=0; 3:r1=1; x=1; z=1;
1831047:>1:r1=1; 3:r1=1; x=1; z=1;
2652451:>1:r1=0; 3:r1=0; x=2; z=1;
174466:>1:r1=1; 3:r1=0; x=2; z=1;
1921569:>1:r1=0; 3:r1=1; x=2; z=1;
14121 :>1:r1=1; 3:r1=1; x=2; z=1;
2514410:>1:r1=0; 3:r1=0; x=1; z=2;
1266065:>1:r1=1; 3:r1=0; x=1; z=2;
556060:>1:r1=0; 3:r1=1; x=1; z=2;
38597 :>1:r1=1; 3:r1=1; x=1; z=2;
5442266:>1:r1=0; 3:r1=0; x=2; z=2;
4377 :>1:r1=1; 3:r1=0; x=2; z=2;
43321 :>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 28.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
73755 :>1:r1=0; 3:r1=0; x=1; z=1;
1705477:>1:r1=1; 3:r1=0; x=1; z=1;
2039822:>1:r1=0; 3:r1=1; x=1; z=1;
1709673:>1:r1=1; 3:r1=1; x=1; z=1;
2489730:>1:r1=0; 3:r1=0; x=2; z=1;
341497:>1:r1=1; 3:r1=0; x=2; z=1;
1406093:>1:r1=0; 3:r1=1; x=2; z=1;
14640 :>1:r1=1; 3:r1=1; x=2; z=1;
2849222:>1:r1=0; 3:r1=0; x=1; z=2;
1628938:>1:r1=1; 3:r1=0; x=1; z=2;
370768:>1:r1=0; 3:r1=1; x=1; z=2;
25094 :>1:r1=1; 3:r1=1; x=1; z=2;
5323385:>1:r1=0; 3:r1=0; x=2; z=2;
10462 :>1:r1=1; 3:r1=0; x=2; z=2;
11444 :>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 29.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1762182:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
986517:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1623457:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
148790:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
14421 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
1812410:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1370708:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
2154416:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5471309:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
87224 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
36715 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1771546:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
2118194:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
526341:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
115770:>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 28.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (40 states)
517476:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
550407:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
46 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
108 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
34588 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
1120388:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
2 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
500 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
9 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
228 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
3061 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1841756:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4839860:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
75990 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
4199 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
431887:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
52435 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
7 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
6 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
18355 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
86 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
1308740:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1419043:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
2057987:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
210502:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
7335 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
595 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
2217979:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
140646:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
121 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
56 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
220 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
16 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1348908:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
379740:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1230076:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1428 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
74596 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
277 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
110341:>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 27.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1620160:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
950039:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1593429:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
77917 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
30012 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2079502:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1348578:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1984711:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
5546957:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
136198:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
14851 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
2072625:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2102456:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
373212:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
69353 :>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 28.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
517133:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
729210:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
12013 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
27208 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
41928 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
913441:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
5630 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
174130:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
1039 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
6424 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
10115 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1516309:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
4686957:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
79977 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
102608:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1632 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
324774:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
54828 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
3279 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
4387 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
406890:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
15787 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1679681:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1531681:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1528350:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
109686:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
68753 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
1292 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1835409:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
78650 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
66020 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
14056 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
72724 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
1969 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1707579:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
519572:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
949577:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
10316 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
52674 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
13513 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
206 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
122593:>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 27.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
67027 :>2:r1=0; x=1; y=1;
3260329:>2:r1=1; x=1; y=1;
7695412:>2:r1=0; x=2; y=1;
2109877:>2:r1=1; x=2; y=1;
5874059:>2:r1=0; x=1; y=2;
417626:>2:r1=1; x=1; y=2;
575670:>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 19.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
54524 :>2:r1=0; x=1; y=1;
3129321:>2:r1=1; x=1; y=1;
7306086:>2:r1=0; x=2; y=1;
2544749:>2:r1=1; x=2; y=1;
5624788:>2:r1=0; x=1; y=2;
672885:>2:r1=1; x=1; y=2;
667647:>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 19.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5545066:>2:r1=0; 2:r4=0; y=1;
1697804:>2:r1=1; 2:r4=0; y=1;
16035 :>2:r1=0; 2:r4=1; y=1;
3938557:>2:r1=1; 2:r4=1; y=1;
2144882:>2:r1=0; 2:r4=0; y=2;
5698829:>2:r1=0; 2:r4=1; y=2;
958827:>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 19.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2730391:>2:r1=0; 2:r4=0; x=1; y=1;
80 :>2:r1=0; 2:r4=1; x=1; y=1;
563091:>2:r1=1; 2:r4=1; x=1; y=1;
71 :>2:r1=2; 2:r4=1; x=1; y=1;
58 :>2:r1=0; 2:r4=2; x=1; y=1;
50830 :>2:r1=2; 2:r4=2; x=1; y=1;
2119156:>2:r1=0; 2:r4=0; x=2; y=1;
5 :>2:r1=0; 2:r4=1; x=2; y=1;
501073:>2:r1=1; 2:r4=1; x=2; y=1;
175 :>2:r1=2; 2:r4=1; x=2; y=1;
448 :>2:r1=0; 2:r4=2; x=2; y=1;
5688829:>2:r1=2; 2:r4=2; x=2; y=1;
3708510:>2:r1=0; 2:r4=0; x=1; y=2;
9431 :>2:r1=0; 2:r4=1; x=1; y=2;
2157795:>2:r1=1; 2:r4=1; x=1; y=2;
376 :>2:r1=0; 2:r4=2; x=1; y=2;
98 :>2:r1=1; 2:r4=2; x=1; y=2;
2469583:>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 19.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4868224:>2:r1=0; 2:r3=0; y=1;
1652537:>2:r1=1; 2:r3=0; y=1;
106069:>2:r1=0; 2:r3=1; y=1;
3866063:>2:r1=1; 2:r3=1; y=1;
2829845:>2:r1=0; 2:r3=0; y=2;
6195522:>2:r1=0; 2:r3=1; y=2;
481740:>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 19.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2886821:>2:r1=0; 2:r3=0; x=1; y=1;
37576 :>2:r1=0; 2:r3=1; x=1; y=1;
463243:>2:r1=1; 2:r3=1; x=1; y=1;
28473 :>2:r1=2; 2:r3=1; x=1; y=1;
3817 :>2:r1=0; 2:r3=2; x=1; y=1;
84499 :>2:r1=2; 2:r3=2; x=1; y=1;
2229495:>2:r1=0; 2:r3=0; x=2; y=1;
29370 :>2:r1=0; 2:r3=1; x=2; y=1;
424470:>2:r1=1; 2:r3=1; x=2; y=1;
676 :>2:r1=2; 2:r3=1; x=2; y=1;
69053 :>2:r1=0; 2:r3=2; x=2; y=1;
5711231:>2:r1=2; 2:r3=2; x=2; y=1;
2655752:>2:r1=0; 2:r3=0; x=1; y=2;
29079 :>2:r1=0; 2:r3=1; x=1; y=2;
2373813:>2:r1=1; 2:r3=1; x=1; y=2;
99365 :>2:r1=0; 2:r3=2; x=1; y=2;
3672 :>2:r1=1; 2:r3=2; x=1; y=2;
2869595:>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 19.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6725078:>1:r1=0; x=1;
13402648:>1:r1=1; x=1;
19872274:>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 14.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
77304 :>1:r1=0; 3:r1=0; x=1; z=1;
1790039:>1:r1=1; 3:r1=0; x=1; z=1;
2093016:>1:r1=0; 3:r1=1; x=1; z=1;
1648692:>1:r1=1; 3:r1=1; x=1; z=1;
2706841:>1:r1=0; 3:r1=0; x=2; z=1;
341545:>1:r1=1; 3:r1=0; x=2; z=1;
1373729:>1:r1=0; 3:r1=1; x=2; z=1;
19063 :>1:r1=1; 3:r1=1; x=2; z=1;
2826108:>1:r1=0; 3:r1=0; x=1; z=2;
1573849:>1:r1=1; 3:r1=0; x=1; z=2;
342467:>1:r1=0; 3:r1=1; x=1; z=2;
15972 :>1:r1=1; 3:r1=1; x=1; z=2;
5174599:>1:r1=0; 3:r1=0; x=2; z=2;
6724 :>1:r1=1; 3:r1=0; x=2; z=2;
10052 :>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 29.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1822129:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
992944:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1567088:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
141445:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
23571 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
2038241:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1454410:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
2090479:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5422352:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
72342 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
32472 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1760700:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1917778:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
531852:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
132197:>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 28.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (40 states)
656655:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
714911:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
123 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
310 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
70056 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
1166894:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
2 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
1229 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
43 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
317 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
12045 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1340313:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4485435:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
53357 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
11910 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
537282:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
21931 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
4 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
8 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
27373 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
50 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
2016479:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1548330:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1906820:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
119113:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
7713 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
305 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
1605030:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
54802 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
197 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
112 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
141 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
38 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1919353:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
531221:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1119524:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1543 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
24205 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
418 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
44408 :>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 27.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2559868:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
760176:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1522834:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
19403 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
66091 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2207919:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1362030:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1891515:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
5495529:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
20399 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
4514 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1916872:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1858012:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
293718:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
21120 :>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 28.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
626519:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
688816:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
13114 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
26055 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
49573 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
888949:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
7592 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
156269:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
1246 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
7107 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
11782 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1583332:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
4613966:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
57928 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
118245:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
379 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
351410:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
16068 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
3077 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
2233 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
350044:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
20157 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1708887:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1450571:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1560399:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
94643 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
73889 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
1628 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1920789:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
66766 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
67560 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
14348 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
69433 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
2543 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1746708:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
429076:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
1022474:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
7709 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
42111 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
12647 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
196 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
113762:>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 27.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
20002011:>1:r1=0; 1:r4=0;
184039:>1:r1=0; 1:r4=1;
19813950:>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 14.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5417302:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
35812 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
1549924:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
915377:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
18997 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
2307811:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
160859:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
1407395:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
2158361:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
2399 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
1660500:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
774091:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
60583 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
1319280:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
2211309:>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 23.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
3588918:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
50706 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
265569:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
470531:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
604 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
8 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
22 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
779134:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
408354:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
16447 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1181673:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
74 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
97 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
346 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
1398 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
112 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
6 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
173 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
1082421:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1531865:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1301 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
1100090:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2807466:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
1315718:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
54100 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
1780 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
7270 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
211 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
151394:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
2724640:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
64907 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
120 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
120 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
12 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
2 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
228 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
1 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
414852:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
1614224:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
363104:>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 27.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5851757:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
96077 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
1082073:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
826996:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
76474 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
1973029:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
172152:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
1617162:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
2091235:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
40144 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
1856216:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
619365:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
192761:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
1539552:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
1965007:>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 23.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3306441:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
46520 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
207235:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
457341:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
62451 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
3413 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
4211 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
14840 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
741674:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
375978:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
13768 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1101815:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
7994 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
9161 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
300 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
68995 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
73971 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
7214 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
228 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1873 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1117423:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
1446260:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
1367 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
1242972:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
2808226:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
1295181:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
50635 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
14172 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
31180 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
479 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
205088:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
2783393:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
59761 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
38529 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
30641 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
2388 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
1683 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
69510 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
549 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
398473:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
1543795:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
352872:>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 26.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
2475707:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
1209 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
519398:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
1995 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
381591:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
230 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
16 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
4 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
428420:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
164 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
169877:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
82 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
39302 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
5 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
34 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
10 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
670 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
10 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
10 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
270447:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
16 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
51894 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
11 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
4129 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1902956:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
1616 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
57263 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
148 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
216380:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
138632:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
135 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
25392 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
10 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
5 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
523359:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
8 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
245 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
199 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
62 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
48 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1490726:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
7052 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
1570263:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
170 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
9 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1697467:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1816975:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
184016:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
2258 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1949162:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
489 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
373 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
9293 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
121362:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
76677 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
6 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
204 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
1972325:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
73 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
29 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
169 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
1 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
24 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
255721:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
355571:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
231 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
152 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
1277483:>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 25.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (40 states)
3488762:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
384 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
724036:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
69 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
466 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
910347:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
43626 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
344418:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
45 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
57 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
1419797:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
269471:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
27560 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
6 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
8351 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
340861:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
11 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
1326652:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
236 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
112 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
1117232:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
2945652:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
1631 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
201825:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
94 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
7 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
413290:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
1597113:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
7397 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
2843432:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
128 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
103 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1636694:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
64897 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
375 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
76001 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
36 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
2 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
188821:>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 26.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (90 states)
2397996:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
1090 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
574906:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1515 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
324907:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
48081 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
14 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
8225 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
9 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
4399 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
416771:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
134 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
189811:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
83 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
34697 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
398 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
6 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
2143 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
706 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
27297 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
2134 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
323 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
262525:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
15 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
46922 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
7 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
14 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
3756 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1819599:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
1442 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
50458 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
132 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
226136:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2194 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
80 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
3546 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
142930:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
242 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
26781 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
20 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
3 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
517437:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2048 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
399 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
12314 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
51799 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
47 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
4888 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
7 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
14470 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1504747:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
7929 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1578102:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
136 :>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;
1684692:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1690076:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
140637:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
2478 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
1626389:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
4652 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
734 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
16 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
32911 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
181589:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
61339 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
168 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
2274835:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
19633 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
3923 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
4 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
24538 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
293 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
376 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
19400 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
294437:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
350293:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
228 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
185 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1269371:>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 25.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww027
"LwSyncdRR Fre LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li 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)
20005460:>1:r1=0; 1:r3=0;
360017:>1:r1=0; 1:r3=1;
19634523:>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 14.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5817797:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
78959 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1311337:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
715795:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
113296:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2066686:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
108717:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1447004:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1994958:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
55806 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1930655:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
655838:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
133842:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1707926:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1861384:>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 23.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
3198976:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
41635 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
228955:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
372854:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
114269:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
9368 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
6839 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
35250 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
857065:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
402994:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
23863 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
1117526:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
18656 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
7830 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1363 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
134200:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
110900:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
20557 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
321 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1961 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1098022:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1336012:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
7880 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
1041003:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
2743580:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1355472:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
51509 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
23202 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
67744 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
685 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
254204:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2752190:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
55407 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
77470 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
66294 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
6480 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
5983 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
118140:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1315 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
406019:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1610435:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
215572:>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 26.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (107 states)
2495132:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
98542 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
410372:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
694 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
61040 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
293732:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
46638 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
529 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
6858 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
248 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
224 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
4311 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
436817:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
18759 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
189147:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
10536 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
3403 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
45287 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
381 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
285 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
3402 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
14 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
65 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
564 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
22609 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
165 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1126 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
70 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
11 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
440 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
236182:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
9418 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
29264 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1108 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
705 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
4999 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1716073:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
8542 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
131827:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
42155 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1785 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
241311:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1989 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
194 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
37 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
4939 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
111921:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
878 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
36769 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
9532 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
841 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
487086:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
1165 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
13 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
594 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
180 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
22 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
10522 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
47053 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
226 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
7734 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
276 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
66 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
11620 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1080727:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
56009 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1961005:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
53938 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
40228 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1557985:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1699739:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
8308 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
136890:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3453 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
143928:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1428888:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3234 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
7 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
769 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
21 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
323 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
30828 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
178767:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
883 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
57771 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1953 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
31206 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
2241708:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
19849 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
52 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2814 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
249 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
276 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
23250 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
302 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
385 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
46 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
75 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
19488 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
274274:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
8629 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
299504:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
17070 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
25264 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1281473:>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 25.45
$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=-s 1000 -r 20000
Tue Jan 5 18:19:42 CET 2010