Wed Dec 23 07:45:34 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
71 :>3:r1=0; 3:r3=0; x=2; y=2;
234 :>3:r1=2; 3:r3=1; x=2; y=2;
245 :>3:r1=1; 3:r3=1; x=2; y=2;
13238 :>3:r1=2; 3:r3=0; x=1; y=2;
28293 :>3:r1=1; 3:r3=0; x=1; y=1;
43425 :>3:r1=1; 3:r3=0; x=1; y=2;
17715 :>3:r1=0; 3:r3=1; x=2; y=2;
12197 :>3:r1=2; 3:r3=0; x=2; y=1;
370130:>3:r1=0; 3:r3=0; x=1; y=2;
394316:>3:r1=0; 3:r3=0; x=2; y=1;
2839643:>3:r1=2; 3:r3=1; x=2; y=1;
1687846:>3:r1=1; 3:r3=1; x=1; y=1;
880230:>3:r1=2; 3:r3=1; x=1; y=2;
910109:>3:r1=1; 3:r3=1; x=1; y=2;
851326:>3:r1=0; 3:r3=1; x=1; y=2;
929092:>3:r1=2; 3:r3=0; x=1; y=1;
864080:>3:r1=0; 3:r3=1; x=1; y=1;
4410238:>3:r1=2; 3:r3=1; x=1; y=1;
4631227:>3:r1=0; 3:r3=0; x=1; y=1;
104164:>3:r1=1; 3:r3=1; x=2; y=1;
1012181:>3:r1=0; 3:r3=1; x=2; y=1;
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 43.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
733 :>3:r1=2; 3:r3=1; x=2; y=2;
888 :>3:r1=0; 3:r3=0; x=2; y=2;
10736 :>3:r1=2; 3:r3=0; x=1; y=2;
687 :>3:r1=1; 3:r3=1; x=2; y=2;
27602 :>3:r1=1; 3:r3=0; x=1; y=1;
34562 :>3:r1=2; 3:r3=0; x=2; y=1;
37225 :>3:r1=1; 3:r3=0; x=1; y=2;
495233:>3:r1=0; 3:r3=0; x=1; y=2;
56325 :>3:r1=0; 3:r3=1; x=2; y=2;
960038:>3:r1=2; 3:r3=0; x=1; y=1;
569615:>3:r1=0; 3:r3=1; x=1; y=2;
871281:>3:r1=1; 3:r3=1; x=1; y=2;
1097585:>3:r1=0; 3:r3=0; x=2; y=1;
3467983:>3:r1=2; 3:r3=1; x=1; y=1;
1524398:>3:r1=1; 3:r3=1; x=1; y=1;
1048706:>3:r1=2; 3:r3=1; x=1; y=2;
1561313:>3:r1=0; 3:r3=1; x=2; y=1;
579455:>3:r1=0; 3:r3=1; x=1; y=1;
3885198:>3:r1=0; 3:r3=0; x=1; y=1;
114239:>3:r1=1; 3:r3=1; x=2; y=1;
3656198:>3:r1=2; 3:r3=1; x=2; y=1;
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 41.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
13271 :>2:r1=0; 2:r3=0; x=2;
334654:>2:r1=2; 2:r3=1; x=2;
1376358:>2:r1=0; 2:r3=1; x=2;
2792857:>2:r1=2; 2:r3=0; x=1;
358688:>2:r1=1; 2:r3=1; x=2;
1789533:>2:r1=0; 2:r3=1; x=1;
6486851:>2:r1=0; 2:r3=0; x=1;
1808570:>2:r1=1; 2:r3=1; x=1;
5039218:>2:r1=2; 2:r3=1; x=1;
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 27.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
452 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
558 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
156 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
12357 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
43692 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
41194 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
476006:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
54404 :>0:r3=1; 3:r1=1; 3:r3=0; y=1;
91167 :>0:r3=0; 3:r1=1; 3:r3=1; y=1;
671649:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
28197 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1822682:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
516747:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
590575:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
954264:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
1666723:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2481666:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
3432701:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
4815259:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
1567393:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
732158:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
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 40.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr004 Allowed
Histogram (39 states)
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2811 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
402 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
542 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
253 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
2101 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
44119 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
926 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1173 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
102 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
12279 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
5948 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
8713 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
106995:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
46001 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
296481:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
272591:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
353 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
185456:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
44253 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
790600:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
287021:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
68488 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
895394:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1500812:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1284440:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
3013706:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
278146:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
186577:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
594228:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1026951:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2331250:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1202603:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1031697:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1418694:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
905431:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1303469:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
497057:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
351936:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
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 50.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
116 :>3:r1=0; 3:r3=0; x=2; y=2;
8974 :>3:r1=2; 3:r3=0; x=2; y=1;
2162 :>3:r1=2; 3:r3=1; x=2; y=2;
82886 :>3:r1=2; 3:r3=0; x=1; y=2;
51795 :>3:r1=1; 3:r3=0; x=1; y=1;
1934 :>3:r1=1; 3:r3=1; x=2; y=2;
38221 :>3:r1=0; 3:r3=1; x=2; y=2;
385729:>3:r1=0; 3:r3=0; x=2; y=1;
1565507:>3:r1=2; 3:r3=0; x=1; y=1;
678790:>3:r1=0; 3:r3=0; x=1; y=2;
824632:>3:r1=0; 3:r3=1; x=1; y=1;
1274130:>3:r1=1; 3:r3=1; x=1; y=2;
228081:>3:r1=1; 3:r3=0; x=1; y=2;
2093737:>3:r1=2; 3:r3=1; x=1; y=2;
1263323:>3:r1=0; 3:r3=1; x=2; y=1;
3324580:>3:r1=2; 3:r3=1; x=1; y=1;
638089:>3:r1=0; 3:r3=1; x=1; y=2;
1411040:>3:r1=1; 3:r3=1; x=1; y=1;
4010047:>3:r1=0; 3:r3=0; x=1; y=1;
131332:>3:r1=1; 3:r3=1; x=2; y=1;
1984895:>3:r1=2; 3:r3=1; x=2; y=1;
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 40.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
37860 :>3:r1=1; 3:r3=0; x=1; y=1;
3382 :>3:r1=0; 3:r3=0; x=2; y=2;
6331 :>3:r1=1; 3:r3=1; x=2; y=2;
7493 :>3:r1=2; 3:r3=1; x=2; y=2;
33840 :>3:r1=2; 3:r3=0; x=2; y=1;
68291 :>3:r1=2; 3:r3=0; x=1; y=2;
396614:>3:r1=0; 3:r3=0; x=1; y=2;
201726:>3:r1=1; 3:r3=0; x=1; y=2;
1071152:>3:r1=2; 3:r3=0; x=1; y=1;
387111:>3:r1=1; 3:r3=1; x=2; y=1;
1518474:>3:r1=1; 3:r3=1; x=1; y=2;
952146:>3:r1=0; 3:r3=0; x=2; y=1;
1811116:>3:r1=2; 3:r3=1; x=1; y=2;
292638:>3:r1=0; 3:r3=1; x=1; y=1;
327627:>3:r1=0; 3:r3=1; x=1; y=2;
1275330:>3:r1=0; 3:r3=1; x=2; y=1;
3615047:>3:r1=2; 3:r3=1; x=2; y=1;
2965712:>3:r1=2; 3:r3=1; x=1; y=1;
3680998:>3:r1=0; 3:r3=0; x=1; y=1;
1224901:>3:r1=1; 3:r3=1; x=1; y=1;
122211:>3:r1=0; 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 42.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
134747:>2:r1=0; 2:r3=0; x=2;
1341503:>2:r1=2; 2:r3=0; x=1;
2298924:>2:r1=1; 2:r3=1; x=2;
5031774:>2:r1=2; 2:r3=1; x=1;
620523:>2:r1=0; 2:r3=1; x=1;
6368014:>2:r1=0; 2:r3=0; x=1;
1549074:>2:r1=1; 2:r3=1; x=1;
2028233:>2:r1=2; 2:r3=1; x=2;
627208:>2:r1=0; 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 25.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
798 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
118381:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
20080 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
155382:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
21708 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
104976:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
181318:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
432072:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
493437:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
19767 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1069779:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
654757:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
481618:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
2076883:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1480827:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
2190348:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1720626:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
2639620:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
4274236:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
1382305:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
481082:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
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 41.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr009 Allowed
Histogram (38 states)
4419 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4510 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
453 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
3725 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
29698 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
27233 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
209473:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
16088 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3494 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
242114:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
79 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
54280 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
79467 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
16397 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
86069 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
536081:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
364823:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
206707:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
316111:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
738922:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
163693:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1326457:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
147884:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
270318:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1432590:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
916312:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1099787:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1189472:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
68316 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
111379:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2599714:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1399662:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
769931:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
2027562:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1725252:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
119683:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
920700:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
771145:>0:r3=1; 3:r1=0; 3:r3=1; x=1; 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 50.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r7,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r8,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
52877 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
140113:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
131242:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
65635 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
823001:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
78820 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
1353018:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
1852469:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
509675:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
1480536:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
2400126:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
6308999:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
1861228:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
2595928:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
346333:>0:r1=1; 0:r3=0; 2:r1=0; 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 30.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
80 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1226 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
3718 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
173771:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
38384 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1161504:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
174590:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2417164:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1339030:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1082488:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
4627952:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
707918:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
4210631:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1950549:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
2110995:>1:r1=0; 1:r3=0; 3:r1=0; 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 35.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
7 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
26 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1759 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1089 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
288 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1855 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
107584:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
55734 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
34139 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
287358:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
14784 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
11322 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
164582:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
87036 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
33129 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
50883 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
474687:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
355188:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
786860:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1382699:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
116763:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
505714:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1089216:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1279044:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1496845:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1073291:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1418464:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
963804:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
204857:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2418151:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1446762:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3244305:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
891775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 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 44.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
3950 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
4479 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
13046 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
178424:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1027746:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
132243:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
422502:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
913476:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2368072:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
3787034:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
4139105:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1892125:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
628950:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2881905:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1606943:>1:r1=1; 1:r3=1; 3:r1=0; 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 34.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr014 Allowed
Histogram (32 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
20 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1273 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4715 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1264 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
38795 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
6162 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
122260:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
118188:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
72219 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
37373 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
45072 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
14147 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
13386 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
96327 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
662935:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
179152:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
67619 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
525071:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1327022:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
46899 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
191806:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1990257:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1332105:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
342757:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1537899:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1612035:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
153830:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2293890:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
5416425:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1749087:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 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 43.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
93 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
790 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
63725 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
21470 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
708823:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1030380:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
4813580:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
1462347:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
481263:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
103427:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
2037825:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
1373997:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
4516882:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
2737113:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
648285:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
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 35.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
1741 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
4402 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
74521 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
74914 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
164797:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
1394472:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
1289502:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
863823:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1085672:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1509563:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
322741:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
3599574:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
3743066:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
4444414:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
1426798:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
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 36.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
3256052:>0:r3=1; 2:r1=1; 2:r3=0;
1517191:>0:r3=0; 2:r1=0; 2:r3=1;
41300 :>0:r3=0; 2:r1=0; 2:r3=0;
1110041:>0:r3=1; 2:r1=0; 2:r3=1;
6422360:>0:r3=1; 2:r1=0; 2:r3=0;
1417327:>0:r3=0; 2:r1=1; 2:r3=1;
6235729:>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 23.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
448 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
48351 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
56397 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
152541:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
3819 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
651197:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
2500169:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1762747:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
1101254:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
1444649:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
3733268:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
822791:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
4321584:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
2890621:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
510164:>0:r3=1; 1:r3=1; 3:r1=0; 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 36.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr019 Allowed
Histogram (31 states)
1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1981 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1091 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
33666 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
121 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
139631:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
7935 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
432858:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
45413 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
25082 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
59164 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
436364:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
2050 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
399560:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1067520:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
5048 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1504263:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
546092:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
142930:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
454009:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1893779:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1061037:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1352874:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
1275478:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1046792:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
88108 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2191653:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
898870:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
323218:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
1247183:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
3316229:>0:r3=1; 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 45.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr020 Allowed
Histogram (45 states)
3 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
1 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
28 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
12 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
40 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
8 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
798 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
129 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
3399 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
5863 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
216 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
25578 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
24471 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
6087 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
5210 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
192324:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
22901 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
62871 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
1055392:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
402162:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
650567:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
391706:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
190971:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
918059:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
1676343:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
225069:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
165205:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
439181:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
156970:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
1076353:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
195712:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
1083396:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
168844:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
401983:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
439797:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
143360:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
1027923:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
1066716:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
433302:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
1668977:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
2645014:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
2274713:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
467924:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
237458:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
46964 :>0:r3=0; 1:r3=1; 3:r1=0; 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 48.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr021
"Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr021 Allowed
Histogram (7 states)
55715 :>2:r1=1; 2:r3=0; x=1;
127993:>2:r1=0; 2:r3=0; x=2;
3549793:>2:r1=0; 2:r3=1; x=2;
6401391:>2:r1=0; 2:r3=0; x=1;
3300253:>2:r1=1; 2:r3=1; x=1;
10621 :>2:r1=1; 2:r3=1; x=2;
6554234:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=aeec733dac4af8be94573c9aff9d0c10
Cycle=Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR
Relax aclwdrr021 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr021 30.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr022
"Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr022 Allowed
Histogram (7 states)
55132 :>2:r1=1; 2:r3=0; x=1;
361610:>2:r1=0; 2:r3=0; x=2;
5417846:>2:r1=0; 2:r3=1; x=2;
6324545:>2:r1=0; 2:r3=0; x=1;
3588432:>2:r1=1; 2:r3=1; x=1;
21062 :>2:r1=1; 2:r3=1; x=2;
4231373:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=fb989d16658311d76866354f8a671029
Cycle=Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR
Relax aclwdrr022 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr022 29.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr023
"Fre SyncdWW Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
Test aclwdrr023 Allowed
Histogram (3 states)
19151842:>1:r1=0; 1:r3=0;
3160018:>1:r1=1; 1:r3=1;
17688140:>1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=501f8f5a33589295352fe1de9678142b
Cycle=Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr023 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr023 18.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr024
"Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr024 Allowed
Histogram (15 states)
77 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
142 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
703 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
708 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
309810:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
125045:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
96086 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1803675:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2557855:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
3024588:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
4123943:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
4862722:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
232461:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
428143:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
2434042:>1:r1=0; 1:r3=1; 3:r1=0; 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=d941e505b27c9a2748aeb4651a9cb643
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr024 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr024 39.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr025
"Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 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_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr025 Allowed
Histogram (32 states)
58 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
109 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2768 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1025 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
93 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2675 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1183 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
127 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1067 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1064 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
561 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
17012 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
65494 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
36583 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
656448:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
86937 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
920506:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
958676:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
159259:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1548336:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
637398:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
443742:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2464439:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3273436:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1281741:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1710566:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
846737:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
599655:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2590354:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
295073:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
684603:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
712275:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=32b005fb973345d626b38029866e06f9
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr025 No ACLwSyncdRR
Safe=Fre SyncsWW SyncdWW
Time aclwdrr025 49.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr026
"Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr026 Allowed
Histogram (15 states)
395 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
402 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1199 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
13438 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
103006:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
408230:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
515484:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1910885:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2475332:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3716828:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1760828:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
4249327:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
704357:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
716970:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
3423319:>1:r1=1; 1:r3=1; 3:r1=0; 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=7a7cbc5359389bdb4170629397f77be6
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr026 No ACLwSyncdRR
Safe=Fre SyncdWW LwSyncdWW
Time aclwdrr026 39.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr027
"Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 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_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr027 Allowed
Histogram (32 states)
9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
8 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
87 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
45 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
30 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
434 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
29 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1426 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1011 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
3372 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2543 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
38414 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
17372 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
56153 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
55181 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
79642 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
98006 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
14587 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
272535:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1294511:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
392505:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1288415:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1767099:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
59551 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1518679:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
113186:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2303453:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
105242:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
3793016:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
566288:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1598523:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
4558648:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c2a2e1328465d78b88dcae553e33604e
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr027 No ACLwSyncdRR
Safe=Fre SyncdWW LwSyncsWW
Time aclwdrr027 46.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr028
"Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz 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 (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr028 Allowed
Histogram (7 states)
50207 :>0:r3=1; 2:r1=1; 2:r3=0;
243057:>0:r3=0; 2:r1=0; 2:r3=0;
4177415:>0:r3=0; 2:r1=0; 2:r3=1;
7453540:>0:r3=1; 2:r1=0; 2:r3=0;
2541621:>0:r3=1; 2:r1=1; 2:r3=1;
18207 :>0:r3=0; 2:r1=1; 2:r3=1;
5515953:>0:r3=1; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=eebdc6b096cdd9c24f38c118593f06bb
Cycle=Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr028 No ACLwSyncdRR
Safe=Fre SyncdWW SyncdWR
Time aclwdrr028 29.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr029
"Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=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 | sync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2: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 r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr029 Allowed
Histogram (13 states)
65 :>0:r3=2; 2:r1=0; 2:r3=1; y=2;
11680 :>0:r3=2; 2:r1=1; 2:r3=2; y=2;
35930 :>0:r3=1; 2:r1=1; 2:r3=2; y=1;
2343405:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
724365:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
244036:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
2804233:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
5449462:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
2511570:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
1301336:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
4053075:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
117531:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
403312:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=4ab12861c7fd48307d5dbbb06073fa65
Cycle=Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr029 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWW
Time aclwdrr029 28.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr030
"Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 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_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: sync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr030 Allowed
Histogram (71 states)
1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
5 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
7 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
22 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
20 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
317 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
170 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
38 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
309 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
166 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
93 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
80 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
12 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
72 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4526 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
128 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
150 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
327 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3921 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
16090 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5913 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1249 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4444 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5739 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
25273 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
23593 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
8782 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
38301 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
67931 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
66959 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
290088:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
9280 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
51686 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
108816:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
5589 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
41643 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
38261 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
57408 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
14055 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
182890:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
25517 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
580478:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1167416:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
76038 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
419353:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
488482:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
196552:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
562649:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
146567:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
19690 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1201384:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
12233 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
240476:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
167044:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
789347:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
643247:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
937700:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
249217:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
892039:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
170487:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
814018:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
970505:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1120158:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
907054:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
329430:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
182392:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
702474:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1181712:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1156340:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1464644:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1111003:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ee8538d5ca48a381e732df1d7c7a6726
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr030 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr030 82.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr031
"Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,2 | ;
stw r3,0(r4) | | stw r3,0(r2) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: sync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr031 Allowed
Histogram (33 states)
2 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
127 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
201 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
15268 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
375 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
8305 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2;
8963 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
5394 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
2011 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2;
2694 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
110741:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
7093 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
408 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
79233 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
237980:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
776733:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
1118113:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
393054:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
984393:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
1383096:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
234880:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
1530860:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
425897:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1403157:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
1293147:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
83668 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
2543274:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
524352:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
703724:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
627072:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
2366742:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
1057361:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
2071682:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7e70701bff0ff65c82954a7448132407
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr031 No ACLwSyncdRR
Safe=Fre SyncsWW LwSyncdWW
Time aclwdrr031 48.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr032.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr032
"Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: sync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr032 Allowed
Histogram (69 states)
4 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
5 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
5 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
8 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
11 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
6 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
74 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
8 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
16 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
39 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
262 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
14 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
697 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2840 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4543 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
6626 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2320 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
9940 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3946 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
478 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
7940 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
5107 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
5484 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4005 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1334 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
18948 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
17214 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
10444 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
51665 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
9821 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
63447 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5158 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
39985 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
105934:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
10805 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
22193 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
570792:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
32923 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
90152 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
25570 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
7521 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
113777:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
360217:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
183471:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
143021:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
830840:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
379681:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
856059:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
111043:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
112055:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
44483 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
200812:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
971520:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1076303:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
111305:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
212886:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1437808:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
693077:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2037803:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1239854:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
17920 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1579356:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1225097:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1354292:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
381838:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3070996:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
116191:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=74930e6bce52d51f9df9817f8385847f
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr032 No ACLwSyncdRR
Safe=Fre SyncsWW LwSyncsWW
Time aclwdrr032 79.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr033.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr033
"Fre SyncdWR Fre SyncsWW 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 | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr033 Allowed
Histogram (15 states)
73 :>0:r3=1; 2:r1=1; 2:r3=0; x=2;
556 :>0:r3=1; 2:r1=1; 2:r3=1; x=2;
87688 :>0:r3=0; 2:r1=0; 2:r3=0; x=2;
74510 :>0:r3=2; 2:r1=1; 2:r3=0; x=2;
846521:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
1056069:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
1430789:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
1203161:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
1240018:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
1844061:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
1049804:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
125846:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
5361386:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
230941:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
5448577:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=9aeeb761b71ddabb3db56388750f2a1a
Cycle=Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr033 No ACLwSyncdRR
Safe=Fre SyncsWW SyncdWR
Time aclwdrr033 31.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr034.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr034
"Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr034 Allowed
Histogram (7 states)
42232 :>2:r1=1; 2:r3=1; x=2;
59924 :>2:r1=0; 2:r3=0; x=2;
170389:>2:r1=1; 2:r3=0; x=1;
2905430:>2:r1=0; 2:r3=1; x=2;
4895171:>2:r1=0; 2:r3=1; x=1;
5755927:>2:r1=1; 2:r3=1; x=1;
6170927:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=10939fdb629e01d3ec7a75f951037026
Cycle=Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr034 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr034 30.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr035.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr035
"Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
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 (x=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr035 Allowed
Histogram (7 states)
111715:>2:r1=1; 2:r3=0; x=1;
269252:>2:r1=0; 2:r3=0; x=2;
2476197:>2:r1=0; 2:r3=1; x=1;
5389482:>2:r1=0; 2:r3=1; x=2;
5629343:>2:r1=1; 2:r3=1; x=1;
87918 :>2:r1=1; 2:r3=1; x=2;
6036093:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=b62ccd86d3f88c50d13b5221a86b68a5
Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr035 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr035 30.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr036
"Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
Test aclwdrr036 Allowed
Histogram (3 states)
13967721:>1:r1=1; 1:r3=1;
19284699:>1:r1=0; 1:r3=0;
6747580:>1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=25520ac6610aa6339bae2caee0005d5b
Cycle=Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr036 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr036 19.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr037
"Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr037 Allowed
Histogram (15 states)
11447 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
8129 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2770 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2281 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
345379:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
260146:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
734439:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1940965:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
641320:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
3175956:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
3300567:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1261644:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
3830932:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3358560:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1125465:>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=e45e2fb06db799317c9d3aeed10f6d45
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr037 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr037 39.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr038
"Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 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_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr038 Allowed
Histogram (32 states)
9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
6 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
26 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
284 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1196 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2770 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
6364 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2036 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
11680 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
52913 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
15507 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1928 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
24091 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
15464 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
122794:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
59225 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
101297:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
206407:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
54442 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
63830 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
330583:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
207920:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
534962:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1251899:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1520763:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
337943:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1987031:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3580442:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3360422:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2006181:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
2652279:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1487306:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=459d76f119641ec12aab94d071c86542
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr038 No ACLwSyncdRR
Safe=Fre LwSyncsWW LwSyncdWW
Time aclwdrr038 47.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr039.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr039
"Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz 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 (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr039 Allowed
Histogram (7 states)
318233:>0:r3=1; 2:r1=1; 2:r3=0;
246265:>0:r3=0; 2:r1=0; 2:r3=0;
4454767:>0:r3=0; 2:r1=0; 2:r3=1;
6620229:>0:r3=1; 2:r1=0; 2:r3=0;
4839319:>0:r3=1; 2:r1=1; 2:r3=1;
108895:>0:r3=0; 2:r1=1; 2:r3=1;
3412292:>0:r3=1; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=9adf86efa9ed99398ed262e7a29cb549
Cycle=Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr039 No ACLwSyncdRR
Safe=Fre SyncdWR LwSyncdWW
Time aclwdrr039 27.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr040.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr040
"Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=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 | lwsync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2: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 r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr040 Allowed
Histogram (13 states)
75 :>0:r3=2; 2:r1=0; 2:r3=1; y=2;
67574 :>0:r3=1; 2:r1=1; 2:r3=2; y=1;
534461:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
37622 :>0:r3=2; 2:r1=1; 2:r3=2; y=2;
2628098:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
402053:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
1556481:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
1030369:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
5150756:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
2658162:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
4921077:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
709877:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
303395:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=1a7c6d1dc4425965c5dae6a980780759
Cycle=Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr040 No ACLwSyncdRR
Safe=Fre SyncsWR LwSyncdWW
Time aclwdrr040 28.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr041.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr041
"Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW 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) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr041 Allowed
Histogram (65 states)
1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
11 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
7 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
18 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1019 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
15 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
345 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
231 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1431 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1082 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2512 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
12082 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1589 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1418 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
419 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
621 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
24007 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
753 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1254 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
184967:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
7623 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5265 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2115 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
6666 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
27286 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
94510 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
86132 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
11146 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
12393 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
8858 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
83393 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
17298 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
51690 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
9071 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
112472:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
23203 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
112332:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
12504 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1921 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
160871:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
36273 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
175285:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
74585 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
607870:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
188411:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
502585:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1540768:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
867090:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
179618:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1476822:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
316974:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
38316 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
182850:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2090742:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1376813:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
260552:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
398970:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1924016:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1418358:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5262563:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=f658f820f1d5e1aea992b078ad3de29c
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR
Relax aclwdrr041 No ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr041 82.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr042.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr042
"Fre SyncdWR Fre LwSyncsWW 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 | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,2
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr042 Allowed
Histogram (15 states)
7 :>0:r3=1; 2:r1=1; 2:r3=0; x=2;
52 :>0:r3=1; 2:r1=1; 2:r3=1; x=2;
8876 :>0:r3=2; 2:r1=1; 2:r3=0; x=2;
143390:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
484648:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
110656:>0:r3=0; 2:r1=0; 2:r3=0; x=2;
742142:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
224324:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
438040:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
1671209:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
2125343:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
1186311:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
6450655:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
239712:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
6174635:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=9862f681ad48c0682ff709f0b167939f
Cycle=Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR
Relax aclwdrr042 No ACLwSyncdRR
Safe=Fre SyncdWR LwSyncsWW
Time aclwdrr042 30.44
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Wed Dec 23 08:14:02 CET 2009