循环数组依赖分析 | Codeboy's Blog

形式陈述

一行代码的多次执行是不同节点

固定深度 $d\ge1$ 、非负整数长度 $n_0,\ldots,n_{d-1}$ ，迭代域为

D=\prod_{r=0}^{d-1}\{0,\ldots,n_r-1\}.

某个长度为零时 $D$ 为空。循环体有 $m\ge1$ 条按编号执行的赋值。实例 $x=(\mathbf i,s)$ 表示在坐标 $\mathbf i\in D$ 执行第 $s$ 条赋值；源次序是 $(i_0,\ldots,i_{d-1},s)$ 的词典序，即先比较最左边不同的分量。总实例数 $T=m\prod_r n_r$ 。同一源代码赋值在不同迭代中有不同身份。[1，PDF7–12页]

每条赋值读取由整数常量、加法、乘法和数组读取组成的表达式，先算完右侧，再向一个数组位置写入结果。数组下标是坐标的整数仿射式，例如 $2i_0-i_1+3$ ，不读取内存来决定下标。循环次数、分支和运算符均不受内存值影响；本片段没有分支、调用、异常、I/O、并发或volatile访问。算术使用数学整数，全部合法实例有限且正常结束。观察是所有存储对象的最终内容，不观察内部循环变量或执行用时。

名字相同与位置相同

数组可以有共享存储的视图。参考程序用视图四元组

(o,b,\mathbf h,\mathbf a)

描述对象身份 $o$ 、起始槽偏移 $b$ 、各维长度 $\mathbf h$ 与槽步长 $\mathbf a$ 。逻辑坐标 $\mathbf j$ 对应真实位置

\operatorname{loc}(\mathbf j)=(o,b+\mathbf a\cdot\mathbf j).

每个被访问的下标先满足 $0\le j_r<h_r$ ，算出的槽偏移还必须在对象长度内。不同视图名可能得到同一位置；同一逻辑下标在不同对象中则是不同位置。步长可以为负或零，只要实际访问合法；零步长意味着多个逻辑元素别名。

对实例 $x$ ，记 $R_x$ 为右侧读取的真实位置集合， $w_x$ 为唯一写位置。它们仅依赖固定尺寸、视图和实例坐标，不依赖初始内存。先为全部实例检查位置合法，之后才允许执行；完整内存须给每个声明槽位一个整数。故正确性命题不会夹带“某次碰巧没越界”的条件。

三类有向边

对源次序中 $x<y$ 的每一对不同实例，加入下列带类型及位置见证的边：

\begin{array}{lll} \text{RAW，先写后读：}&w_x\in R_y,&x\longrightarrow y;\\ \text{WAR，先读后写：}&w_y\in R_x,&x\longrightarrow y;\\ \text{WAW，先写后写：}&w_x=w_y,&x\longrightarrow y. \end{array}

RAW保留后者可能需要的新值；WAR保留前者应读到的旧值；WAW保留最终由谁写入。读与读不产生冲突。同一对实例可以有多类边，参考程序分别输出。本页保存全部冲突对，包括可由其他边传递得到的边，不要求中间没有覆盖写入；这是一份便于核验的保守顺序约束，不是最小的最后写入图。

保持定理。 若目标恰执行同一批实例各一次，实例的赋值内容不变，并保持每条上述边的先后，则对该尺寸及视图下的每个合法整数初始内存，目标与源的最终全部存储内容相同。构边对声明的读写冲突是精确的；保持边是语义等价的充分条件，而非必要条件。

直觉

不止“谁把值传给谁”

看两条语句：B[0]:=A[0]，随后 A[0]:=0。第二条没有使用第一条产生的值，只有定义到使用的图可能漏掉它们的联系。但若交换执行，B读到的就变成0。这里需要的是WAR边：先让读者取走旧值，再允许覆盖。

另一个例子是 A[0]:=1，随后 A[0]:=2。两条都不读取A，却由最后一次写决定结果，因此需要WAW边。这些边约束的是对同一存储槽的作用次序，不是表达式的语法相似性。

矩阵累加中的三个标签

计算 C[i,j]:=C[i,j]+A[i,k]*B[k,j]。固定 $(i,j)$ ，取两次迭代 $k=0$ 与 $k=1$ ，它们都读取并写入C的同一个槽，于是这对实例同时有RAW、WAR、WAW三类边。三个标签共享相同方向，保留任意一条已能约束这对次序；分析器保留全部类型，让检查结果说明冲突的来源。

同一C槽的两次累加形成三类顺序约束；不同槽的两次累加在输入数组不别名时没有冲突 — 从真实槽位到循环实例的冲突边

当A、B、C分别属于不同对象时，不同 $(i,j)$ 的实例只共享只读输入，可以交换。同名表达式 C[i,j] 并不意味着所有实例都访问同一槽；必须代入迭代坐标。

例子与边界

实际构出45条边

取 $i=0,1,2$ ， $j=0,\ldots,4$ ， $k=0,1$ ，A、B、C互不别名。源循环按i、j、k嵌套，共30次累加。每个C槽只有两次相关实例，三个标签各一条；15个槽合计45条带类型边。不同C槽之间没有边。

例如实例 $(0,2,0)$ 到 $(0,2,1)$ 的三条边都以C的行优先槽2作见证。把次序改成i、k、j时，两者分别处在目标序列的第2和第7位，仍然先0后1；这里及下载输出的序号从0开始。循环交换会把这个逐边条件用于实际目标代码。

别名会改变整个判断

仍取相同形状，改让A视图指向C对象的前6个槽，A的形状为3×2、步长为(2,1)，C仍为3×5、步长为(5,1)。A[0,0]与C[0,0]现在是同一位置。初始C取1到15，B取1到10。

源中的 $(0,0,1)$ 先更新C[0,0]， $(0,1,0)$ 随后通过A[0,0]读取它，新增RAW边。i、k、j目标把两者置于第5和第1位，倒置该边。重新构图得到101条带类型边，验证器拒绝；源最终C[0,0]=14，目标却为38。把“名叫A”视为“不可能与C别名”会漏掉这个实际反例。

冲突不等于不可证明交换

若两条赋值都写 A[0]:=0，交换后最终内容仍相同，但本分析仍给WAW边。它只使用读写位置，没有使用两个表达式同值这个更强事实。类似地，数学整数上的某些归约可借助结合律、交换律得到更宽松变换；那需要另一份证明，不能直接删掉本图中的边。

如果下标写成 A[B[i]]，本页的静态位置模型不再适用。仅记录一次测试运行的地址，会把“此次没有冲突”错误推广到其他初始B。允许这种语法需要可靠别名分析、运行时检查或更强的语义验证；本参考程序拒绝不属于仿射坐标索引的表达式。

推论与应用

为什么保持边能保持所有内存值

先看没有冲突的两个实例。它们写不同槽，任一写位置都不属于另一实例的读集合，所以先执行谁都不改变另一方的读取值；两次写入也互不覆盖。地址已经固定且合法，两者始终可执行。这正好满足动作独立与交换的使能和结果条件。

再把源序列逐步改成目标序列。从目标第一个尚未对齐的实例x开始，在当前序列中找到x，把它向左越过前面的实例，直到目标位置。每个被越过的y，在源相对次序中先于x，而目标把x排在y前；若它们有冲突，就存在y→x边，违反目标已通过的条件。因此每一次相邻交换都是上段的无冲突交换，保持整个内存。

有限序列至多作有限次交换，最终恰得到目标。逐次保持终态即证明定理。证明不枚举内存值，因而覆盖任意大小的整数；它依赖的是每次交换都读取同样的值。若引入可见读写事件、异常或资源耗尽，观察契约改变，必须重新论证。

算法不变量与真实成本

analyze先按源次序列出身份，计算每个写位置与读取集合，再按编号对 $a<b$ 扫描。处理完一对后，已经输出的边恰是已检查实例对的三种冲突；全部有限对处理完成便得到定义中的完整边集。所有边都从小编号指向大编号，因此天然无环。

设A为输入语法及视图表长度，F为全部实例展开、坐标和仿射地址求值的工作总量，e为带类型边数。以存储身份及槽地址为常数字、散列表查询为期望常数，实际构图时间为

O(1+A+F+T^2).

每对只做两次读集合成员查询和一次位置比较，至多输出三条边。F包含维数与每条仿射式的系数遍历，不能把长下标式视为常数。脚本用计数器式坐标枚举，空域不会先把其他巨大range复制成数组。空间计输入、坐标身份、读集合及边；保守写为 $O(1+A+F+e)$ 。这是关于展开规模的费用，长度参数按二进制输入时，T可以远大于输入位数；整数超出常数字还需另计位运算和哈希成本。

共同终点任务继续把边交给交换和分块。迁移练习：先令A视图与C分离，再改成上述共享前6槽；不执行数值运算，仅根据位置计算，指出首次被i、k、j倒置的边及两个目标编号。答案为 $(0,0,1)\to(0,1,0)$ 的RAW，编号5→1。再问为何只把初始C全置零可能掩盖数值差异，却不能删除这条边。

参考资料

[1] Seth Copen Goldstein，CMU15-411/611，Loop Optimization–2: Locality，2025-04-01，PDF7–14页：实例、循环携带依赖及地址等式。本文的显式视图、全部冲突对枚举和成本为独立教学实现。

[2] Michael E. Wolf、Monica S. Lam，A Data Locality Optimizing Algorithm，PLDI1991，§2.1，PDF4–5页（印刷33–34页）：迭代词典序、距离向量与依赖保持。本文另以逐次交换证明所用有限模型，不实现文中的完整局部性搜索。

形式陈述 ​

一行代码的多次执行是不同节点 ​

名字相同与位置相同 ​

三类有向边 ​

不止“谁把值传给谁” ​

矩阵累加中的三个标签 ​

实际构出45条边 ​

别名会改变整个判断 ​

冲突不等于不可证明交换 ​

为什么保持边能保持所有内存值 ​

算法不变量与真实成本 ​

反向链接