1 引用
Knoth T, Wang D, Polikarpova N, et al. Resource-guided program synthesis[C]//Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019: 253-268.
2 摘要
本文介紹了一種資源導向的程序合成技術，該技術用於合成遞歸程序，並同時滿足功能規範和符號資源約束。該技術是類型引導的，並基於一種新穎的類型系統，該系統將多態細化類型與自動攤銷資源分析的潛在註釋結合在一起。
該類型系統可以進行有效的基於約束的類型檢查，並可以精準地表達基於優化的資源界限。類型健全性的證明表明合成程序在構造上是正確的，而通過緊密地集成程序探索和類型檢查，合成器可以利用用戶提供的資源界限來指導搜索，從而捨棄佔用過多資源的不完整程序。資源引導合成器 ReSyn 被用於對一系列遞歸數據結構操作進行評估。實驗表明，ReSyn 所合成的程序比資源不可知的合成器所生成的程序更加高效。而且使用 ReSyn 進行合成比合成和資源分析的簡單組合要快。ReSyn 還能針對固定的輸入長度生成具有恆定資源消耗的實現，這些實現可用於緩解邊信道攻擊。
3 技術介紹
3.1 類型驅動的程序合成
類型驅動程序合成是一種根據表示為細化類型的高級規範自動生成功能程序的技術。例如，程序員可以描述一個函數，該函數使用以下類型簽名來計算兩個列表之間的公共元素：
該函數可以判斷一個給定值是否在列表中。給定該目標和組件，SYNQUID 構造器可以生成 common 的實現，如圖 1 所示。
圖 1 合成示例
類型驅動的合成通過系統地探索可以從組件庫構建的程序的空間，並使用類型推斷的變體來對目標類型驗證候選程序來進行工作。為了針對細化類型來驗證程序，類型推斷會生成一個細化類型的子類型約束系統。然後將子類型約束簡化為精煉謂詞之間的含義。
3.2 自動攤銷資源分析
為了推斷程序的資源使用情況，我們使用自動攤銷資源分析（AARA）來解決該問題。AARA 是一種用於自動推導功能程序上的資源界限的最新技術，並針對 Resource Aware ML（RaML）中的 OCaml 的子集實現。例如，RaML 能夠自動推導上述函數 common 的遞歸調用次數最壞情況下的邊界為 2m+n*m。
3.3 類型系統
這裡我們將 RE2 的子集定義為形式演算，以證明類型的合理性，該子集包括按他們的取值細化的布爾值和按他們長度細化的列表。之前的程序均使用 Synqid 的表面語法，從表面語言到核心演算的差距涉及歸納類型和細化級別的度量。在技術開發中對該子集的限制僅是出於簡短，並且繼承了 Synqid 的所有功能。
語法
圖 2 示例語法
操作語義
細化
類型
3.4 合成算法
資源約束
增量求解
圖 4 增量求解算法
4 本文主要貢獻
（1）類型系統。本文的第一個貢獻是一種新的類型系統，我們將 Re2 進行優化，該系統將多態細化類型與 AARA 相結合。（2）類型驅動合成。第二個貢獻則是基於 Re2 的資源引導的合成算法。（3）ReSyn 合成器。第三個貢獻是第一個針對遞歸程序的資源引導合成器的實現與實驗評估。
致謝
國家重點研發計劃課題：基於協同編程現場的智能實時質量提升方法與技術（2018YFB1003901）和國家自然科學基金項目：基於可理解信息融合的人機協同移動應用測試研究（61802171）
本文由南京大學軟件學院 2020 級博士張犬俊翻譯轉述。
閱讀更多 慕測科技 的文章
