同步數(shù)據(jù)流語言可信編譯器Vélus與L2C的比較*

康躍馨, 甘元科, 王生原

(清華大學 計算機科學與技術(shù)系,北京 100084)

應用于航空航天、高速鐵路、核電能源和醫(yī)療衛(wèi)生等領域的安全攸關(guān)系統(tǒng)[1]一旦失效,將給人類生命財產(chǎn)、社會生產(chǎn)、生活環(huán)境帶來巨大的破壞.如何為安全關(guān)鍵系統(tǒng)構(gòu)造一個基礎的安全軟件環(huán)境是需要面對的首要問題,尤其是對操作系統(tǒng)、編譯器等基礎軟件而言.

作為用來產(chǎn)生代碼的工具,編譯器的實現(xiàn)和維護自然經(jīng)過了“精雕玉琢”,因此編譯器的正確性問題容易被人們忽視.但了解實際情況的人都知道,編譯器的“誤編譯”問題是司空見慣、習以為常之事.對于許多領域來說,由于一般不會引發(fā)本質(zhì)的問題,又是小概率事件,人們也往往容易忽視誤編譯所帶來的負面影響.然而,對于安全關(guān)鍵系統(tǒng)而言,則必須考慮因編譯器引入的錯誤,否則,花大力氣在源程序級的驗證工作可能在目標程序級失效.實際上,如航空領域的RTCA DO-178B/C標準,編譯器屬于需要鑒定的工具類軟件,需要按照機載軟件的要求那樣對待.

要保障編譯器的正確性/可靠性,傳統(tǒng)上采用大量的測試以及嚴格的軟件過程管理來實現(xiàn),這并不能杜絕“誤編譯”現(xiàn)象.對編譯器進行正確性驗證,而不僅僅是測試,是解決問題的根本途徑.最嚴格的驗證手段莫過于采用形式化方法,近年來,有關(guān)編譯器形式化驗證的研究工作取得了長足的進步,達到了實用化水平,為未來新的工業(yè)標準的制定奠定了強有力的基礎.CompCert編譯器[2]是經(jīng)過形式化驗證的可信編譯器的杰出代表.該編譯器將C的一個重要子集Clight翻譯為PowerPC匯編代碼(后來也支持IA、ARM以及RISC-V后端),其編譯過程劃分為多個階段,每個階段的翻譯正確性都借助證明輔助工具 Coq[3]進行了證明,且這些證明可由獨立的證明檢查器檢查,這是迄今最強的形式化驗證手段,達到了人們所能期望的最高可信程度[4].Yang等人關(guān)于Csmith[5]的研究工作表明:CompCert在正確性方面的表現(xiàn)明顯優(yōu)于常用的開源或商用 C編譯器.因 CompCert編譯器的杰出成就,其代表性論文[6]的作者 Leroy獲得了 2016年度的 10年前最有影響 POPL論文獎(Most Influential POPL Paper Award).

C語言一直以來是安全關(guān)鍵領域中使用最為普遍的開發(fā)語言,人們下了很大功夫,使基于 C語言的系統(tǒng)開發(fā)更加安全、高效.然而,畢竟C語言程序?qū)哟屋^低,不易使人們聚焦于問題本身,開發(fā)效率受到很大影響,并且也難于驗證,于是基于模型/模型驅(qū)動的開發(fā)逐步興起并成為業(yè)界主流,由模型自動生成的代碼(C代碼為主)占比越來越高.比較著名的建模語言/工具,如Simulink[7]、Scade[8]等.

有一類建模語言稱為同步語言,特別適合于實時控制系統(tǒng)的開發(fā).所有同步語言均遵循同步假設,即每個周期內(nèi)的計算(從輸入值得到輸出值)都是瞬間完成的.另外,同步語言的語義被要求具有確定性.同步假設以及確定性可以極大地簡化實時系統(tǒng)的驗證.Esterel[9]、Argos[10]、Lustre[11,12]和Signal[13]是幾種有代表性的同步語言.其中,Esterel是命令式語言;Argos是基于并行和分層自動機的圖形化語言;Lustre和Signal是陳述式語言,具有數(shù)據(jù)流特征,常稱為同步數(shù)據(jù)流語言.Lustre是函數(shù)風格的語言,而Signal是關(guān)系型的語言.這些同步語言各自的特點有利于進行一些實質(zhì)性的靜態(tài)檢查甚至于形式化分析和驗證,從而有益于產(chǎn)生安全的代碼.在基于同步語言的開發(fā)工具中,最著名的是Scade,其代碼生成器KCG將一種基于Lustre的建模語言翻譯到C語言,KCG應該是獲得民用航空軟件生產(chǎn)許可(DO-178B/C)的第一個商用代碼生成器.目前,Scade工具已滲透到我國航空、航天、軌道交通及核電等若干安全關(guān)鍵領域.

與 C語言編譯器的情形類似,人們同樣不會止步于像 Scade這樣的安全級代碼生成器.基于高級建模語言代碼生成器的形式化驗證近年來已受到極大關(guān)注.本文主要分析與比較兩個關(guān)于同步數(shù)據(jù)流語言 Lustre的可信編譯器項目,二者均采用如CompCert那樣的方法對翻譯過程本身進行驗證.這兩個項目是目前僅有的從事形式化驗證的Lustre可信編譯器研發(fā)的長線項目,一個是法國Pouzet教授的項目組,另一個是作者所在的L2C項目組.前者較早的工作[14]將具有Lustre語言關(guān)鍵特征的Lustre子集翻譯至一種基于對象的中間語言,最近的工作是將這一中間語言翻譯至Clight(見CompCert項目),并與CompCert銜接后稱為Vélus編譯器[15].L2C項目致力于基于Lustre的語言到C語言的可信代碼生成器(或稱L2C編譯器)的研發(fā),從一開始便以Clight作為目標語言,從而與 CompCert實現(xiàn)對接.有關(guān)這兩個可信編譯器項目的進一步發(fā)展情況會在正文中詳細介紹.為方便起見,文中分別以Vélus和L2C代稱這兩個項目以及相應的編譯器.

編譯器形式化驗證的另外一種重要方案是翻譯確認(translation validation),由Pnueli等人于1998年首先提出[16].翻譯確認不是直接驗證翻譯程序,而是對翻譯前后代碼前的語義等價關(guān)系進行確認.比起直接對翻譯過程進行驗證,這種方法具有較好的可重用性.然而,它必須是一個自動化的過程,因而從理論上決定了它可能出現(xiàn)誤報(false alarm).值得指出的是,Pnueli等人首次提出翻譯確認方法時,是以Signal作為示范例子,即編譯器源語言是同步數(shù)據(jù)流語言Signal,目標語言是C.翻譯確認的話題與本文主題關(guān)系不大,因此不再進一步展開討論.

本文第1節(jié)首先介紹Vélus和L2C的基本情況.第2節(jié)～第6節(jié)分別就源語言特性、編譯器結(jié)構(gòu)、核心翻譯步驟、同步數(shù)據(jù)流語義與翻譯正確性驗證、實現(xiàn)與性能等多個角度對Vélus和L2C進行較為深入的分析與比較.最后,第7節(jié)是全文總結(jié).

1 基本情況

同步的概念[17]早在20世紀80年代初就開始被關(guān)注.到20世紀80年代后期出現(xiàn)了包括Lustre[12]的幾個最著名的同步語言,其他,如 Esterel[9]和 Signal[13]等.Lustre語言最初是由 Caspi和 Halbwachs等人提出來的[18],然后在工業(yè)領域需求的基礎上發(fā)展起來[19].先是在Merlin-Gerin公司開發(fā)了基于Lustre的Saga工具,用于核電保護系統(tǒng)開發(fā).接著,Verilog公司接手了 Saga商品化的工作.同時期,Aerospatiale公司(現(xiàn)隸屬于空客)為空客 320機載軟件開發(fā)設計了Sao工具,其思想也類似于Saga.后來,在Saga和Sao的基礎上,Aerospatiale、Merlin-Gerin以及Verilog聯(lián)手啟動了新工具(Scade)的開發(fā)計劃.當時,Verimag實驗室建立了Verilog公司和Lustre項目組合作的一個共同實驗室,專攻Scade的設計,并由Lustre項目組的Pilaud領導Scade團隊.再后來,Scade又吸收了其他公司的一些技術(shù),并經(jīng)多次轉(zhuǎn)賣,目前全球聞名.

Lustre語言被應用于商用工具后得到更多的重視,Verimag的Lustre團隊也一直在維護和更新版本,目前的最新版本是Lustre V6[20].

Pouzet教授課題組很早開始從事同步語言相關(guān)的研究工作,曾與Caspi等人合作在數(shù)據(jù)流語言Lucid[21]基礎上加入同步特征,設計實現(xiàn)了同步數(shù)據(jù)流語言Lucid Synchrone[22],實際上也可以看作是Lustre的函數(shù)式語言(ML)的擴展[23].

大致在2006年前后,Pouzet與Paulin共同啟動了形式化驗證Lustre語言編譯器的一個長線項目[24].最早的參與者有Bertails和Biernacki.在TYPES 2007會議上,Bertails[25]報告了該項目的目標以及最初始的一些工作(類型檢查、時鐘演算以及因果性分析等問題).Biernacki等人在 2008年發(fā)表的論文[14]中刻畫了一個更加清晰的藍圖并給出一些實質(zhì)性進展,為該項目奠定了基調(diào).后來,Auger完成了其博士論文工作[26,27],該項目取得進一步的成果.從這些工作可知,該課題組這一時期實現(xiàn)的形式化驗證編譯器,源語言為包含Lustre語言關(guān)鍵特征的小型同步數(shù)據(jù)流語言,目標語言是一種基于對象的中間語言.最近幾年,Bourke等人基于Biernacki和Auger等人的工作,實現(xiàn)了從上述中間語言到CompCert的前端中間語言Clight的翻譯與驗證,從而得到一個核心Lustre子集的可信編譯器Vélus[15].

本文作者所在課題組的L2C項目,源于國內(nèi)核電領域的實際需求,于2010年9月正式啟動.L2C可信編譯器的預研工作于2013年6月完成驗收[28],源語言為一個單時鐘的核心Lustre子集.L2C可信編譯器的一個完整企業(yè)版于2015年4月完成驗收[29],源語言為一個面向領域的類Lustre同步數(shù)據(jù)流語言.L2C項目開展后,合作企業(yè)的建模與代碼生成工具從原 Scade的用戶走向自主研發(fā)之路,目前已被實際應用.最近幾年,L2C項目組主要在做開源L2C可信編譯器的工作[30-32].

后續(xù)各節(jié)中,會涉及到有關(guān)Vélus編譯器和L2C編譯器的更多細節(jié).

2 源語言特性

本節(jié)在討論Vélus和L2C的源語言特性時,會涉及到原始論文中的Lustre語言、Lustre V6以及Scade源語言的特性.

Caspi和 Halbwachs等人在其早期論文[11,12]中給出了 Lustre語言最基本的特性.Lustre程序由若干節(jié)點(node)組成,執(zhí)行時會明確一個主節(jié)點.每個節(jié)點相當于普通語言中的子程序.不同于普通語言,Lustre語言的所有數(shù)據(jù)對象(變量、常量以及表達式)的取值都是流(stream).每個流都有各自的時鐘(clock);每個節(jié)點有一個基本時鐘,是該節(jié)點中所有數(shù)據(jù)對象的時鐘里面最快的一個.程序的執(zhí)行是無限循環(huán)的過程,每次循環(huán)均在一個時鐘周期(cycle)內(nèi)完成,每次執(zhí)行都針對不同的輸入和輸出.對于每個時鐘周期,一個流或者有值,或者沒有值,前者是當前時鐘周期包含在這個流的時鐘的激活(activation)周期,而后者是當前時鐘周期不屬于激活周期的情形.時鐘相同的流之間可以進行運算,相當于這些流在該時鐘的每個激活周期里的取值都進行相應的運算.節(jié)點可以被調(diào)用,可以看作特殊的運算.節(jié)點調(diào)用相比傳統(tǒng)語言(如C語言)的函數(shù)調(diào)用,允許有多個返回值.每個節(jié)點中包含一組等式,每個等式的執(zhí)行效果類似于賦值.

Lustre語言中有幾個與時鐘和流相關(guān)的特殊運算(或算子).when和current均為一元運算,它們產(chǎn)生新的流,其時鐘會不同于原來的流;when會使時鐘變慢,而current會使時鐘變快,二者為互補的運算.pre為一元運算,所產(chǎn)生的流會比原來的流延遲一個激活時鐘周期.二元運算 arrow(→),所產(chǎn)生的流第 1個激活周期的值取自第 1個流,其余激活周期的值取自第2個流;特別是,通常會與pre運算配合使用,為新流置第 1個激活周期的值.fby為二元運算,所產(chǎn)生的流第1個激活周期的值取自第1個流,其余激活周期的值取自第2個流進行pre運算之后的流,其效果相當于前面提到的arrow(→)與pre運算的配合使用.為敘述方便,下面將pre、arrow以及fby之類的算子稱為時態(tài)(temporal)算子,而將when和current之類的算子稱為時鐘(clock)算子.

為方便起見,我們稱上述原始論文中的 Lustre語言為經(jīng)典 Lustre語言.為便于實際應用,Lustre V6以及Scade在經(jīng)典Lustre語言核心特性的基礎上增加了更為豐富的語言特性,在下面討論Vélus和L2C時會涉及到其中一些.

Vélus編譯器目前未開源,其源語言的信息主要依據(jù)其里程碑論文[14,15,27]以及該項目最新論文[15]的作者Bourke提供給我們的Vélus編譯器部分源程序測例.

從實現(xiàn)角度看,無論是Lustre V6和Scade,還是本文討論的Vélus和L2C,對于經(jīng)典Lustre語言核心特性的實現(xiàn)基本上是遵循原始論文中所定義的語義.有一個值得注意的例外,即關(guān)于節(jié)點的調(diào)用.在Caspi和Halbwachs等人的論文中以及之后相當一段時間內(nèi)的學術(shù)探討中,Lustre語言編譯器在翻譯時都是將節(jié)點調(diào)用進行宏展開(有必要時會進行一系列換名),形成實際上只含一個節(jié)點的中間語言.這在實際應用中顯然是不合適的,因此在Lustre V6、Scade、Vélus以及 L2C中,節(jié)點調(diào)用的實現(xiàn)均與傳統(tǒng)語言類似.對此,在 Vélus中,將其稱為模塊化(modular)實現(xiàn)[14,15,27].

從傳統(tǒng)語言特性方面看,Vélus與Lustre V6基本類似,而L2C和Scade除了這些特性外,還增加了一些面向?qū)嶋H應用的特性,主要包括case表達式以及更多的數(shù)組和結(jié)構(gòu)體運算.

在時態(tài)算子方面,Vélus目前僅支持經(jīng)典Lustre語言中的fby算子,而L2C、Lustre V6以及Scade均支持經(jīng)典Lustre語言中的全部時態(tài)算子(pre、arrow和fby).在Bourke提供的Vélus測例程序中,對原始例子中出現(xiàn)pre和arrow之處均用fby及條件(if)表達式進行了等價替換,參見PLDI 2017論文[15].另外,L2C與Scade還增加了一個三元fby算子.二元fby算子可通俗理解為:結(jié)果流是將原來的流(第2個參數(shù))延后一個激活周期,且第1個激活周期取第1個參數(shù)的流在該周期的值.三元fby算子是一種擴展:結(jié)果流是將原來的流(第3個參數(shù))延后n個激活周期,且前n個激活周期均取第1個參數(shù)的流在第1個激活周期的值,這里,n為第2個參數(shù).

在時鐘算子方面,Lustre V6是最全面的,包含when、current和merge算子.merge算子是作用于互補的慢速流,將它們歸并后得到一個快速的流.Vélus與Scade均不支持current算子,認為merge完全可以替代current的作用.雖然Vélus與Scade同樣都是支持when和merge算子,但二者有一個本質(zhì)的差異:Scade既有布爾型的時鐘,又有枚舉型的時鐘.布爾型時鐘是通過布爾量的true或者false進行二選一取樣(或確定是否激活周期),而枚舉型時鐘則可以通過枚舉量進行多選一取樣.Scade和Lustre V6都同時支持布爾型時鐘和枚舉型時鐘,Vélus與L2C目前都只支持布爾型時鐘.與Vélus不同的是,L2C除支持when和merge算子外,也支持current算子.L2C規(guī)劃中擬支持枚舉型時鐘,但目前尚未實現(xiàn).

對于一般運算,各操作數(shù)的時鐘要求是相同的.但對于節(jié)點調(diào)用的運算,在一些語言中各個參數(shù)的時鐘可以是不同的,L2C、Lustre V6以及Scade都是這樣,但Vélus目前要求所有參數(shù)的時鐘是相同的.

在高階迭代算子方面,L2C的兩個主要版本有不同的支持.對于面向核電領域的企業(yè)版L2C,支持Scade的9個高階迭代算子[29];對于開源版的L2C,則支持Lustre V6的全部5個高階算子[31].這二者之間,有3個算子的含義是等價的.目前,Vélus未支持高階迭代算子.

表1是有關(guān)Vélus和L2C的源語言特性對照的一個簡單小結(jié).

Table 1 Source language features (L2C vs. Vélus)表1 源語言特性(L2C vs. Vélus)

3 編譯器結(jié)構(gòu)

Vélus編譯器的架構(gòu)如圖1所示,該圖與Bourke等人在PLDI 2017論文[15]中的編譯架構(gòu)圖(該文的圖1)相對應,包括所有中間語言和翻譯過程所用的名稱.Vélus編譯器繼承了 Pouzet課題組的前期工作[14,27],下面的介紹并未刻意區(qū)分這些集成進來的部分,欲了解詳情可參考文獻[15].

圖2刻畫了最新的L2C編譯器架構(gòu),是目前的開源版L2C[31]所采用的架構(gòu).以前的L2C版本(主要有原型版與企業(yè)版)的架構(gòu)與此有所不同,不在本文討論范圍之內(nèi),這里不再贅述.

兩個編譯器的前期處理工作很相似.圖1中Vélus將源程序(Source)翻譯至中間表示SN-Lustre的過程,對應于L2C將源程序(Lustre*)翻譯至中間表示LustrS的過程.

二者的 Parsing過程如同常規(guī)的編譯器,實現(xiàn)詞法和語法分析,并生成抽象語法樹(AST).經(jīng)過 Parsing過程,Vélus將源程序變換至AST,圖1中標為Unannotated Lustre.同樣,L2C經(jīng)過Parsing過程也將源程序變換至AST,之后附加了一個LustreWGen過程,最后生成LustreW中間表示.LustreWGen最核心的任務是完成全局和部分局部常量表達式求值(含常量定義的依賴性檢查和排序),以方便后續(xù)技術(shù)環(huán)節(jié)高效地處理需要單個常量的情形,如三元 fby運算中的延后激活周期數(shù)(正整數(shù)常量值)、高階迭代運算的迭代次數(shù)常量、數(shù)組定義或訪問區(qū)間有關(guān)的常量,等等.Vélus目前不支持這些特性,故此類需求不足.LustreWGen還有一些個別很細節(jié)的任務,比如根據(jù)調(diào)用關(guān)系自動設定主節(jié)點.主節(jié)點不一定非要自動設定,也可以在執(zhí)行時手動設定,對于此類細節(jié),在Vélus的相關(guān)論文中并未提及,因此在本文后續(xù)內(nèi)容中,對于此類細節(jié)也并未作為關(guān)注重點.

隨后,是類型和時鐘檢查及其標注過程,Vélus和L2C所完成的工作是一致的:對程序(AST)進行常規(guī)類型檢查以及時鐘檢查.若檢查不通過,則報錯;檢查通過后,進行類型和時鐘標注,類型檢查與傳統(tǒng)語言相同,時鐘檢查二者遵循相同的時鐘演算規(guī)則.如圖1所示,Vélus稱這一過程為Elaboration,標注后的中間語言稱為Lustre.同樣的工作在L2C中是由LustreVGen過程完成的.除了類型和時鐘檢查及其標注過程之外,LustreVGen還包括一些后續(xù)階段所需要的準備工作,參見隨后的介紹.

完成類型和時鐘檢查及其標注之后,Vélus進行Normalization變換,其最核心的工作是使每個fby表達式和節(jié)點調(diào)用實例從上層表達式分解出來,確保它們只出現(xiàn)在專用等式的右端,而不是嵌在其他表達式中.這與Lustre官方編譯器以及 Scade工具的做法是一致的,主要是進行一些使代碼規(guī)范化以及新生成某些結(jié)構(gòu)信息,為后續(xù)階段做好鋪墊:對于fby等時態(tài)算子,要準備好如何對fby等時態(tài)算子在有關(guān)歷史數(shù)據(jù)的訪問方面得到妥當處理;以及針對節(jié)點的每一個調(diào)用實例要如何做好輸入流和輸出流相關(guān)的處理.首先是不同輸入流和輸出流的時鐘有可能不同(Vélus目前不支持這種情形),其次是輸出流可能有多個(比較,C函數(shù)僅有一個返回參數(shù)).

在L2C框架中,與Vélus的Normalization相對應的工作體現(xiàn)在LustreVGen和LustreSGen過程中,如圖 2所示.LustreVGen首先進行如前所述的工作(類型和時鐘檢查及其標注),之后是生成fby和pre等時態(tài)運算所需要的特殊標識符和類型;以及生成類型比較函數(shù)的函數(shù)名;結(jié)果得到LustreV中間表示.使每個fby表達式和節(jié)點調(diào)用實例從上層表達式分解出來的工作在LustreSGen過程完成.除此之外,LustreSGen還實現(xiàn)以下功能:將含有表達式列表的平行等式分解為多個不含表達式列表的等式集合,將arrow(→)和pre算子的組合轉(zhuǎn)換成二元fby算子,以及將高階迭代算子處理成類似for循環(huán)的結(jié)構(gòu)(為后續(xù)階段的高階算子消去,即生成for循環(huán)作準備)等.

在LustreVGen和LustreSGen過程中有許多方面對于當前的Vélus來說是不需要的.另外,在對于包含條件的表達式處理上,Vélus和L2C略有不同.經(jīng)Normalization變換后,Vélus將所有if和merge表達式置為頂層,而L2C是在排序(見后文)之后才處理if、case和merge等算子.

接下來,Vélus和L2C均對上述變換之后的中間代碼以等式為粒度進行排序.這些等式之間具有數(shù)據(jù)流并發(fā)關(guān)系,排序之后等式之間具有先后順序關(guān)系,等式的語義與命令式語言的賦值語句相類似.排序的結(jié)果應不違背數(shù)據(jù)依賴關(guān)系,即滿足先寫(或先有值)后讀的原則.Vélus和 L2C的排序過程分別稱為 Scheduling和 Toposort,如圖1和圖2所示.

后續(xù)翻譯過程中,Vélus從SN-Lustre到Obc的過程,以及L2C從LustreS到LustreC的過程,集中了多數(shù)核心同步數(shù)據(jù)流語言特征的翻譯.同樣,Vélus從Obc到Clight以及L2C從LustreC到Clight的變換將同步數(shù)據(jù)流語言的可信編譯與可信編譯器CompCert銜接起來,對二者來說都是整個編譯器最后的重要環(huán)節(jié).對于這些核心翻譯步驟,我們將在下一節(jié)加以專門討論.

在當前的開源版L2C中,已發(fā)布了從LustreS到LustreC全部翻譯過程(包含了所有的核心翻譯階段)的正確性驗證代碼;LustreWGen、LustreVGen和LustreSGen等非核心過程的驗證工作多數(shù)也已完成,將會在后續(xù)版本中陸續(xù)發(fā)布(試對比,CompCert的前端一些非核心翻譯過程如語法分析、類型檢查等的驗證工作也是在新近的版本中才陸續(xù)發(fā)布).因Vélus至今尚未開源,其核心翻譯步驟的驗證工作可以從相關(guān)論文中有所了解,但非核心翻譯過程驗證的工作在論文中很少提到具體的實現(xiàn)情況.有關(guān)二者核心翻譯階段的驗證工作,在第 5節(jié)有進一步的討論.

相比Vélus,L2C之所以有更多的翻譯階段,主要有如下原因:(1) L2C立項時是面向?qū)嶋H的領域需求,所以支持較多和較為復雜的語言特性,而 Vélus相關(guān)的工作主要面向?qū)W術(shù)研究,二者在源語言特性方面的對照參見表1;(2) 實用語言的編譯器開發(fā)需要不斷維護,多階段的翻譯有利于可重用性及可擴展性,如 CompCert面向可實用的 C語言,其編譯器結(jié)構(gòu)中包含了許多翻譯階段;(3) 安全攸關(guān)領域一般都有可追溯的要求,多階段的翻譯有利于提高可追溯性.

4 核心翻譯步驟

從 Lustre語言翻譯到 C,由同步數(shù)據(jù)流范型變換為串行命令式范型,必須實現(xiàn)幾個核心同步數(shù)據(jù)流語言特征的翻譯,Vélus和L2C的翻譯階段均包含了對這些核心特征的處理,主要包括:(1) 通過以等式為粒度的排序或調(diào)度,完成數(shù)據(jù)流并發(fā)特征的消去,實現(xiàn)等式集合的串行化;(2) 實現(xiàn)同步數(shù)據(jù)流語言時鐘算子特征的消去;(3) 實現(xiàn)同步數(shù)據(jù)流語言時態(tài)算子特征的消去;(4) 結(jié)合前述這些特征的處理,實現(xiàn)同步數(shù)據(jù)流范型向串行命令式范型的轉(zhuǎn)換.

在上述幾個核心同步數(shù)據(jù)流語言特征的翻譯步驟中,以等式為粒度的排序或調(diào)度容易解釋,在前面一節(jié)已經(jīng)介紹過(Vélus中對應Scheduling,L2C中對應Toposort),剩余的3個方面在本節(jié)進行討論.對于經(jīng)歷這幾個消去同步數(shù)據(jù)流特征的翻譯步驟之后所得到的中間代碼,Vélus和 L2C最終將其翻譯至 Clight代碼,從而實現(xiàn)與CompCert的對接.翻譯至Clight代碼的步驟也是本節(jié)要討論的重點內(nèi)容之一.

L2C支持高階迭代算子,高階算子的消去也是L2C的核心翻譯步驟之一.這項工作主要是在LustreRGen過程(如圖2所示)中實現(xiàn)的,它將高階運算翻譯為等價的for循環(huán)語句.由于Vélus未支持高階迭代算子,所以我們不對這一核心翻譯步驟作進一步討論.順便,對于其他L2C支持而Vélus不支持的非核心語言特征,其處理過程也同樣不作討論,比如,將復雜類型比較運算翻譯為比較函數(shù)的過程(圖2中的TransTypecmp).

值得注意的是,在上述核心翻譯步驟中,除了排序(調(diào)度)和生成到Clight,對于其余幾個方面,Vélus均集中在從SN-Lustre到Obc兩個層次的變換,而L2C則是分散在LustreS到LustreC的多個層次的變換中.

(a) 時鐘算子的消去

我們僅討論Vélus和L2C均支持的時鐘算子when和merge(此外,L2C還支持current算子).

Vélus和L2C遵循相同的時鐘演算規(guī)則,在僅限于布爾型時鐘的情況下,嵌套時鐘可由時鐘變量(或其否定)的序列來表示(可參見Biernacki等人在2008年發(fā)表的論文[14]):baseonb1onb2… onbn.其中,base為當前節(jié)點的基準時鐘,每個bi或者是某個時鐘變量(布爾型)x或者是其否定notx.

圖3給出Vélus和L2C均可以接受的一個源程序例子.我們來觀察節(jié)點tracker的代碼.假設該節(jié)點的基本時鐘為base.根據(jù)時鐘演算規(guī)則,變量c的時鐘為baseonx(與counter調(diào)用中的兩個參數(shù)的時鐘相同),而表達式(ptwhen notx)的時鐘為baseon notx;x,t,pt等變量的時鐘均為base.表達式mergexc(ptwhen notx)的作用是將時鐘分別為baseonx和baseon notx的兩個表達式c和(ptwhen notx)歸并為一個時鐘為base的表達式.這里,需要注意的是,when算子會使時鐘變慢,而merge算子會使時鐘變快.

在得到各變量以及表達式的時鐘后,when算子實際上就可以消去了.翻譯的結(jié)果就是將等式(左邊的變量和右邊的表達式具有相同的時鐘)的執(zhí)行加上時鐘為真的條件,生成if條件語句.這一條件的構(gòu)成是將時鐘表達式中所有的時鐘變量(或者其否定)進行合取,而基本時鐘base可認為是true.例如,若時鐘為baseon notx,則條件即為notx.

對于merge算子,則會翻譯為if-else條件語句或case語句.例如,圖3中的mergexc(ptwhen notx),Vélus會翻譯為類似于if (x) {c=…} else {pt=…}之類的語句.在L2C中也類似,不同的是,L2C的設計要支持枚舉型時鐘,所以目前選擇了一種更為一般的情況,會將merge表達式翻譯至case語句.具體細節(jié)可分別對應于附錄中圖4所示右半邊的if語句和圖5所示右半邊的case語句.

順便,Vélus在生成Obc表示后會針對這些if語句進行Fusion Optimization的優(yōu)化處理(如圖1所示),使條件相容(多為時鐘相同)的分支語句序列進行合并,這樣僅需一次條件判斷即可.目前,L2C尚未開展此類優(yōu)化工作.這個問題,后面還會提到.

(b) 時態(tài)算子的消去

Vélus經(jīng)過Normalization變換,或者L2C經(jīng)過LustreVGen和LustreSGen過程,已確保了每個fby表達式只出現(xiàn)在專用等式的右端,而沒有嵌在其他表達式中.圖3中的所有fby表達式均已滿足這一要求,對應的等式為:節(jié)點counter中的f=true fby false和c=1 fbyn,節(jié)點rising中的ps=true fbys,以及節(jié)點tracker中的pt=0 fbyt.我們以tracker中的pt= 0 fbyt為例解釋fby算子的消去.

每個fby對應一個時態(tài)變量,用于記錄歷史狀態(tài).對于圖3中節(jié)點tracker的含fby等式pt=0 fbyt,這一變量為pt.無論是Vélus還是L2C,都會將pt包裝為節(jié)點tracker內(nèi)可訪問的特殊變量.下一小節(jié)會看到,Vélus會將pt看作節(jié)點tracker所對應的類的屬性變量,每個tracker實例都會維護一份pt的存儲,可以保存以前周期的信息,而其他普通變量(比如t)只能看作節(jié)點tracker所對應的類的方法的內(nèi)部變量.類似地,L2C會將pt看作與每個tracker的實例相關(guān)聯(lián)的某個全局結(jié)構(gòu)體的域變量,而其他普通變量(比如t)不在這個全局結(jié)構(gòu)體的域中.

若從對應到Vélus翻譯后的Clight代碼角度來看,圖4所示的結(jié)構(gòu)體類型tracker包含了域變量pt,對應于上述節(jié)點tracker所對應的類的屬性變量pt.若從對應到L2C翻譯后的Clight代碼角度來看,圖5所示的結(jié)構(gòu)體類型outC_tracker包含的域變量acg_fby4,對應于上述節(jié)點tracker所對應的類的屬性變量pt.這種時態(tài)變量在L2C中是自動產(chǎn)生的新變量,比如對于圖 3所示的程序,將會產(chǎn)生acg_fby1、acg_fby2、acg_fby3和acg_fby4,分別對應于該程序中的4個fby的時態(tài)變量f、c、ps和pt.

對于每個tracker實例中pt=0 fbyt的執(zhí)行過程,Vélus和L2C的處理是類似的.在該實例執(zhí)行的第1個激活周期開始時,會將相應于這一實例的時態(tài)變量pt的值置為0,而在之后的每個激活周期開始時會將pt的值置為前一個激活周期結(jié)束時pt的值.在每個激活周期的結(jié)束階段,會將在該周期中已經(jīng)計算好的t的值存入pt的存儲空間,存入之后在該周期不會再有對pt的讀取.

若從對應到翻譯后的Clight代碼角度來看,圖4中省略了reset相關(guān)的部分,而從圖5右半邊上部的if語句來看,我們會發(fā)現(xiàn):第1個激活周期(acg_init為1時)開始時,pt會被置為0,而在之后的每個激活周期開始時會將pt的值置為相應時態(tài)變量acg_fby4在前一個激活周期結(jié)束時的值.關(guān)于每個激活周期結(jié)束時對時態(tài)變量的修改,圖 4中是由最后一句(?self).pt=(?out).t來完成的,而在圖 5中是由倒數(shù)第 2句(*outC).acg_fby4=(*outC).t來完成的.

另外,L2C還支持三元的fby算子,其實現(xiàn)更加復雜一些.L2C的實現(xiàn)方案是將自動產(chǎn)生的新增時態(tài)變量(類似上述的acg_fby4)擴展為數(shù)組,其大小即為三元fby比起前面討論的二元fby多出來的常量參數(shù)值.因Vélus目前不支持三元fby算子,所以我們不在這里討論相應的翻譯細節(jié).

除了二元和三元fby算子,L2C還支持傳統(tǒng)Lustre的時態(tài)算子pre.雖然Vélus目前未涵蓋pre算子,但其實現(xiàn)與fby雷同.

(c) 同步數(shù)據(jù)流范型轉(zhuǎn)換為串行命令式范型

在處理好前述幾個核心同步數(shù)據(jù)流語言特征翻譯的基礎上,再解決好流數(shù)據(jù)對象的表示及其周期性處理的環(huán)節(jié),基本上就實現(xiàn)了同步數(shù)據(jù)流范型向串行命令式范型的轉(zhuǎn)換.在 Vélus中,這種范型轉(zhuǎn)換體現(xiàn)在生成 Obc中間表示.相應地,在L2C中,這種轉(zhuǎn)換導致了LustreC中間表示的產(chǎn)生.

Vélus的Obc是一種基于對象的中間表示,用于封裝從同步數(shù)據(jù)流代碼到命令式代碼的翻譯結(jié)果.在翻譯到Obc時,每一個節(jié)點會對應到一個類.這個類中包含的屬性有兩類:一類是該節(jié)點中的所有時態(tài)變量(每個fby對應一個這樣的變量);另一類是該節(jié)點中調(diào)用其他節(jié)點的實例(注:不允許調(diào)用到本節(jié)點的實例).這兩類屬性都是有狀態(tài)的,即要維護其以前周期的歷史信息(注:節(jié)點實例內(nèi)部也可能有自己的時態(tài)變量).該類中包含的方法有兩個:一個是reset,用于初始化時態(tài)變量屬性以及調(diào)用實例,僅在第1個激活周期執(zhí)行;另一個是step,用來執(zhí)行該節(jié)點內(nèi)部的所有等式,每個激活周期都會被重復調(diào)用.每個節(jié)點的輸入輸出參數(shù)以及局部變量均在 step方法中得以體現(xiàn).

與 Vélus不同,L2C從同步數(shù)據(jù)流代碼到命令式代碼的翻譯結(jié)果(LustreC中間表示),并未將每個節(jié)點對應的方法及reset方法與它們要處理的狀態(tài)數(shù)據(jù)(時態(tài)變量和調(diào)用實例)封裝在一起,而是采用了類似于C程序的組織方式.每個節(jié)點對應 C的一個函數(shù),它的每個實例(對應于程序中實際調(diào)用該節(jié)點的位置)對應于一個結(jié)構(gòu)體,其中封裝了對應的時態(tài)變量和要調(diào)用的其他節(jié)點實例.為方便每個周期的循環(huán)調(diào)用,每個節(jié)點的輸入輸出參數(shù)變量也會被封裝在一個該節(jié)點專用的結(jié)構(gòu)體中,對于主節(jié)點要封裝所有輸入和輸出變量,而對于其他節(jié)點僅封裝輸出.因為有可能有多個輸出,所以對應到C時用一個結(jié)構(gòu)體類型的變量存放多個返回值,所以,所有節(jié)點的輸出變量均被分裝在結(jié)構(gòu)體中.主節(jié)點的輸入變量要作為外部輸入,為方便起見,也被封裝在結(jié)構(gòu)體中.同時,每個節(jié)點均有一個對應的reset函數(shù).由此可見,雖然沒有對每個節(jié)點對應的函數(shù)和reset函數(shù)以及它們要處理的數(shù)據(jù)對象進行封裝,但這些內(nèi)容均包含在生成的LustreC代碼中,如同C語言的代碼結(jié)構(gòu).

從翻譯后的Clight代碼可以看到一些具體的細節(jié),如圖4和圖5所示.

(d) 翻譯至Clight

綜合前面幾個核心同步數(shù)據(jù)流語言特征的翻譯步驟,應該能夠看明白從圖 3所示的 Lustre源程序分別經(jīng)Vélus和L2C翻譯至圖4和圖5所示的Clight代碼(二者雖然形式上不同,但體現(xiàn)的行為是相通的),從而也可以了解最后階段的這一核心翻譯步驟所起到的作用.

在這個階段,Vélus就是將Obc中間代碼的語法設法與翻譯后的Clight代碼的語法對應起來.L2C也類似,通過CtempGen完成從LustreC到Ctemp的翻譯,又通過ClightGen將Ctemp中的memcpy語義翻譯為內(nèi)存拷貝函數(shù),最終翻譯至Clight代碼.L2C后面這一步驟(從Ctemp到Clight)在Vélus目前的版本中沒有對應的需求.這些翻譯步驟的圖示可分別如圖1和圖2所示.

5 同步數(shù)據(jù)流語義與翻譯正確性驗證

這部分內(nèi)容的準確論述需采用形式化或半形式化方式,但受限于篇幅,本文僅就其要點進行非形式描述.

(a) 同步數(shù)據(jù)流語義

在從Lustre到C的轉(zhuǎn)換過程中,經(jīng)歷了同步數(shù)據(jù)流語義逐步向串行命令式語義的過渡.在現(xiàn)階段,Vélus的動態(tài)語義的形式化定義是從SN-Lustre中間表示開始的,在Obc,中間表示被變換至一種基于對象的串行命令式語義;相應地,L2C的動態(tài)語義形式化定義是從LustreS中間表示開始的,在LustreC,中間表示徹底變換為一種類C的串行命令式語義.這些中間層語言所處位置,如圖1和圖2所示.

可以看出,Vélus的同步數(shù)據(jù)流語義消去僅在一個階段完成,而L2C則經(jīng)歷了多個階段逐步消去.由于L2C的源語言特征相比Vélus要復雜很多,實踐過程決定了跨多層的語義過渡是必然的選擇.

Vélus在定義 SN-Lustre語義時已完成排序(scheduling),因此無需考慮同步數(shù)據(jù)流語言的數(shù)據(jù)流并發(fā)特性.L2C是在LustreS層進行排序(toposort),在LustreS層有串行語義定義(節(jié)點內(nèi)部的所有等式相互之間存在全序關(guān)系),同時也定義有超粗粒度的并發(fā)語義(以等式為粒度,等式操作是不可分割的原子操作,等式之間存在由數(shù)據(jù)依賴所確定的偏序關(guān)系).

Vélus和L2C的同步數(shù)據(jù)流語義都選擇了基于操作語義來定義(雖然也存在看似很不錯的基于指稱語義的基礎工作[33]).在Lustre語言的原始論文[11]中,作者給出了Lustre語言的基本操作語義規(guī)則.Vélus和L2C的操作語義定義首先要與學界公認的這些工作相符,同時也應考慮實現(xiàn)的因素(交互式定理證明的方便性).比如,采用Coinductive來定義流看似是非常自然的(因為要處理的是 infinite對象),然而無論是Vélus還是L2C均放棄選擇這種方法,L2C團隊當初遇到的問題主要是因為采用Coq實現(xiàn)整體任務需求的技術(shù)難度無法預測.

在Vélus和L2C的同步數(shù)據(jù)流語義中,對于流數(shù)據(jù)對象的基本理解是一致的,均將其看作是從自然數(shù)到取值論域的函數(shù).比如,可以將一個流s在第n個周期的值記為s(n).然而,在具體實現(xiàn)上,L2C采取了一些不同的措施.特別是針對同步數(shù)據(jù)流語義中最具代表性的fby算子.

在定義fby算子的語義時,Vélus使用了一個輔助算子hold,會將所處理的流數(shù)據(jù)對象在上一個激活周期的取值保持到其后續(xù)的無效周期,這樣,若當前周期是激活周期,則fby運算的結(jié)果就相當于當前周期hold運算的結(jié)果.這一思想在 L2C項目開展的初期用來實現(xiàn)一種時鐘歸一化(clock unifying)算法[34],其中定義了類似于hold的算子,并用來刻畫fby算子的語義.然而,在后來的工作中,L2C擯棄了這種做法.主要原因是,這種方法僅適合于定義二元fby算子,而難以推廣到實際應用中很有用的三元fby算子.L2C對二元和三元fby算子的語義定義采用了一致的框架,定義一個大小為n的循環(huán)緩沖區(qū),并設法限定僅在激活周期可訪問緩沖區(qū),這里,n即為三元fby算子的第3個參數(shù)(對于二元fby算子,n=1).

定義同步數(shù)據(jù)流語義的另一個重要方面,就是語義環(huán)境中要保留子環(huán)境的狀態(tài),這些子環(huán)境對應于當前環(huán)境下調(diào)用其他節(jié)點而形成的實例環(huán)境.保存這些子環(huán)境的原因是因為存在時態(tài)變量(見第4.2節(jié)),需要保存歷史狀態(tài),這就導致了在調(diào)用的節(jié)點實例返回時不能像傳統(tǒng)的函數(shù)調(diào)用那樣釋放掉變量的存儲空間.因而,我們必須要定義并維護一個樹狀的語義環(huán)境,這對語義定義以及相應的證明來說,難度增加了許多,但這是我們必須要應對的.L2C在定義語義時對是否是時態(tài)變量進行了區(qū)分,以方便對應到Clight的語義環(huán)境中.Vélus在文獻[15]中對這種樹狀語義環(huán)境也有許多描述,但僅從論文無法了解其進一步的實現(xiàn)詳情.

另外,L2C因支持高階迭代算子以及更多的數(shù)組和結(jié)構(gòu)體算子,使語義定義的難度增大許多,但相關(guān)細節(jié)不屬本文所要討論的范圍.L2C的多階段翻譯架構(gòu)(如圖 2所示)正是為了適應各種各樣的語義復雜度以及與Clight語義之間的巨大差異,同樣,圖2所示的許多翻譯步驟也不在本文所討論的議題之內(nèi).

(b) 翻譯正確性驗證

在形式化定義動態(tài)語義階段,Vélus和L2C的各階段翻譯正確性的驗證目標與CompCert所建議的階段翻譯正確性目標從形式上是一致的,都是要證明一種從高層到低層單向的語義模擬等價關(guān)系.這種模擬等價關(guān)系之所以可以是單向的,是由于每一層語言均具有確定的語義(deterministic semantics).

對于同步數(shù)據(jù)流語義來說,這種單向的語義模擬等價關(guān)系可大致描述為:任意數(shù)據(jù)流程序G的每個節(jié)點f,若可以將輸入流xs映射到輸出流ys,則對于翻譯后得到的程序G′中與f對應的節(jié)點或函數(shù)f′以及這一層次中相應于G′的初始化函數(shù)reset,如果G′在其第1個激活周期先執(zhí)行reset后執(zhí)行f′,而在其他后續(xù)激活周期中都重復執(zhí)行f′,那么同樣可以將xs映射到輸出流ys.注意:這一命題中的G、f、xs和ys都是任意的.

雖然各階段要證明的單向語義模擬等價關(guān)系形式上看都是相似的,但具體到不同階段,其含義卻都有所不同.首先,各個階段的語法和語義互不相同;其次,每個階段可能有或沒有語法層面的reset函數(shù),如果有的話,不同階段的reset函數(shù)也可能有所不同;以及還有其他各種不同,這里不再贅述.

一般來說,從 Lustre源程序到 Clight程序的各階段翻譯過程中,同步數(shù)據(jù)流語言的語法及語義特征逐漸被消去,C語言語法及語義特征逐漸增加.在定義上述單向語義模擬等價關(guān)系時,所消失的語義特征描述通常會由新增加的語法特征來彌補.比如前面提到的 reset特征,在較高的語言層次,語法層面并沒有對應的函數(shù),所以是在語義定義中體現(xiàn)其行為,而在靠后的語言層次(比如圖2所示的LustreE2層)已有語法層面的reset函數(shù),就不會也不可能通過語義定義來體現(xiàn)reset行為.

因Vélus和L2C的編譯框架之間差異較大(如圖1和圖2所示),可以想象到二者在翻譯正確性驗證方面存在較大的差異.這種差異體現(xiàn)在各個方面.這里僅列舉一例.如果考慮第4.1節(jié)～第4.3節(jié)提到的核心翻譯步驟,在Vélus中僅由Translation一個階段完成(如圖1所示),而在L2C中則是分散到從LustreR1到LustreD的許多階段實現(xiàn)的(如圖2所示).一般來說,一個翻譯階段所負責的工作越多,其正確性證明的難度也越大,重用性也越差.然而,另一方面,翻譯階段也不能太多,否則會導致語言層次增加太多,反而加重維護的負擔.因此,應根據(jù)源語言的規(guī)模合理設計翻譯階段的數(shù)量.

Vélus中SN-Lustre之前的階段未定義動態(tài)語義,這些階段所保持的特性主要是靜態(tài)方面的.多數(shù)這些階段,甚至從 SN-Lustre到 Obc的過程(Translation),基本上是繼承前人(Bertails、Biernacki和 Auger等人)的工作.Bourke等人的論文[15]對這些靜態(tài)語義相關(guān)階段的介紹很少,同時,Vélus未開源,所以具體繼承情況的詳情未能很好地得到了解,從Biernacki和Auger等人的論文[14,27]僅可了解到其中的一些.

Vélus的語法分析器是Bourke等人重新寫的,它基于Jourdan等人提出的對LR(1)自動機進行確認并對確認程序進行驗證的方法[35],因此可以認為是一個經(jīng)過形式化驗證的語法分析器.L2C中,最近剛完成與此平行的工作[32],并以編譯選項的方式集成到了開源L2C編譯器[31]中.

對于 Vélus中的類型、時鐘檢查(elaboration)以及接下來的規(guī)范化過程(normalization),僅了解 Bertails、Biernacki和 Auger等人在 Coq中實現(xiàn)了這些過程以及進行了驗證,但他們的論文中未提到是如何進行驗證的.L2C中與此對應的過程(LustreWGen、LustreVGen和 LustreSGen)的驗證在目前的開源版本中尚未發(fā)布,相關(guān)工作仍在完善和整理之中.這些翻譯過程在Vélus和L2C編譯框架中所處位置,如圖1和圖2所示,下同.

Vélus對于排序過程(Scheduling)的驗證是基于翻譯確認的方法[16],具體實現(xiàn)在相關(guān)論文[14,15,27]中未加介紹.L2C中的排序過程(Toposort)是經(jīng)過嚴格形式化驗證的,證明了經(jīng)過排序后的LustreS程序的串行語義行為,與排序前LustreS程序的等式粒度并發(fā)語義所刻畫的行為是兼容的.從實現(xiàn)角度來看,對排序過程的形式化驗證要比翻譯確認的工作量大很多,所以從通常的觀點來看,是否有必要這樣做是值得商榷的.但 L2C的這項工作,對于在項目開展初期積累團隊成員在使用Coq進行編程和驗證的經(jīng)驗以及檢查LustreS操作語義定義的合理性等方面起著重要的作用.

6 實現(xiàn)與性能

Vélus和L2C的開發(fā)環(huán)境與CompCert[2,36]一致,有驗證需求的部分均在Coq[3,37]工具之中實現(xiàn),并自動抽取得到相關(guān)的 Ocaml代碼.詞法分析器的 Ocaml代碼由 Ocamllex自動產(chǎn)生.語法分析器使用了 Ocamlyacc,或者Menhir[38],前者針對未經(jīng)驗證的語法分析器選項,后者針對經(jīng)過形式化驗證的語法分析器選項.驅(qū)動程序以及其他輔助工具(如各層的語法樹或代碼的格式輸出程序)通過手工編寫Ocaml代碼實現(xiàn).

由于Lustre沒有標準測試集,在Bourke等人的論文[15]中從前人相關(guān)工作中選取了14個有代表性的程序進行性能測試,在開源OTAWA框架[39]下,對Vélus以及其他一些Lustre編譯器(Lustre V6和Heptagon與CompCert或者GCC的組合)的最壞執(zhí)行時間(worst-case execution time,簡稱WCET)指標進行了測試評估.CompCert的版本是2.6,GCC的版本是4.8.4,目標體系結(jié)構(gòu)是armv7-a(含硬件浮點單元vfpv3-d16).

我們從Bourke那里獲得了文獻[15]中使用的全部14個測例程序源碼,并在與上述測試環(huán)境基本相同的配置下(配置選項為-march=armv7-a-mfloat-abi=softfp-mfpu=vfpv3-d16),針對L2C完成了測例程序的評估測試.我們將得到的測試結(jié)果匯總于表2.

表2中的第1列是14個測例程序的名稱,第2列是L2C和CompCert 2.6組合編譯器的測試結(jié)果(WCET值),第3列是從文獻[15]中摘錄的Vélus測試結(jié)果,第4列是L2C和GCC4.8.4(加-O1優(yōu)化選項)組合編譯器的測試結(jié)果,最后一列是Lustre V6和GCC4.8.4(加-O1優(yōu)化選項)組合編譯器的測試結(jié)果.

Table 2 WCET estimates in cycles for an armv7-a/vfpv3-d16 target表2 周期為單位的WCET評估值(目標處理器:armv7-a/vfpv3-d16)

從表2的結(jié)果粗略來看,L2C+CompCert的性能比Vélus低50%左右.L2C性能不如Vélus的原因,目前能想到的主要是因為Vélus在Obc中間表示進行了if語句的Fusion Optimization優(yōu)化(如圖1所示),而目前L2C未作任何優(yōu)化,CompCert目前也沒有支持有關(guān)的優(yōu)化.

附件A.1和A.2分別給出了測例程序tracker(源碼如圖3所示)經(jīng)Vélus和L2C編譯生成的Clight代碼,如圖4和圖5所示.從圖5可以看出,L2C生成的代碼中包含了大量可融合的if語句.從圖4可以看出,Vélus生成的代碼中時鐘相同的操作已被合并到相同的條件分支下.

表2的第4列給出了L2C和GCC4.8.4(加-O1優(yōu)化選項)組合編譯器的測試結(jié)果.從中可以看出,測例程序tracker的WCET值比起第2列有顯著降低(由1 035降至580),其他測例程序的情況也是如此,性能也優(yōu)于Vélus的測試結(jié)果(見第3列).在GCC的“-O1”優(yōu)化選項中,包含了針對if語句的“-fif-conversion”優(yōu)化,可以縮短if-then語句所花費的時間.

Lustre V6編譯器設計時也未過多考慮相關(guān)優(yōu)化,主要是寄望于C編譯器會負責這些優(yōu)化工作(L2C也曾有類似的考慮,但更主要的是在開發(fā)L2C企業(yè)版時,用戶方出于可追溯性的硬性要求,原則上不允許對代碼進行編譯優(yōu)化,這種理念一直延續(xù)至今,但不一定適合各種場合).從文獻[15]的測試結(jié)果(如該文中圖12第6列所示)看,Lustre V6和CompCert組合的編譯器對于各測例程序的WCET性能指標均不如L2C和CompCert組合的編譯器.目前,我們對Lustre V6和CompCert組合編譯器的性能測試工作也在進行之中.

7 總 結(jié)

Vélus和 L2C都是基于輔助定理證明器(Coq)構(gòu)造 Lustre可信編譯器的長線項目,它們都是先將源語言翻譯至Clight,并與CompCert編譯器實現(xiàn)銜接.Vélus和L2C課題組在立項目標、發(fā)展過程和方向、源語言需求以及工作基礎等方面都不同,因而導致Vélus和L2C編譯器在許多方面有明顯的差異,形成了各自的特色.

本文從基本情況、源語言特性、編譯器結(jié)構(gòu)、核心翻譯步驟、同步數(shù)據(jù)流語義與翻譯正確性驗證以及實現(xiàn)與性能等多個角度對Vélus和L2C進行了較為深入的分析與比較.當然,也不排除漏掉一些比較重要的方面,今后會通過其他機會加以補充.

據(jù)Bourke介紹,Vélus項目組近期在開展將有限自動機融入 Vélus的研究工作.Scade[8]工具中包含對有限自動機的支持,其目的是增加控制流特性.L2C項目組目前尚無計劃開展類似的工作.

附錄

A.1

例:Vélus生成的Clight代碼.如圖4所示.

A.2

例:L2C生成的Clight代碼.如圖5所示.