天天看點

麻省理工為高性能計算機開發新的程式設計語言

在上月于費城舉辦的程式設計語言原理大會上,麻省理工學院(MIT)計算機科學與人工智能實驗室(CSAIL)二年級博士生 Amanda Liu 表示,使用他們專為高性能計算而設計的新程式設計語言,可以很好地兼顧速度與正确性。此前人們普遍認為,速度與可靠性存在不可避免的權衡。

麻省理工為高性能計算機開發新的程式設計語言
據悉,Liu 與加州大學伯克利分校博士後 Gilbert Louis Bernstein、MIT 副教授 Adam Chlipala 和助理教授 Jonathan Ragan-Kelley 一道,描述了他們最近開發的“張量語言”(A Tensor Language)。

ATL 語言旨在産生一個數字或張量,所謂張量就向向量和矩陣的泛化。

向量是一維對象(通常由單獨的箭頭表示),矩陣是相對臉熟的二維數字數組。

而張量是 n 維數組,例如可用 3×3×3 的數組形式、或更高 / 更低的次元。

a verified framework for optimizing tensor programs(via)

計算機算法或程式的全部意義,在于啟動特定的計算。不過想要實作目的,可用諸多不同的方式來編寫。正如該研究團隊在即将發表的會議論文中所寫的那樣:

各種不同的代碼實作方式讓人眼花缭亂,某些方案的速度要快得多。

但鑒于高性能計算的資源開銷極其誇張,ATL 希望用更高效的方式來修改或重寫程式。

普通開發者習慣從最容易着手的地方開始程式設計,但這顯然沒有考慮到最佳的運作效率,因而需要進一步調整優化。

麻省理工為高性能計算機開發新的程式設計語言

假設圖像由 100×100 的數字數組表示,每個數字對應一個像素,且希望獲得這些數字的均值。

這項工作可通過兩階計算完成,首先确定每行的平均值,然後擷取每列的平均值。

ATL 提供了一個相關的工具包 —— 計算機科學家稱之為“架構”—— 能夠展示如何将這兩個步驟轉換為更快的一步過程。

麻省理工為高性能計算機開發新的程式設計語言

Liu 補充道:我們可借助所謂的“證明助手”(proof assistant),來確定這種優化的正确性。

有鑒于此,團隊在現有的 Coq 語言的基礎上建構了新語言。而其中包含的證明助手,具有以數學嚴謹的方式證明其斷言的内在能力。

不過在 MIT 團隊看來,Coq 有另一個值得稱道的内在特性 —— 用它編寫或适配的程式,是無法在無限循環中無止境地運作的。

麻省理工為高性能計算機開發新的程式設計語言

舉個例子,用 Java 編寫的程式,可能會發生這種狀況。我們運作一個程式來得到一個單一的答案 —— 一個數字、或一個張量。

一個永不終止的程式,對我們說來毫無用處,但終止(terminate)是我們可使用 Coq 免費獲得的一項特性。

隻得一提的是,ATL 項目結合了 Ragan-Kelley 和 Chlipala 兩項研究的成果,前者長期持續關注着高性能計算背景下的算法優化。

與此同時,Chlipala 更關注算法優化的形式化(例如基于數學的驗證),但 ATL 是兩者都首次合作 —— Bernstein 和 Liu 與去年攜手,并産出了 ATL 這個成果。

麻省理工為高性能計算機開發新的程式設計語言

據悉,ATL 是首個、也是迄今唯一一個具有正式驗證優化的張量語言。目前 ATL 仍處于原型階段,但研究團隊已在許多小程式上展開了測試,可知其具有相當光明的前景。

展望未來,他們的主要目标之一是提升 ATL 的可擴充性,以便它能夠用于我們在現實世界中看到的更大型的程式。

此前這些程式的優化工作,通常需要人工來完成。除了總有臨時需要解決的問題、還總涉及反複實驗,因而難免發生大量的錯誤。

好消息是,借助 ATL,我們有望遵循一種更具原則的方法來重寫這些程式 —— 且這麼做更加容易,也更能保證程式的正确性。