淺談 程式語言研究 與 程式分析
前言
在上一篇文章《 ofollow,noindex" target="_blank">淺談國內高校程式語言教育 》(簡稱《淺教》)中,我提到了國外頂尖大學的程式語言課程大都是由從事 程式語言 (Programming Languages簡稱, PL )研究的專門人才來講授的。PL作為軟體的核心技術,在軟體開發效率、軟體可靠性、安全性、效能等方面都提供了根本性的支援。PL是一個已經活躍了50餘年的研究領域,作為軟體創新的核心動力,如今仍是一個極有生命力且非常活躍的學科。
如《淺教》所述,在排名領先的世界名校中,但凡有點規模的計算機院系,幾乎都會有PL方向的全職教授和研究人員,且越頂尖的大學,PL的研究越受重視。然而我國的情況並非如此,PL這樣歷史悠久且龐大複雜的學科在中國計算機學會並沒有相應的專委(Again,形式化方法專委和軟體工程專委無法取代程式語言專委,反之亦然),高校和科研院所也極少有專門註明PL為研究方向的教授和科研人員。因此,我想通過這篇文章向感興趣的知友們簡單介紹一下當前PL研究的整體概況和我所在的研究領域——PL方向下程式分析的研究現狀。
程式語言會議
判斷一個人的研究領域是否屬於PL,最簡單的方法就是看他文章發表的會議。
- A級會議
國際上程式語言有公認的四大頂會: PLDI 、 POPL 、 OOPSLA 、 ECOOP 。(有點像Security裡面的四大頂會Oakland、CCS、Usenix Security、NDSS)。
如果非要細分,PLDI和POPL要比OOPSLA和ECOOP好。這麼多年,我通過博士、博後導師們的灌輸+開會聊天瞭解到,歐洲人一般認為ECOOP稍好於OOPSLA(歐洲的PL研究人員特別多,很多知名程式語言的創始人也都來自歐洲如C++, C#, Python, Scala, PHP, ML, Haskell等),而北美人一般認為OOPSLA稍好於ECOOP。說ECOOP稍好的人一般持“OOPSLA由美國ACM主導,有錢有顏(資金和宣傳力),且ECOOP(由歐洲AITO主導)被斃掉的文章一般會流向OOPSLA(ECOOP和OOPSLA作為姊妹會議同一年創辦且deadline一前一後),所以OOPSLA有更多的submission和隨之而來更低的錄取率”。
我剛開始讀博士時不太懂,單純地認為錄取率低的會議好於錄取率高的,後來隨著在research上逐漸成熟慢慢了解到一個會議的好壞要看一個領域自己的人對它的認可情況,這個會議的program committee比它的排名、會議規模和錄取率更重要(後面也懂得頂會論文數量和citation並不能評價一個人的真正學術水平和影響,這個就不在此展開了)。打一個比方,超級女聲和青歌賽,前者報名人數眾多1000人(因為名氣大能出名,能吼兩句的都想試試)且錄取率很低(進100,10%),而後者報名人數很少200人(起碼都是稍微專業一些的)隨之錄取率也相對較高(進50,25%),但你不能因為說前者人數更多且競爭更激烈,就覺得進超女決賽的人比進青歌賽決賽的人唱歌更好吧。
近些年,OOPSLA和ECOOP為了擴大PL在應用方面的影響力,也鼓勵錄取一些偏軟體工程(SE)等方面的文章,個人認為在錄取的文章中,還是那些偏PL的文章的整體水平更高,因為PL人審PL類文章會更專業且更嚴格(當然凡事也都有例外,偏PL的文章也有差的而偏SE的文章也有好的)。
實際上還有一個非常好的PL會議,雖然不像ECOOP和OOPSLA那樣general,但其名聲和質量並不比它們差。這個會議就是 ICFP ,是functional programming領域的ECOOP和OOPSLA。
- B級會議
繼PLDI/POPL/OOPSLA/ECOOP後下一個檔次的PL會議是 ESOP (歐洲程式語言會議),這個是“純”PL的會議(搞純PL的人認為這個會議相當的好)。在我個人所在的研究領域program analysis(注:它是偏PL的基礎分析技術即傳統的靜態分析,例如pointer/points-to/alias analysis等,而並不是利用這些基礎分析技術開發的偏SE應用的software analysis)也有一些和ESOP一個檔次的“類”PL會議。
這個檔次的“類”PL會議包括靜態分析會議 SAS (VMCAI和SAS一個級別,但搞抽象解釋的朋友,他們很多都投VMCAI,告訴我他們認為SAS稍好於 VMCAI ),軟體工程會議 ISSTA (還有一個稍偏PL的SE會議是FSE,但FSE比ISSTA更好些,一般認為非同一級別),編譯會議 CGO (CGO和CC一個級別,但近幾年CGO要稍好於 CC ),再有就是更小眾的(在分析領域一般認為雖屬同一檔次但比前面的會議稍差那麼一點的)記憶體管理會議 ISMM ,還有偏嵌入式的 LCTES 和 EMSOFT 等。
- C級會議
再下一個檔次的“純”PL會議是 APLAS ,它被認為明顯好於同屬一個檔次的其他“類”PL會議,如 SOAP( 是個非常好的workshop有很多不錯的分析文章)、 SCAM 、 SAC 的 PL track (SAC的老牌高質track)等。
最後提一下PL的期刊 TOPLAS ,公認為PL最好的期刊,挺難投的(一年貌似就十幾篇),它的submission來源主要集中在PL的四大頂會(一般是把會議文章內容擴充套件30%左右)。
程式語言都研究些什麼
PL學科龐大,結構複雜,讓我這麼個搞PL分析的說清楚整個PL都在研究什麼是不可能的(估計這輩子都說不清楚)。但是簡介一下概貌還是可以的。我覺得按照如下三個方面對PL的研究進行分類是相對容易理解的。
- 純PL ,即關於PL本身的設計。例如,
- 語言設計和拓展 (language designs and extensions)
- 型別系統 (type systems)
- 語言語義和程式邏輯 (language semantics and program logics)
2. PL支援環境 ,即支撐PL的編譯和執行系統。例如,
- 編譯器技術 (optimization, transformation等)
- 執行時技術(virtual machine, garbage collection等)
3. PL應用 ,即利用PL的語法語義等知識對PL編寫的程式展開的一系列應用。例如,
- 程式分析(program analysis)
- 程式驗證(program verification)
- 程式合成(program synthesis)
上述分類只是一個框架,實際上並沒有展開,因為它很難展開,太龐雜了。例如,純PL中的第一條“語言設計和拓展”,就這一點就有各種程式設計正規化,比如,object-oriented, functional, logic, constraint, domain-specific, asynchronized programming等等。因此針對PL的研究內容我就止步於此,大家有一個大致瞭解就好。
下面我針對上述各PL分類方向的研究現狀做一個簡單的總結。
1. 純PL的研究相比於十年前已經安靜很多了,但是大家也不要低估研究純PL的這些人的數量,他們大多分佈在世界頂級大學和軟體公司,如今各種純PL技術仍活躍在各大PL舞臺,主要是POPL,ECOOP,ICFP和ESOP,PLDI和OOPSLA也有一些。我個人認為純PL圈子的人有如當年佔據計算機領域金字塔尖的那些搞演算法、邏輯、複雜性的研究者們,雖然如今力量日漸消退,但我依然認為他們是引領PL乃至軟體領域發展的一股中堅力量,值得尊敬。
2. PL支援環境實際上和編譯領域、系統領域甚至體系結構都有一些關係。由於上層程式語言本身就是各種型別,那麼支援它們的編譯和執行時技術更是種類繁多,層出不窮。就憑當今主流的那些程式語言,也可以讓這個方向的研究一直持續下去,畢竟使用它們的金主們(各大軟體公司)為了它們編寫的程式有更好的可靠性和效能也會給這股研究力量多多支援的。此外還有各種編譯和系統方面交叉人才的加持,我相信這個方向還會有很多實用的技術被創造出來。
3. PL應用舉的這三個例子,如今在PL的熱度是一年比一年高,主要原因是如今的軟體越來越複雜了,對於可靠性、安全性、效能和編寫效率都有新的要求,提出了新的挑戰,有很多實際且有趣的問題亟待解決,甚至這些技術的展開和探討對於程式語言的設計也會有很大的影響。如果你是一個research新人,對PL有點興趣但不知道研究什麼好,我建議你入PL應用的坑,因為我認為它至少在未來五年依然會是一個很活躍的研究方向(原因如上所述)。
接下來,我們來聊聊PL應用中最龐大、最火熱的分支之一,程式分析。
程式分析
- 程式分析的重要性
- 學術界
程式分析可以看成是一個交叉的研究方向,因為你會在PL以外的其它不同計算機領域的會議上看到程式分析的topic。例如,軟體工程如FSE, ICSE, ISSTA, ASE等;系統領域如 OSDI, SOSP, ASPLOS, EuroSys, ATC等;安全領域如Oakland, CCS, NDSS, Usenix Security等等。造成這種交叉性質的原因不難理解:程式分析是一種方法技術,目的是分析出程式在可靠性、安全性、效能等各種方面的表現和問題,而各領域的程式都是用程式語言寫的,且都或多或少地有上述方面的分析需求,因此不同領域對於程式分析的廣泛興趣便不足為奇。尤其是近些年,程式分析在上述很多會議的Call For Papers裡都會被單獨列為一項願意接收的topic,比較火熱。
- 企業界
程式分析不只在學術界佔有重要席位,近些年來也越來越受到企業界的青睞,原因我在之前簡單提到過,因為當今的軟體越來越複雜,在可靠性、安全性、效能等方面提出了新的要求和挑戰,這些都是傳統技術(如軟體測試等)很難駕馭的。據我所知,國際知名的大公司都有專門的程式分析研究或開發組,例如Microsoft,Google,Oracle,Apple,IBM,Facebook、Uber、華為等等。隨著人們逐漸意識到程式分析的重要性,專門研發程式分析技術的公司也越來越多,例如Coverity(被收購),GrammaTech,Semmle,SourceBrella(源傘)等。
如上所述,程式分析無論在學術界還是工業界都扮演著重要的角色。程式分析如此重要,它到底是個啥呢?接下來,我們來簡單看看什麼是程式分析。
2. 什麼是程式分析
程式分析雖有靜態動態之分,但從PL的角度我們一般關注的是 靜態分析 (static analysis)。簡單說來,靜態分析要回答的問題是
我想知道在任何輸入下,整個程式或程式的某一點是否能滿足某種條件或特性?
但是,程式的輸入可以無窮無盡,程式到達某一點的路徑可以根據輸入變化莫測、不勝列舉,如何將所有情況都考慮周全最後得出一個正確的(sound)結論呢?為此,我覺得靜態分析技術的核心可以圍繞兩個關鍵字展開:Abstraction和Over-approximation。
- Abstraction
程式在動態執行時,有各種不同型別的動態值,例如int型別的 1, -2, 350,String型別的 “a”, "007", "Hello" 還有各種referenced的concrete object(比如你在一個死迴圈裡放一句new A()你想想執行時會有無數個A型別的concrete object被生成直到吃滿你的記憶體),如果你想用有限的記憶體資源來分析這些無限的動態值,你首先需要把它們抽象起來,即Abstraction。例如只有一個int型別的抽象值(或一個整數int、一個負數int、一個0,共三個抽象值),一個型別的String值,一個new A()語句只生成一個抽象的物件,即(和上面concrete object對應的)abstract object。怎麼抽象是可以調節的,抽象方式不同,靜態分析的精度和速度便會不同。
- Over-approximation
程式在動態執行時,根據輸入的不同,可能會走各種不同的路徑,隨著程式規模和複雜度的增加,這些路徑也會無窮無盡,最終不能用有限的空間來列舉每條可能的動態路徑下的不同值(路徑爆炸),進而也無法知道程式的某一點的值是否還滿足某些條件。為了用有限的空間和時間來“列舉”無限路徑下的各種可能值,我們需要保守近似over-approximation。如下所示
if (e) x = 1 else x = 0 @Label A
假設我們想知道程式Label A這一點x的值是什麼?想象一下如果我們可以列舉路徑,我們可以得到很精確的答案,即在e == true時x = 1 (路徑1);在 e == false時x = 0 (路徑2)。然而如果程式很大且複雜,我們沒法列舉每一條路徑(路徑爆炸)下的值。over-approximation是在某些程式位置或區域保守地近似不同執行路徑(executions)下的值。如在Label A,我們可以說無論走哪條路,x要麼是1要麼是0。這是sound(safe)的結論,儘管不精確,但是如果x只要不是負數就可以做某種優化,那麼這樣的結論就是有用的。對不同路徑抽象的粒度是可以調節的,粒度不同(如context, flow, path-sensitivity),靜態分析的精度和速度也會不同。
實際上真正的靜態分析要複雜的多,因為它要針對不同程式語言不同語法下的不同語義來合理的抽象近似程式在每一個語句下的動態執行結果(可以想象成靜態地抽象一個直譯器)。因此靜態分析是和程式語言緊密相關的(需要深入準確地瞭解語言的語法和語義)。如此,我再說 程式分析(靜態分析)實際上是偏PL的研究方向 你就更容易理解了。
如今,軟體工程、系統和安全方向的很多程式分析都是利用基礎的靜態分析技術和結果,結合程式和問題的特點,進行更high-level的分析,比如查到更有趣的bug和安全漏洞,或更好的幫助優化或理解程式等等。既然基礎靜態分析和PL聯絡的這麼緊密且如此重要,我覺得有必要再深入地瞭解一下它。接下來,我要介紹基礎靜態分析中最核心、最重要的一個分支(之一),也是大家經常在各種程式分析論文和程式分析工具的程式碼、文件和註釋中看到的指標分析(pointer analysis),又名指向分析(points-to analysis)或別名分析(alias analysis)。
指標分析/指向分析/別名分析(Pointer/Points-To/Alias Analysis)
提到靜態分析,都應該聽說過指標分析,這個奇葩研究方向居然延續了近40年而且長盛不衰,至今仍活躍在各大PL相關會議當中。原因很簡單,它太重要了。
- 什麼是指標分析
指標分析並不是“分析指標”,如果不好理解,你可以用它的另一個名字“指向分析”來記,顧名思義,給定程式的任何變數或引用p,指向分析在compile-time(靜態)回答p都可能指向哪些值(實際上也是回答靜態分析的問題)。既然知道了p1和p2都指向什麼,如果p1和p2的指向有交集,就說p1和p2互相alias(alias對很多sound的分析是必須的),因此指向分析也叫別名分析即alisas analysis。
- 指標分析的重要性
為什麼指標分析如此重要?就像幾乎所有指標分析論文中描述的那樣,指標分析可以認為幾乎是所有靜態分析的基礎,因為它可以被用來構建全域性的程式控制流(Interprocedural control flow graph, ICFG)和方法呼叫圖(call graph),且所有全域性的程式靜態分析都需要這些基本結構,與指標分析提供的指向資訊和別名資訊來構建自己更high-level的靜態分析。
我上面提到的那些大的軟體公司尤其是IBM、Oracle等都有自己專門的指標分析的團隊(@TwoFrogs 的源傘公司也是研發指標分析的,國內首屈一指),很多程式分析的開源或商業框架也都是用指標分析搭建起來的。40年來各種PL相關會議上的指標分析論文層出不窮。近十多年來,指標分析的重點也逐漸從以前的C語言側重到面嚮物件語言(這個不難理解,畢竟如今的應用軟體的主流語言是面向物件),佔據了近些年來各大PL相關top會議指標分析topic的更多席位。
既然面向物件(OO)指標分析(主要是Java)在近些年相對更受關注,接下來我們就簡單聊聊它的發展程序,我覺得下面的梳理對想入坑或感興趣的同學會有所幫助。
- OO指標分析的過去和現在
OO的指標分析一般以Java為主,現在的很多Android的靜態分析技術和工具也都是基於Java指標分析的。接下來,我通過幾個關鍵人物和他們開發的關鍵技術或工具來幫助梳理Java指標分析的研究程序。故事從楓葉國說起:
加拿大麥吉爾大學的Laurie Hendren教授(早期指標分析領軍人物之一)的研究組在1999年以論文的形式發表了Soot,Soot直到今天仍是最流行的針對Java的靜態分析器。
在2003年,Laurie的學生Ondřej Lhoták在Soot上開發了指標分析Spark,影響力很大。Ondřej Lhoták從2003後繼續發力,一直在指標分析的topic發表文章,例如用BDD來實現指標分析,強調context-sensitivity對於Java的重要性等等。Ondřej 現在是加拿大滑鐵盧大學的副教授,可以說他是Java指標分析的最核心人物之一。
Laurie的另一個學生Eric Bodden(現德國Paderborn大學教授)從大概2012年接管了Soot,並在其上增加了IFDS的實現框架,在近些年開展了一系列針對Java的demand-driven指標分析的研究(注:Eric在分析程式安全性上有一些知名的工作,比如針對Android的taint analysis框架FlowDroid)。
在2009年之前,還有幾個人需要提及。
首先是Ana Milonova(現美國倫斯勒理工學院副教授)。Ana是Barbara G. Ryder(早期指標分析的領軍人物之一,現弗吉尼亞理工教授)的學生。Ana在2002年提出了object-sensitivity並驗證用它作為Java的context會帶來更好的分析精度甚至速度。這就打破了一直以來從C語言靜態分析那裡繼承而來的基於callsite的context-sensitivity的局面。這個工作在業內影響力很大,四大Java指標分析框架Doop,Wala,Soot,Chord都有object-sensitivity的實現,因為它是Java指標分析精度提升的必備技術。
其次是Mayur Naik(現賓夕法尼亞大學副教授)。Mayur是Alex Aiken(早期的指標/程式分析的重要人物之一,現斯坦福大學教授)的學生,他2006年發表了Chord,起初Chord是為了靜態檢測Java程式的data race寫的,而他檢測data race的核心技術就是依賴指標分析,因為Chord本身實現了不同種指標分析演算法,如今被認為是Java指標分析的四大框架之一。實際上,Mayur的Chord是基於John Whaley的BDDBDDB框架寫的 ,BDDBDDB是2004年發表於PLDI的指標分析工作。John是斯坦福大學Monica S. Lam教授(編譯龍書的作者之一,最新版龍書關於靜態分析那部分就是Monica寫的,她也是早期指標分析的重要人物之一)的學生,John和Monica在90年代末期也做了一系列指標分析工作。但是John最後自己創業,分析工作沒有延續。
再者是Manu Sridharan(現Uber靜態分析團隊的leader),他在加州伯克利讀博士期間,於2005和2006兩年連續發表了針對Java的demand-driven指標分析的工作,業內影響力較大,後續很多demand-driven指標分析工作都受此影響。Manu畢業後去了IBM T. J. Watson研究中心,參與了另一個知名Java指標分析框架Wala的開發,實際上之前IBM的研究人員已經開始了指標分析的研究和Wala的實現。
2009年後Java的指標分析主要有以下幾個國際團隊在做,
希臘雅典大學的Yannis Smaragdakis教授,
澳洲新南威爾士大學的Jingling Xue教授,
韓國高麗大學的Hakjoo Oh教授,
德國Paderborn大學的Eric Bodden教授,
香港科技大學的Charles Zhang教授,
澳洲悉尼大學的Bernhard Scholz教授和與其合作的Oracle Lab的程式分析團隊,
美國賓西法尼亞大學的Mayur Naik教授,
加拿大滑鐵盧大學的Ondřej Lhoták教授。
注:值得一提的是,以上除了Bodden和Naik教授的團隊,其餘幾個團隊也做過或正在做C/C++的指標分析。實際上在我們國內也有做過C/C++的指標分析團隊,那就是中科院計算所的馮曉兵教授和李煉研究員。關於C/C++的指標分析如果大家感興趣可以訪問以上幾個團隊的主頁,外加UCSB的Ben Hardekopf教授和印度理工的Uday Khedker教授。
2009年後,Java(或OO)指標分析領域的最核心人物當屬雅典大學的Yannis Smaragdakis教授,接下來我們簡單瞭解一下他的工作。
Yannis Smaragdakis教授原來是美國佐治亞理工和馬薩諸塞大學的教授,後來在2011年左右回到了希臘的雅典大學任教。他2009年在OOPSLA發表了當今最先進的Java指標分析器Doop,然後持續地在各PL頂級會議POPL,PLDI,OOPSLA,ECOOP發表大量的指標分析文章。我個人認為目前為止Yannis對指標分析最大的貢獻有兩個,一個就是Doop這個指標分析器本身,另一個是於2011年在POPL發表的一篇文章。這篇文章從新精確地解釋了Ana Milanova在2002年提出的object-sensitivity的定義,以消除從02年到11年期間關於object-sensitivity的有分歧的理解:即當context層數大於一層時應該用哪些object來做context。此外這篇文章又提出了一種新的context技術叫type-sensitivity(精度比object-sensitivity稍差但是速度快很多),這對於大程式分析不scalable的問題起到了很好的緩解作用。
2016年以後到今天,Java指標分析的關鍵人物是我們的一位知友Tian Tan@甜品專家 (新南威爾士大學Jingling Xue教授的博士,現在是丹麥Aarhus大學Anders Møller教授的博士後)。
Tian在2016發表於SAS的工作改變了20多年來context-sensitivity一直使用連續context元素的局面,巧妙地避開了對分析精度沒有用卻又影響分析速度的context元素。據我所知,上面提到的Ondřej Lhoták,Yannis Smaragdakis還有Mayur Naik教授在不同場合都對這項工作有很高的評價,此外,上面提到的Hakjoo Oh教授團隊在今年的OOPSLA,就是用機器學習的方法嘗試了Tian的這個工作。Tian從2017年開始又陸續在PLDI、OOPSLA和FSE等頂會發表了針對Java的一系列指標分析工作,感興趣的同學可以去他主頁看看。
關於Java的指標分析我就說這麼多,接下來簡單提及一下另一個OO語言JavaScript的指標分析研究團隊。值得注意的是,國際上有很多團隊做JavaScript的程式分析,但是做JS指標分析這種很基礎的並不多。主要有以下幾個團隊:
丹麥Aarhus大學的Anders Møller教授
韓國KAIST的Sukyoung Ryu教授
IBM Watson研究中心的Wala分析團隊
英國帝國理工學院的Benjamin Livshits教授
美國弗吉尼亞理工的Barbara G. Ryder教授(不活躍狀態)
美國加州聖芭芭拉大學的Ben Hardekopf教授(不活躍狀態)
在這裡我就不對JS的指標分析展開了(它主要的一些技術還是來源於Java的指標分析,但是JS的一些神煩的特性還是讓搞JS指標分析的人吃了不少苦),有興趣的同學可以訪問上述團隊的主頁。
總結
這篇文章從介紹PL會議入手,簡單描述了哪些人是從事PL研究的,他們都研究些什麼,這些研究的現狀怎樣。接著,介紹了PL研究的一個重要分支——(基礎)程式分析,包括什麼是程式分析(主要是靜態分析)以及為什麼程式分析在今天越來越重要。最後,介紹了程式分析中最核心、最重要的技術(之一)—— 指標分析,包括指標分析的概念、重要性以及它發展的過去和現在。希望這篇科普性的文章讓你對PL的研究和程式分析技術都能有所瞭解。
過去的50多年裡,針對PL的research從來沒有間斷過,也一直保持著生命力,它成就瞭如今軟體的琳琅滿目,也影響著未來軟體的生產力和創新力。作為資訊時代崛起的大國,不應該在如此重要的研究領域掉隊,衷心期待我國程式語言領域科研的進步。
後記
終於完成了這兩篇關於PL的文章,一篇問教育,一篇道科研。世界上有那麼多研究領域,多到你只要能看到這兩篇文章,你就已經和PL有著難得的緣分了。無論你是想做一名出色的程式設計師,還是想成為一名優秀的PL方向的researcher,你都為這份緣分續上了契約,我也和你一樣,一直走在履行約定的路上,雖然道阻且長,卻也一路風光(太 文 藝 了,對 不 住 了 )。那麼,同道中人,一起加油吧!
最後,感謝霧雨魔法店 和店裡熱愛PL的小夥伴們,非常感謝邀請我來寫文章 (((┏(; ̄▽ ̄)┛
祝大家國慶快樂!