類別：編譯時間：Mosaic 未經證明的記憶體存取對齊
當編譯器分析記憶體存取作業 (例如 vector.load、vector.store、tpu.load 或 tpu.store)，但無法靜態證明特定維度使用的動態索引是必要分塊大小的倍數時，就會發生這個錯誤。
錯誤訊息示例：
INTERNAL: Mosaic failed to compile TPU kernel: cannot statically prove that index in dimension 1 is a multiple of 128
at location: ...
The MLIR operation involved:
%14372 = "vector.load"(%14371, %93, %14363) : (memref<4x256xf32, #tpu.memory_space<vmem>>, index, index) -> vector<1x32xf32>
XLA 後端：TPU
總覽
當核心載入或儲存向量時，記憶體位址 (從基本指標加上動態索引計算而來) 必須與硬體上的向量分塊大小對齊。舉例來說，如果某個維度以 128 個元素平鋪，用於存取該維度的動態索引必須是 0、128、256 等。請注意，許多作業 (例如向量載入和儲存) 對靜態索引沒有這類要求。
編譯器會使用靜態分析強制執行這項規定。這項功能會追蹤索引變數的歷史記錄，回溯產生該變數的算術運算 (例如乘法、加法)。如果編譯器無法保證 (在編譯時) 結果值一律可除以圖塊大小，就會引發這項錯誤。
編譯器會將「已證實的對齊方式不一致」和「不明的對齊方式」視為相同。
因此，如果您使用的索引在數學上保證會錯位 (例如i * 128 + 32)，編譯器會引發相同的錯誤。
因此，如果
- 您可以使用執行階段變數 (動態索引) 存取記憶體。
- 編譯器無法分析索引計算邏輯，因為該邏輯過於複雜。
- 索引在數學上有效，但程式碼中缺少明確的證明。
- 靜態分析判定「已證實的錯位」。
偵錯
如要解決這項錯誤，請採取下列任一做法：
1. 明確斷言對齊
如果您知道索引有效，但編譯器無法證明，請使用 tpu.assume_multiple 作業。這會向編譯器保證值可除以特定因數。
2. 使用「對齊載入」和「旋轉」
如果刻意不對齊，請勿載入小型未對齊的向量區隔，而是：
- 載入較大的完整對齊圖塊，然後以動態量旋轉值，將所需資料移至適當位置 (因為系統不支援具有動態開始索引的向量切片)。或
- 重塑或填補張量，使資料從索引 0 開始，且存取之間的步幅符合硬體對齊方式。
- 舉例來說，如果您從位移 1 開始，以大小為 32 的區塊進行疊代，位移會是 1、33、65... (未對齊)。
- 修正方式：將資料重新封裝到新張量中，其中第一個區塊位於 0，且維度會填補至 128。您的位移會變成 0、128、256...，符合對齊規定。
這些方法會耗用較多記憶體，但通常可簡化核心邏輯，且不必手動進行對齊斷言。