Bank Conflict Free问题建模，异或方法的数学原理

type

status

date

slug

summary

总结

本文将bank conflict free问题进行了建模抽象，并从数学上验证 swizzle 使用异或解决这个问题的正确性。然后本文从抽象后的问题本身出发，借助AI正向求解这个问题，并从AI解决的思路中学习。

背景

cute 之 Swizzle

How to understand the bank conflict of shared_mem

Bank Conflict free 的几种方式看了reed大佬的文章，了解到了cute swizzle内部是通过异或来解决Bank冲突的，但是关于为什么异或能解决这个bank冲突，没有给出进一步解答，这里记录我关于这个 “为什么” 的理解。

问题描述

关于解决bank冲突，本质上是希望改变smem中数据的物理layout，使得每个 transaction 取出来的数据都是有效的。（一个transaction最大为128byte，这里我理解就是对应32个bank，一个bank宽4byte)。下图是cute 之 Swizzle中的配图，同一个颜色的数据表示wrap一次访存的数据，假设图里有32行，则一次访问128byte，全都在同一个bank上，导致需要32个transaction，每次的transaction出来的数据直保留目标bank的4byte，效率很低。

因此我们希望将这些数据分布到不同的bank上，使得一次transaction就能把他们全部取出来同时不改变原kernel关于计算的算法逻辑，只改变数据摆放的物理layout。

问题抽象

假设我们有一个矩形网格，宽W,高H，且 H < = W，H代表数据的二维行数, 这里W代表bank数量, W为2的幂。对于网格里的每个位置，我们可以用二维坐标(row, col)来表示. 我们希望找到一种映射方式, 使得：

原本在同一列的元素，经过映射后，全都分布在不同的列。 (解决冲突问题)

经过映射后的元素，依然在这个网格内。（不考虑padding, 不能越界呀）

两个不同位置的元素，不会映射到同一个位置去。 (映射前后一一对映)

用数学语言描述就是; 给定映射函数，row,row',col,col'均为非负整数，且 , W为2的幂满足以下两个性质：

性质1：对于任意的，如果，则

性质2： f是双射的. (映射前后一一对应)

cute swizzle

cute swizzle对于这个问题的解是: ，其中表示异或运算。以下分别证明这两个性质。(以下证明由grok3完成)

证明性质1

由函数定义，。因此，输出二元组的第二项（即）为：

具体到性质1，我们有：

需要证明：如果，则。

反证法：

假设，但。

对等式两边同时异或，利用异或运算的性质（）：

左边计算：

右边计算：

于是：

这与假设矛盾。

结论：性质1成立。

证明性质2

需要证明 f 是单射又是满射的，

单射

满射

正向求解？

上面我将bank conflict free问题抽象成一个“构造满足特定条件的函数”的问题，然后再去方向证明swizzle关于这个问题的解的正确性，但是如何从这个问题正向得到这个解呢？我贫瘠的大脑，可能不一定能想到用异或这个操作，于是我决定问问AI。

我把抽象出来的问题丢给了grok3 think模式， grok3首先给出了如下解，并证明了正确性。

这个解就是Bank Conflict free 的几种方式里面提到的第二种方式。但这种方式计算col'需要两条指令，加法和按位与(如果b为2的幂，则 a%b == a&(b-1) )，但是我们知道如果用异或的话，只有一条指令，更简洁，于是我进一步追问ai，让他不要用取模，给出一个对计算机更友好的解，然后就得到了异或的解, 真是非常的Amazing !