Tue Jan 5 10:17:39 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)
6403407:>1:r1=0; x=1;
13739173:>1:r1=1; x=1;
19857420:>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 11.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
23061 :>1:r1=0; 3:r1=0; x=1; z=1;
1667668:>1:r1=1; 3:r1=0; x=1; z=1;
1674541:>1:r1=0; 3:r1=1; x=1; z=1;
1737196:>1:r1=1; 3:r1=1; x=1; z=1;
2505924:>1:r1=0; 3:r1=0; x=2; z=1;
253776:>1:r1=1; 3:r1=0; x=2; z=1;
2034147:>1:r1=0; 3:r1=1; x=2; z=1;
18366 :>1:r1=1; 3:r1=1; x=2; z=1;
2517461:>1:r1=0; 3:r1=0; x=1; z=2;
1524995:>1:r1=1; 3:r1=0; x=1; z=2;
534552:>1:r1=0; 3:r1=1; x=1; z=2;
37492 :>1:r1=1; 3:r1=1; x=1; z=2;
5427521:>1:r1=0; 3:r1=0; x=2; z=2;
12246 :>1:r1=1; 3:r1=0; x=2; z=2;
31054 :>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 24.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
45416 :>1:r1=0; 3:r1=0; x=1; z=1;
1793976:>1:r1=1; 3:r1=0; x=1; z=1;
1945521:>1:r1=0; 3:r1=1; x=1; z=1;
1562344:>1:r1=1; 3:r1=1; x=1; z=1;
2477490:>1:r1=0; 3:r1=0; x=2; z=1;
377981:>1:r1=1; 3:r1=0; x=2; z=1;
1421762:>1:r1=0; 3:r1=1; x=2; z=1;
16250 :>1:r1=1; 3:r1=1; x=2; z=1;
2883094:>1:r1=0; 3:r1=0; x=1; z=2;
1792574:>1:r1=1; 3:r1=0; x=1; z=2;
299224:>1:r1=0; 3:r1=1; x=1; z=2;
32416 :>1:r1=1; 3:r1=1; x=1; z=2;
5330395:>1:r1=0; 3:r1=0; x=2; z=2;
16613 :>1:r1=1; 3:r1=0; x=2; z=2;
4944 :>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 24.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1675035:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1164743:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1734641:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
163276:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
11323 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
2014010:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1088813:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
2294431:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5282578:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
142945:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
38825 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1783382:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1956173:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
539139:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
110686:>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 23.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
421035:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
641046:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
13 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
24 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
38811 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
991294:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
6 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
399 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
5 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
253 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
10662 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1715820:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4941777:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
114175:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
752 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
352022:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
34482 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
8 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
1 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
2519 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
29 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
1790510:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1457843:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1675128:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
117240:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
3761 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
226 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
2370574:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
141156:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
37 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
19 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
228 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
3 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1420087:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
508136:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
928297:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
455 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
151572:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
576 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
1 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
169018:>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 22.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww005
"LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
lwsync | li r4,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li 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)
1615953:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
1112001:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1725660:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
98715 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
20423 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2166277:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1126010:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
2087969:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
5422059:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
173081:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
16245 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
2036395:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2012320:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
335092:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
51800 :>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 23.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
448726:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
776588:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
24031 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
56865 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
41713 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
811684:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
3880 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
93755 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
2983 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
17073 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
16197 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1246891:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
4912395:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
82787 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
75947 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
3386 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
271995:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
43794 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
4979 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
2121 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
341897:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
20058 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1965168:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1581995:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1321616:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
76992 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
46674 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
325 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
2227824:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
64564 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
57563 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
6778 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
78583 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
1872 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1616637:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
508350:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
881314:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
9151 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
87440 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
9444 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
111 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
157854:>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 22.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
28629 :>2:r1=0; x=1; y=1;
4184720:>2:r1=1; x=1; y=1;
6027515:>2:r1=0; x=2; y=1;
2038880:>2:r1=1; x=2; y=1;
6185192:>2:r1=0; x=1; y=2;
311581:>2:r1=1; x=1; y=2;
1223483:>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 17.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
41195 :>2:r1=0; x=1; y=1;
4152832:>2:r1=1; x=1; y=1;
6003918:>2:r1=0; x=2; y=1;
1996151:>2:r1=1; x=2; y=1;
6228833:>2:r1=0; x=1; y=2;
285163:>2:r1=1; x=1; y=2;
1291908:>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 17.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4672847:>2:r1=0; 2:r4=0; y=1;
1743089:>2:r1=1; 2:r4=0; y=1;
14216 :>2:r1=0; 2:r4=1; y=1;
4739904:>2:r1=1; 2:r4=1; y=1;
2178718:>2:r1=0; 2:r4=0; y=2;
5374877:>2:r1=0; 2:r4=1; y=2;
1276349:>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 16.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3365505:>2:r1=0; 2:r4=0; x=1; y=1;
292 :>2:r1=0; 2:r4=1; x=1; y=1;
233302:>2:r1=1; 2:r4=1; x=1; y=1;
16 :>2:r1=2; 2:r4=1; x=1; y=1;
93 :>2:r1=0; 2:r4=2; x=1; y=1;
44424 :>2:r1=2; 2:r4=2; x=1; y=1;
1984833:>2:r1=0; 2:r4=0; x=2; y=1;
10 :>2:r1=0; 2:r4=1; x=2; y=1;
250966:>2:r1=1; 2:r4=1; x=2; y=1;
249 :>2:r1=2; 2:r4=1; x=2; y=1;
71 :>2:r1=0; 2:r4=2; x=2; y=1;
6215432:>2:r1=2; 2:r4=2; x=2; y=1;
3127761:>2:r1=0; 2:r4=0; x=1; y=2;
14292 :>2:r1=0; 2:r4=1; x=1; y=2;
2662425:>2:r1=1; 2:r4=1; x=1; y=2;
151 :>2:r1=0; 2:r4=2; x=1; y=2;
139 :>2:r1=1; 2:r4=2; x=1; y=2;
2100039:>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 16.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4464261:>2:r1=0; 2:r3=0; y=1;
1865659:>2:r1=1; 2:r3=0; y=1;
52481 :>2:r1=0; 2:r3=1; y=1;
4301564:>2:r1=1; 2:r3=1; y=1;
2630713:>2:r1=0; 2:r3=0; y=2;
6556332:>2:r1=0; 2:r3=1; y=2;
128990:>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 16.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3154435:>2:r1=0; 2:r3=0; x=1; y=1;
54617 :>2:r1=0; 2:r3=1; x=1; y=1;
264369:>2:r1=1; 2:r3=1; x=1; y=1;
3493 :>2:r1=2; 2:r3=1; x=1; y=1;
9023 :>2:r1=0; 2:r3=2; x=1; y=1;
70751 :>2:r1=2; 2:r3=2; x=1; y=1;
2178680:>2:r1=0; 2:r3=0; x=2; y=1;
8403 :>2:r1=0; 2:r3=1; x=2; y=1;
279221:>2:r1=1; 2:r3=1; x=2; y=1;
435 :>2:r1=2; 2:r3=1; x=2; y=1;
32572 :>2:r1=0; 2:r3=2; x=2; y=1;
6139414:>2:r1=2; 2:r3=2; x=2; y=1;
2144223:>2:r1=0; 2:r3=0; x=1; y=2;
15396 :>2:r1=0; 2:r3=1; x=1; y=2;
2292956:>2:r1=1; 2:r3=1; x=1; y=2;
72309 :>2:r1=0; 2:r3=2; x=1; y=2;
1018 :>2:r1=1; 2:r3=2; x=1; y=2;
3278685:>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 16.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4684858:>1:r1=0; x=1;
15976320:>1:r1=1; x=1;
19338822:>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 12.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
47653 :>1:r1=0; 3:r1=0; x=1; z=1;
1931575:>1:r1=1; 3:r1=0; x=1; z=1;
1914638:>1:r1=0; 3:r1=1; x=1; z=1;
1540575:>1:r1=1; 3:r1=1; x=1; z=1;
2738602:>1:r1=0; 3:r1=0; x=2; z=1;
376680:>1:r1=1; 3:r1=0; x=2; z=1;
1392402:>1:r1=0; 3:r1=1; x=2; z=1;
18735 :>1:r1=1; 3:r1=1; x=2; z=1;
2835592:>1:r1=0; 3:r1=0; x=1; z=2;
1704449:>1:r1=1; 3:r1=0; x=1; z=2;
285799:>1:r1=0; 3:r1=1; x=1; z=2;
12166 :>1:r1=1; 3:r1=1; x=1; z=2;
5185644:>1:r1=0; 3:r1=0; x=2; z=2;
11100 :>1:r1=1; 3:r1=0; x=2; z=2;
4390 :>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 24.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1718196:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1070102:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
1615903:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
123585:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
12218 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
2116173:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1335237:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
2234355:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5332926:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
106112:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
36930 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1790674:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1830094:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
567459:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
110036:>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 23.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
504465:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
708181:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
37 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
104 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
83669 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
1198376:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
1 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
24 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
165 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
21498 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1004619:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
4222994:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
58303 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
2444 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
527753:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
19607 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
1 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
16019 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
13 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
2833363:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1420349:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1474836:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
67980 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
5101 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
119 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
1999519:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
41409 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
59 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
24 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
4 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
1977193:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
526816:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
873012:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
748 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
178012:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
421 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
232762:>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 23.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww017
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li 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)
2851238:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
591337:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1627546:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
11527 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
23521 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2162007:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1231512:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
1925944:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
5559366:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
10462 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
3166 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1758138:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1967010:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
258030:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
19196 :>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 23.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)
506948:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
714214:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
28389 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
58246 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
49871 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
804497:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
4101 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
82257 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
3265 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
17695 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
20916 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1300464:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
4866631:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
68792 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
87107 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
235 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
278472:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
9228 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
5537 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1196 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
282719:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
24342 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
2068073:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1464329:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1332337:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
65695 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
54317 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
788 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
2222103:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
55097 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
65114 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
7968 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
61587 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
2921 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1745560:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
414891:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
947985:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
6370 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
101409:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
13829 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
289 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
154216:>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 23.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
19999243:>1:r1=0; 1:r4=0;
446593:>1:r1=0; 1:r4=1;
19554164:>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 11.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5784270:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
26968 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
1607365:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
484237:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
49156 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
2330724:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
64477 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
1363059:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
2160282:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
8104 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
1511949:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
820793:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
103305:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
1803133:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
1882178:>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 22.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3732111:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
53369 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
267350:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
491029:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
556 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
10 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
51 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
690650:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
252820:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
19277 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1179413:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
34 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
48 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
10 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
636 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
1098 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
37 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
106 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
1184742:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1619661:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
4352 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
1197508:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2551448:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
1444678:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
51100 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
231 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
5225 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
190 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
170787:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
2708689:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
73765 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
83 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
66 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
30 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
3 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
182 :>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;
337972:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
1557453:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
403213:>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 21.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5705329:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
93230 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
1137648:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
715597:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
85119 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
2016681:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
163344:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
1763949:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
2090754:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
27196 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
1845560:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
624047:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
162138:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
1710872:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
1858536:>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 21.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3425005:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
50293 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
192335:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
472427:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
41140 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
1027 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
4281 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
8228 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
672629:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
249192:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
15937 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1132075:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
2928 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
4639 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
224 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
56422 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
52088 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
2439 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
290 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
977 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1262906:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
1432875:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
4331 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
1379430:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
2584007:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
1430516:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
54272 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
5474 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
18749 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
322 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
251782:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
2717143:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
81162 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
28795 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
23052 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
1645 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
560 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
58410 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
383 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
332763:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
1538066:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
408781:>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 21.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (74 states)
2503384:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
2292 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
453989:>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;
2005 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
412042:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
503 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
77 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
7 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
375416:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
196 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
130534:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
17 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
161 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
29240 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
8 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
14 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
1 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
599 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
28 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
2 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
259888:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
50 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
33968 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
45 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
3551 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1827473:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
221 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
45929 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
149 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
226955:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
113012:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
69 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
13091 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
38 :>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;
604301:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
3 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
344 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
162 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
23 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
8 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1672483:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
9027 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
1515991:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
191 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
6 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1652004:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1907793:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
86362 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
4 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
7649 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1630705:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
214 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
128 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
5861 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
217584:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
60049 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
3 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
86 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
2224257:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
63 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
50 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
3 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
58 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
274084:>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;
407203:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
515 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
117 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
1287697:>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 21.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
3313641:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
378 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
666067:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
19 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
445 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
872021:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
34589 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
295247:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
4 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
22 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
1504376:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
250557:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
19571 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
8 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
6392 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
268126:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
20 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
1416471:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
375 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
66 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
1093189:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
2906870:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
436 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
386881:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
83 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
14 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
408599:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
1644585:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
2764 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
3026073:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
50 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
440 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1569047:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
55647 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
15 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
45546 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
4 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
6 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
211351:>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 21.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (88 states)
2557484:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
2285 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
499556:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
7 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1443 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
351407:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
46642 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
4349 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
4946 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
357810:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
170 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
147125:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
13 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
133 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
25576 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
478 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
10 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
1261 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
9 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
534 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
44823 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
989 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
309 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
251853:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
56 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
31031 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
28 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
3231 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1707212:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
102 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
31252 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
83 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
229557:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
864 :>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;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
1109 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
121722:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
65 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
11928 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
56 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
519294:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
1436 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
151 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
11974 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
32439 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
40 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
1619 :>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;
6040 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1735152:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
9567 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1540277:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
212 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1641593:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1775629:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
57747 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
7075 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
1229880:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
5209 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
305 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
23737 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
285296:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
29482 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
3 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
84 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
2572651:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
17542 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
2604 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
17572 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
243 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
161 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
21301 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
318117:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
407124:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
423 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
120 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1290360:>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 21.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
20015736:>1:r1=0; 1:r3=0;
481696:>1:r1=0; 1:r3=1;
19502568:>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 11.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5837149:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
66500 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1313993:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
585412:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
125966:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2102353:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
90135 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1568649:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
2070946:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
36645 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1838486:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
613987:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
132870:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1867628:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1749281:>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 21.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3370814:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
51628 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
249715:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
489748:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
121598:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
1240 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
12021 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
21547 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
725021:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
223502:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
24900 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
1180699:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
9002 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1097 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1072 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
92663 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
77268 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
7538 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
848 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1776 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1086802:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1489259:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
9648 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
1190150:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
2526583:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1497683:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
56589 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
7048 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
80362 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
474 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
358154:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2819981:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
67592 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
87338 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
64979 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
4563 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
4225 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
106451:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1533 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
247276:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1430155:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
199458:>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 21.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bclwdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww030
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r2) | lwsync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P0_0_: li 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 (106 states)
2747938:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
119609:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
300090:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
481 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
62983 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
270135:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
51046 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
181 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
3946 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
267 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
113 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
4227 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
393370:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
8003 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
119795:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
11475 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1451 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
33420 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
263 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
195 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2379 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
12 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
105 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
296 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
35262 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
45 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
396 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
73 :>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;
290 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
215555:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
7708 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
16703 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
535 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
737 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
3311 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1569076:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
5927 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
150535:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
54962 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1936 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
236416:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1106 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
23 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
14 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1971 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
80270 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
472 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
22031 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
4893 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
1180 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
491120:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
860 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
421 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
71 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
29 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
11493 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
31083 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
72 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
4130 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
57 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
48 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
6133 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1082833:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
37616 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2249141:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
46358 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
49923 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1494892:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1623875:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
1853 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
67732 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1546 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
106661:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1134728:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3384 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
274 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
13 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
21774 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
260753:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
181 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
25986 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
819 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
15413 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
2582972:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
17277 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
17 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1733 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
128 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
92 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
17108 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
311 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
177 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
12 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
172 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
21501 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
331707:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
6778 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
340717:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
28180 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
10259 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1326374:>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 21.61
$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 10000 -r 2000
Tue Jan 5 10:28:04 CET 2010