OCaml 編譯器 - 2021 年 5 月
我很樂意發布第二期的「OCaml 編譯器開發電子報」。(這絕非詳盡無遺:很多人最終沒有時間寫東西,這沒關係。)
當然,歡迎隨時評論或提問!
如果您一直在開發 OCaml 編譯器,並且想要分享一些內容,請隨時在這串討論中發文!如果您希望下次我準備電子報時(未來某個隨機時間點)與您聯繫,請透過電子郵件 (gabriel.scherer at gmail) 告知我。
上一期
Gabriel Scherer 和 Nicolas Chataing (@gasche 和 @nchataing)
[Gabriel 撰寫] 我最近與編譯器相關的主要活動是與我的實習生 Nicolas Chataing 合作,實作變體建構子拆箱的原型,這是 Jeremy Yallop 提出的核心子集 (https://github.com/ocaml/RFCs/pull/14)。目前,如果變體只有一個建構子(帶有單一參數),OCaml 可以將其「拆箱」。
type t = Int of int [@@unboxed]
Jeremy 的想法是支援有其他建構子的情況,但建構子參數的標籤(立即值或區塊建構子標籤)與此類型中任何其他值的標籤不相交。
type t = Short of int [@unboxed] | Long of Mpz.t
Nicolas 的原型實作進展順利,遇到並解決了一些有趣的挑戰,並沿途進行了一些重構 PR (#10307, #10412, #10428)。
一個關鍵要素是能夠計算 OCaml 類型的「頭部形狀」,這是其值可能標籤集合的過度近似。我們在執行此操作時遇到了一些工程和研究問題。應該在程式碼庫的哪個位置計算此值(請注意循環模組相依性)?在存在相互遞迴類型的情況下,我們是否可以精確地計算此資訊,而不會有非終止的風險?
我們正在從 Leo White 和 Stephen Dolan 提出的通用方法中汲取靈感,以便根據需求計算這些「類型宣告屬性」,而不是作為類型宣告簽章的一部分(請參閱他們關於「立即性」的提案,#10017, #10041),但我們的屬性需求更頻繁(建構子的任何出現),並且更細微(它對類型參數敏感),因此我們必須針對新問題提出一些解決方案。(一個近親是 `get_unboxed_type_representation`,它透過使用 fuel 來避免非終止,而我們想要比這更好的東西。)
我們在以下簡短摘要中詳細討論了我們對終止的處理: 展開沒有迴圈的 ML 資料類型定義。
Xavier Leroy (@xavierleroy)
我與 Damien Doligez 和 Sadiq Jaffer 合作制定了「安全點」提案 (#10039),這對於推進整合 Multicore OCaml 是必要的。我將支援插入輪詢的靜態分析重新表示為向後資料流分析,使其更容易理解且更穩健。我們還討論了是在迴圈頂部還是底部插入輪詢。這兩種策略都在 PR 的目前狀態中實作,而 Sadiq 目前正在對它們進行效能基準測試。
所有這些重新燃起了我對資料流分析的興趣。我編寫了一個通用的向後資料流分析器,該分析器由一個抽象域和一個轉換函式參數化 (#10404)。最初,我打算僅將其用於插入輪詢,但我也用它來重新實作活變數分析,這對於暫存器配置和無效程式碼消除至關重要。舊活變數分析的一個問題是,它的時間複雜度與迴圈的巢狀層數成指數關係。新的通用分析器透過不從抽象域的底部系統性地開始定點迭代,而是從先前找到的定點開始(如果有的話)來避免這個陷阱。這使得活變數分析與迴圈的巢狀層數成線性關係,並且在最壞的情況下,與函式的大小成三次關係,而不是指數關係。
然後,我將相同的技巧應用於預防性插入溢出和重載的兩個通道 (#10414)。這些是「分析並同時轉換」的通道,所以我無法使用通用的資料流分析器,但我可以重複使用相同的改進的定點迭代策略,再次避免迴圈巢狀層數的指數行為。例如,一個由 16 個巢狀「for」迴圈組成的簡單函式現在只需幾毫秒即可編譯,而之前需要幾秒鐘。
Jacques Garrigue (@garrigue)
本月沒有新的 PR,但我一直在處理四月份開始但尚未合併的 PR
- #10348 改善了統一期間的展開方式,以避免一些虛假的 GADT 相關歧義錯誤
- #10364 變更了模式比對案例主體的類型檢查方式,允許在某些非主要情況下發出警告;它還揭示了類型檢查器內部的許多與主要性相關的錯誤
- #10337 透過將 type_expr 設為抽象類型(與 Takafumi Saikawa (@t6s) 合作),強制始終操作類型的標準化檢視
對於最後一個 PR,我們有趣地觀察到,雖然這使得對 repr 的呼叫次數增加了最多 4 倍,導致例如在 stdlib 中增加了 4% 的額外負擔,但我們看不到 Coq 編譯的效能下降。
我也發現了 GADT 實作中一個新的主要性錯誤(請再次參閱 #10348),幸運的是它不應影響健全性。
在一個稍微不同的方向上,我已經開始研究針對 Coq 的後端:https://github.com/COCTI/ocaml/tree/ocaml_in_coq
如果將 -coq 選項新增至 ocamlc,您將會得到一個 .v 檔案,而不是 .cmo。它仍處於非常早期的階段,只能編譯核心 ML 程式,包括引用。與 coq-of-ocaml 的主要區別在於,翻譯旨在保留健全性:產生的 Coq 程式碼可以鍵入和求值而無需公理,並且應該化簡為與來源程式相同的結果,以便 Coq 的類型健全性保證 ocaml(針對個別程式)的類型健全性。在這一點上,它僅依賴於 Coq 的正向性限制的單一鬆弛。
Thomas Refis (@trefis)
最近,Didier Rémy 和我一直在研究模組化顯式,這是核心語言和模組語言之間的一個小型延伸,旨在幫助操作一級函子,並透過一個(暫時)稱為相依函式的新建構,在核心語言中產生對模組參數抽象的錯覺。
這個建構首先在 模組化隱式 提案的背景下引入;大致來說,如果你去除該提案的「隱式參數解析」部分,剩下的就是它。
因此,它是通往模組化隱式的自然墊腳石,並且已經有其自身的獨立 PR:#9187,由 Matthew Ryan 貢獻。
最近 Didier 和我一直關注的是產生對該功能的更正式描述及其與一級模組的關係,以及一些論證,以證明即使在沒有模組化隱式的情況下,將其新增到語言中也是合理和可取的。
Stephen Dolan (@stedolan)
我剛開啟了 #10437,這允許在簽章和 GADT 中使用類型變數的顯式量詞,這是我幾個月前承諾給 OCaml 維護者的一个小功能。(背後的動機是這些顯式量詞為放置版面配置資訊提供了一個很好的位置,但我認為它們本身就值得擁有)。
注意:#10017 / #10041 中提到的按需立即性提案,Gabriel 上面提到過,是從實驗分支 https://github.com/janestreet/ocaml/tree/layouts 中類型檢查系統的一部分中提取的,該系統另外允許在給定立即性/版面配置的類型上進行量化:例如,可以寫 `type ('a : immediate) t = { foo : 'a }` 並使推論等按預期工作。
Sadiq Jaffer (@sadiqj)
安全點 PR #10039 有一些更新。它現在有了一個新的靜態分析,由 Xavier Leroy 和 Damien Doligez 編寫,並且在所有 64 位元平台上都有可用的程式碼發射器。
靜態分析在迴圈中的輪詢放置方面具有一定的彈性。我們在 amd64 和 arm64 上進行了效能基準測試,選擇了在 Sandmark 套件中產生略少指令和分支的選項。除了某些重構之外,我認為 PR 沒有其他任何未解決的問題。
在安全點的基礎上,我應該很快會有一個屬性可以提出,這將使具有原子程式碼區塊的使用者能夠安全地遷移到具有安全點的 OCaml 版本。草案 PR 或 RFC 將很快推出。
我還在處理 儀器化執行期。該專案的目標之一是能夠持續監控在生產環境中執行的 OCaml 應用程式。為此,我正在評估儀器化執行期的效能開銷(無論啟用與否),確定減少開銷需要哪些工作,以及我們如何修改執行期以持續擷取度量和事件。
Anil Madhavapeddy (@avsm)
Ewan Mellor 和我正在開發一個 CI,這將使測試 OCaml 編譯器的個別變更集並針對一組 opam 套件執行「反向相依性」變得容易,以便精確隔離導致失敗的原因。
建置 opam 套件的失敗可能有多種原因。這包括針對已發布的穩定編譯器建置失敗,僅在 OCaml 主幹上失敗(但在已發布的編譯器上成功),以及僅在 OCaml 主幹 + 所討論的 PR 上失敗。我們的新的 CI 專注於分類這些情況中的哪一個導致了套件建置失敗。有了這個 CI,我們應該能夠快速確定 PR 的影響以及對套件生態系統的潛在迴歸。一旦 CI 在 OCaml 多核心樹上穩定下來,我計劃將其提交為針對主線 OCaml 執行的 CI。
工作樹位於 ocaml-multicore-ci(雖然它被稱為「多核心 CI」,但實際上它只是變成了一個「ocaml-compiler-ci」,我們將在第一次發布之前重新命名儲存庫)。
Florian Angeletti (@Octachron)
這週我花了一些時間在 #10361 中,為類型宣告的差異訊息新增了交換(swaps)和移動(moves)的功能。
(以及 OCaml 4.13.0 第一個 alpha 版本的發布)
這個 PR 的核心概念是,當比較
type t = { a:int; b:int; c:int; d:int }
和
type t = { a:int; c:int; d:int }
在錯誤訊息中,最好注意到我們缺少一個欄位,而不是試圖比較欄位 b
和 c
。
有了為函式子差異引入的機制,這件事實作起來相當簡單。我從去年 12 月開始嘗試這個選項,並且在函式子差異 PR 合併 #9331 後,我在四月提出了 PR #10361。
然而,與函式子相比,在類型宣告中,我們還有一個額外的資訊:特定位置的欄位和建構子的名稱。不使用這個資訊會產生有點奇怪的錯誤訊息
module M: sig type t = { a:int; b:int } end = struct type t = {b:int;
a:int}
1. Fields have different names, x and y.
2. Fields have different names, y and x.
這裡,最好識別出這兩個欄位已經被交換了。
一個簡單的方法,在不增加差異複雜度的前提下,是在差異演算法產生的最佳修補程式上,事後識別交換。
這樣一來,我們可以在不增加錯誤分析成本的情況下,將之前的錯誤訊息替換為
1<->2. Fields x and y have been swapped.
。
當欄位在介面和實作之間的順序改變時,也會發生類似的情況
module M: sig
type t = { a:unit; b:int; c:float}
end = struct
type t = { b:int; c:float; a:unit}
end
解釋說,實作可以透過在欄位 b
之前新增一個欄位 a
,並在 c
之後刪除另一個欄位 a
來轉換為介面,是正確的。但如果將問題總結為
1->3. Field a has been moved from position 1 to 3
會好得多。現在,複合移動都被識別出來了。
對 OCaml 中的錯誤訊息感興趣的人,也應該看看 Antal Spector-Zabusky 在 #10407 中的出色工作,他透過擴展完整的錯誤追蹤來改善模組層級的錯誤訊息。(這兩個 PR 是相當互補的。)