Tue Jan 5 10:09:43 CET 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr000
"Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
2097893:>3:r1=0; 3:r3=0; x=1; y=1;
79544 :>3:r1=1; 3:r3=0; x=1; y=1;
1192445:>3:r1=2; 3:r3=0; x=1; y=1;
37325 :>3:r1=0; 3:r3=1; x=1; y=1;
1257491:>3:r1=1; 3:r3=1; x=1; y=1;
1191577:>3:r1=2; 3:r3=1; x=1; y=1;
2051252:>3:r1=0; 3:r3=0; x=2; y=1;
205665:>3:r1=2; 3:r3=0; x=2; y=1;
1991946:>3:r1=0; 3:r3=1; x=2; y=1;
318667:>3:r1=1; 3:r3=1; x=2; y=1;
3856445:>3:r1=2; 3:r3=1; x=2; y=1;
2167981:>3:r1=0; 3:r3=0; x=1; y=2;
209171:>3:r1=1; 3:r3=0; x=1; y=2;
167798:>3:r1=2; 3:r3=0; x=1; y=2;
402261:>3:r1=0; 3:r3=1; x=1; y=2;
927183:>3:r1=1; 3:r3=1; x=1; y=2;
1582424:>3:r1=2; 3:r3=1; x=1; y=2;
3716 :>3:r1=0; 3:r3=0; x=2; y=2;
253587:>3:r1=0; 3:r3=1; x=2; y=2;
1443 :>3:r1=1; 3:r3=1; x=2; y=2;
4186 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 22.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr001
"Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 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_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
1683485:>3:r1=0; 3:r3=0; x=1; y=1;
94820 :>3:r1=1; 3:r3=0; x=1; y=1;
993147:>3:r1=2; 3:r3=0; x=1; y=1;
24565 :>3:r1=0; 3:r3=1; x=1; y=1;
1154032:>3:r1=1; 3:r3=1; x=1; y=1;
721194:>3:r1=2; 3:r3=1; x=1; y=1;
2473246:>3:r1=0; 3:r3=0; x=2; y=1;
416253:>3:r1=2; 3:r3=0; x=2; y=1;
2385668:>3:r1=0; 3:r3=1; x=2; y=1;
364336:>3:r1=1; 3:r3=1; x=2; y=1;
4328568:>3:r1=2; 3:r3=1; x=2; y=1;
2307706:>3:r1=0; 3:r3=0; x=1; y=2;
290758:>3:r1=1; 3:r3=0; x=1; y=2;
221818:>3:r1=2; 3:r3=0; x=1; y=2;
188303:>3:r1=0; 3:r3=1; x=1; y=2;
728524:>3:r1=1; 3:r3=1; x=1; y=2;
1358766:>3:r1=2; 3:r3=1; x=1; y=2;
4499 :>3:r1=0; 3:r3=0; x=2; y=2;
248498:>3:r1=0; 3:r3=1; x=2; y=2;
2481 :>3:r1=1; 3:r3=1; x=2; y=2;
9333 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 22.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr002
"Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r27,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
6067450:>2:r1=0; 2:r3=0; x=1;
1746511:>2:r1=2; 2:r3=0; x=1;
248264:>2:r1=0; 2:r3=1; x=1;
1230760:>2:r1=1; 2:r3=1; x=1;
4334461:>2:r1=2; 2:r3=1; x=1;
590162:>2:r1=0; 2:r3=0; x=2;
1012199:>2:r1=0; 2:r3=1; x=2;
1625627:>2:r1=1; 2:r3=1; x=2;
3144566:>2:r1=2; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=e86498b53008de1e6a240afbf078cd14
Cycle=Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr002 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr002 14.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr003
"Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r28,1
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
2294386:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
2047657:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
268641:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
315576:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1518374:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2014892:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
45507 :>0:r3=1; 3:r1=0; 3:r3=1; y=1;
490444:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1399384:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
3644645:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
760835:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
12096 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
2144261:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
284530:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
281945:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
464643:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
210950:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
7084 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
556472:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
3021 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
1234657:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 21.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr004
"Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr004 Allowed
Histogram (38 states)
1619883:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
375174:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
23106 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1090270:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
761952:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
30082 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
52105 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
520490:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
524617:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
201559:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
841766:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1687106:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1258680:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
144464:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
82338 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2238860:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
577463:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
298417:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
277326:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
1547750:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
37 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1507183:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
399 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
485977:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2009 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
481759:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
11962 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2614448:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
346099:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3154 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1115 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
7590 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
375358:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1193 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3445 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
397 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4040 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
427 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 No ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 21.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr005
"Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
1690664:>3:r1=0; 3:r3=0; x=1; y=1;
101432:>3:r1=1; 3:r3=0; x=1; y=1;
1278065:>3:r1=2; 3:r3=0; x=1; y=1;
17654 :>3:r1=0; 3:r3=1; x=1; y=1;
1080986:>3:r1=1; 3:r3=1; x=1; y=1;
893176:>3:r1=2; 3:r3=1; x=1; y=1;
1944546:>3:r1=0; 3:r3=0; x=2; y=1;
124777:>3:r1=2; 3:r3=0; x=2; y=1;
1748801:>3:r1=0; 3:r3=1; x=2; y=1;
585145:>3:r1=1; 3:r3=1; x=2; y=1;
3499100:>3:r1=2; 3:r3=1; x=2; y=1;
1984128:>3:r1=0; 3:r3=0; x=1; y=2;
632465:>3:r1=1; 3:r3=0; x=1; y=2;
368237:>3:r1=2; 3:r3=0; x=1; y=2;
166359:>3:r1=0; 3:r3=1; x=1; y=2;
1339824:>3:r1=1; 3:r3=1; x=1; y=2;
2012932:>3:r1=2; 3:r3=1; x=1; y=2;
34477 :>3:r1=0; 3:r3=0; x=2; y=2;
448323:>3:r1=0; 3:r3=1; x=2; y=2;
21580 :>3:r1=1; 3:r3=1; x=2; y=2;
27329 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 22.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr006
"Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw 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 (x=2 /\ y=2 /\ 3:r1=2 /\ 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_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
1393706:>3:r1=0; 3:r3=0; x=1; y=1;
107847:>3:r1=1; 3:r3=0; x=1; y=1;
1116376:>3:r1=2; 3:r3=0; x=1; y=1;
12393 :>3:r1=0; 3:r3=1; x=1; y=1;
946760:>3:r1=1; 3:r3=1; x=1; y=1;
578365:>3:r1=2; 3:r3=1; x=1; y=1;
2243025:>3:r1=0; 3:r3=0; x=2; y=1;
289317:>3:r1=2; 3:r3=0; x=2; y=1;
2044075:>3:r1=0; 3:r3=1; x=2; y=1;
727134:>3:r1=1; 3:r3=1; x=2; y=1;
3809048:>3:r1=2; 3:r3=1; x=2; y=1;
1900634:>3:r1=0; 3:r3=0; x=1; y=2;
752899:>3:r1=1; 3:r3=0; x=1; y=2;
400918:>3:r1=2; 3:r3=0; x=1; y=2;
93383 :>3:r1=0; 3:r3=1; x=1; y=2;
1143758:>3:r1=1; 3:r3=1; x=1; y=2;
1809635:>3:r1=2; 3:r3=1; x=1; y=2;
106697:>3:r1=0; 3:r3=0; x=2; y=2;
452463:>3:r1=0; 3:r3=1; x=2; y=2;
24028 :>3:r1=1; 3:r3=1; x=2; y=2;
47539 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr006 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr006 21.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr007
"Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 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 r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r27,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
4683723:>2:r1=0; 2:r3=0; x=1;
1503292:>2:r1=2; 2:r3=0; x=1;
17340 :>2:r1=0; 2:r3=1; x=1;
2093899:>2:r1=1; 2:r3=1; x=1;
3069910:>2:r1=2; 2:r3=1; x=1;
1984476:>2:r1=0; 2:r3=0; x=2;
221441:>2:r1=0; 2:r3=1; x=2;
2825368:>2:r1=1; 2:r3=1; x=2;
3600551:>2:r1=2; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=ba17863040d25a62a648bb8030bf59fd
Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr007 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr007 14.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr008
"Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r28,1
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
1771778:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
1464164:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
327589:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
296977:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1250482:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1236824:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
9103 :>0:r3=1; 3:r1=0; 3:r3=1; y=1;
1244673:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1239326:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2426470:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
503013:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
347851:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
1680186:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
1233549:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
578694:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
1139802:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
50870 :>0:r3=1; 3:r1=0; 3:r3=1; y=2;
79631 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
1080814:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
302166:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
1736038:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=61bd93196401321b8fb91e15727e3c64
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr008 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr008 21.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr009
"Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr009 Allowed
Histogram (39 states)
1244461:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
464930:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
17787 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
902163:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
632090:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
25724 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
56609 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
604903:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1012330:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
139003:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1213603:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1994648:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
620590:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
585753:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
224277:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2122421:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
532459:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
197280:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
183752:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
1496638:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
31 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1190157:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
427 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
270407:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2618 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
844401:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
51189 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2186099:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
368890:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
37930 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
24650 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
63678 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
9 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
559603:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2652 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
46091 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1778 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
75397 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2572 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 21.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr010
"Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ;
lwz r3,0(r4) | | lwz r3,0(r4) | ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: lwz r27,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r30,0(r2)
_litmus_P1_0_: li r5,1
_litmus_P1_1_: stw r5,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
_litmus_P3_0_: li r6,1
_litmus_P3_1_: stw r6,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
2574860:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
630882:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
1015759:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
2176393:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
483733:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
1172513:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
302227:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
1237918:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
1032014:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
2885 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
1489160:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
1865443:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
250783:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
1403178:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
4362252:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=8ce05c9f86d49b2adfd5546bd471aa44
Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr010 No ACLwSyncdRR
Safe=Fre
Time aclwdrr010 17.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr011
"Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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 ;
sync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_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 r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
4325845:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
36196 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
2007974:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
425420:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
580025:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1903053:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
32060 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1851778:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
949856:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
33263 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1157573:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1993126:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
154291:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2602802:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1946738:>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=064d7a96bedb614c156f5bd3adf783d8
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr011 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr011 20.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr012
"Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 ;
sync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r28,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
2668769:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
239307:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
93603 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1562982:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
802214:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1096724:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
644609:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1327613:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
234229:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
70030 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
446299:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
39 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
983 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1866 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
29 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
6674 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
324451:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
819527:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
3281 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
328180:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
476811:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
10359 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1020332:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
599 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
5395 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1309950:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1630114:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3672 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
329854:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
961892:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
546202:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3033405:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=992754280de579a7f5feb516274ac846
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr012 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr012 20.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr013
"Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3: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)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
4402193:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
55624 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1597973:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
768928:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
585670:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1700146:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
82496 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1105601:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1461410:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
12315 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1218098:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1500922:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
381952:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2173509:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
2953163:>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=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 19.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr014
"Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r28,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr014 Allowed
Histogram (31 states)
2545463:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2576 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
571564:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1228690:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3796 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1999683:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
569361:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1300479:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
4478 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
322927:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
2820 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
68 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
93 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
547 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
9458 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
38024 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
4 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
5545 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1211774:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1835 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1104726:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4004 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
864 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1470917:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1869523:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
951 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
317309:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1536276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
14997 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3861246:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=0363e525d1d5c107b6654781a780ef6a
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr014 No ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr014 19.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr015
"Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
3245327:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2395153:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
679603:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1888157:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
843657:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
12408 :>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1670125:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1691068:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
14636 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
1473120:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
240262:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
465122:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1890259:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
16533 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
3474570:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=61d664ae95ff6d97da76ebb37bc47ca3
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr015 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr015 21.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr016
"Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 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_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
3303501:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1792052:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
655552:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1638945:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
588718:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
4974 :>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1469297:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1079429:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
38808 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
2124754:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
409957:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
401765:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
2224005:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
19829 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
4248414:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4947e9ed11cb60630be5b54900bf7b6c
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr016 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr016 21.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr017
"Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
1310298:>0:r3=0; 2:r1=0; 2:r3=0;
5349853:>0:r3=1; 2:r1=0; 2:r3=0;
2723348:>0:r3=1; 2:r1=1; 2:r3=0;
2508795:>0:r3=0; 2:r1=0; 2:r3=1;
3398 :>0:r3=1; 2:r1=0; 2:r3=1;
4157379:>0:r3=0; 2:r1=1; 2:r3=1;
3946929:>0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=0dd8df1959f84e11508b32d374a44775
Cycle=Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr017 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr017 14.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr018
"Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 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_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r30,1
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r29,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
466213:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
2753938:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
1877879:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
1626337:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
564793:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
370391:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
1720664:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1225644:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
995945:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
1290676:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
652 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
317136:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
1699873:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
3952910:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
1136949:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3fed6cc74892902ab28df779672578f8
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr018 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr018 20.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr019
"Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | lwz r3,0(r4) | | ;
exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr019 Allowed
Histogram (31 states)
713672:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
1587552:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
605447:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
708126:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
942 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
2226208:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
1024251:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
1537478:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
4258 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
512296:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
733242:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
17727 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
20131 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2056166:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
607896:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
336691:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
391466:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
38458 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1732303:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
32 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2280719:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1019 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
558232:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
6643 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
173684:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1786 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
14915 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1555 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1824577:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
282527:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=660c5e262906b3ab9066962d8bf69882
Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr019 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr019 20.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr020
"Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r2) | | ;
exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr020 Allowed
Histogram (44 states)
445605:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
1946402:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
904218:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
330741:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
1388811:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
396714:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
1011357:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
2777 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
4080 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
876897:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1048163:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
191322:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1095738:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
481791:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1143241:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
191739:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
418008:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
566626:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
169299:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
13 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
377500:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
209641:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
1202356:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
4 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
60 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
658740:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
5570 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
411105:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
3344 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
1658 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
279606:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
1481 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
729221:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
737017:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
280872:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
26 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
21 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
24 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
279036:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
303869:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1584468:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
295781:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
16 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
25042 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=bad92812900a1656a66221eff19f711e
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR
Relax aclwdrr020 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr020 20.37
$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:16:43 CET 2010