摘要

同步數據流語言(如Lustre,Signal)近年來在航空、高鐵、核電等安全關鍵領域得到了廣泛應用，因此與這類語言相關的開發工具本身的安全性問題受到高度關注.同步數據流語言到串行命令式語言的代碼生成工具是此類工具的典型代表(如Scade)。構造代碼生成工具的途徑可分為兩大類：一類是傳統的方法，例如通過大量測試和嚴格的過程管理等手段來實現；另一類是通過形式化方法，例如直接對編譯器本身進行形式化證明，采用翻譯確認的方法等。近年來，形式化方法作為構造和驗證代碼生成工具的關鍵途徑而得到廣泛的重視，有望最大限度地解決“誤編譯”問題，因而成為新的研究熱點。文章在介紹代碼生成工具的形式化構造和驗證方法的基礎上，特別聚焦于同步數據流語言代碼生成工具的相關研究工作，對其現狀進行綜述和分析。

1引言

計算機技術日益廣泛地應用于航空航天、高速鐵路、核電能源和醫療衛生等領域的安全關鍵系統（Safety-CriticalSys-tem,SCS）中。SCS一旦失效，將給人類的生命財產、社會生產和生活環境帶來巨大的破壞。在現代計算機技術的發展中，相比軟件來說，硬件方面的安全性保障技術更加成熟，人為因素導致硬件故障的概率相對較小。雖然人們一直關注于軟件安全性問題，并積累了大量研究成果和實踐經驗，但軟件方面的安全保障目前仍舊是計算機系統安全性中的薄弱環節。如何為安全關鍵系統構造一個基礎的安全軟件環境是需要解決的首要問題，尤其是對操作系統、編譯器等基礎軟件。本文將針對安全可信的編譯器進行介紹。 所謂安全可信的編譯器，就是要保證編譯器做正確的事情，保證它能將符合源語言規范的程序正確翻譯到目標語言程序。這里，“正確翻譯”主要指功能方面，通常情況下是指源語言到目標語言的語義保持關系（通常被刻畫為一種反向的行為模擬等價關系）不能實現“正確翻譯”的編譯器，則一定存在某種程度的“誤編譯”錯誤。 作為用于產生代碼的工具，編譯器的實現和維護自然經過了“精雕玉琢”，同時又“隨時隨地”經受著無數應用程序的“考驗”，因此編譯器的正確性問題容易被人們忽視。但了解實際情況的人都知道，編譯器的“誤編譯”問題是司空見慣、習以為常之事。在許多領域中，由于“誤編譯”一般不會引發本質的問題，又是小概率事件，因此人們往往也忽視了“誤編譯”所帶來的影響。然而，對于安全攸關系統而言，則必須考慮編譯器引入的錯誤，否則在源程序級的高成本驗證工作可能在目標程序級失效。實際上，在航空領域的RTCADO-178B/C類標準中，編譯器屬于需要鑒定的工具類軟件,需要按照機載軟件的要求同等對待。 圖1（摘自X。Leroy在POPL^2011的特邀報告⑵）描述了安全關鍵的嵌入式控制領域中典型的應用程序開發流程：從高級算法描述語言或建模語言所描述的安全級應用程序生成行為等價的C代碼，后者接著被翻譯成可執行的目標代碼。圖1中，Simulink是面向建模語言MatLab的著名工具；Scade是基于同步數據流語言Lustre的建模與開發工具。如圖1所示，在對安全關鍵系統進行驗證和確認（V&V）時，不能不考慮編譯器可能引入的錯誤。另外，更值得關注的是：若代碼生成器或編譯器不可信，針對（高級算法描述語言或建模語言）源程序（模型）進行的有關安全性方面的各種努力（模型檢查、正確性證明、靜態分析及模擬仿真等）則會付之東流。因此，除了要保障應用程序本身的安全性之外，還需要有安全可信的編譯器（或代碼生成器）。

圖1編譯器（代碼生成器）帶來安全隱患的流程

本文將在介紹代碼生成工具的形式化構造和驗證方法的基礎上，特別聚焦于同步數據流語言代碼生成工具的相關研究工作及其發展現狀。同步數據流語言（如Lustre,Signal）近年來在安全關鍵領域得到了廣泛應用，比如Scade工具將一種擴展的Lustre語言翻譯成C語言。在實際應用中，通常會將諸如同步數據流語言之類的高級算法描述語言翻譯成常規的串行命令式語言（通常為C語言），如圖1的上半部分。同步數據流語言與串行命令式語言之間有很大的語義差距，正如X。Leroy所言，構造這樣的代碼生成工具（或可信代碼生成器）是一項很有價值且富有挑戰性的工作。 本文第2節先對同步數據流語言進行簡要介紹；第3節分析并討論當前實現代碼生成工具的主要途徑；第4節側重對同步數據流語言到串行命令式語言（通常為C語言）代碼生成工具的典型工作和發展情況進行綜述；最后有針對性地進行小結。

2同步數據流語言

傳統的常規語言，如C語言，一直以來都是安全關鍵領域中使用最為普遍的開發語言。人們為安全有效地使用C語言下了很大功夫，積累了非常豐富的經驗。盡管人們通過各種辦法來使得基于C語言的系統開發更加安全高效，但畢竟C語言程序層次較低，不易使人們聚焦于問題本身，開發效率受到很大影響，并且也難于驗證。因此，基于模型/模型驅動的開發逐步興起并成為業界主流，由模型自動生成的代碼（C代碼為主）已占據主導地位，比較著名的建模語言/工具有Simulink和Scade等。 有一類建模語言被稱為同步語言，特別適合于實時控制系統的開發。所有同步語言均遵循同步假設（synchronyhypothesis），即每個周期內的計算（從輸入值得到輸出值）都是瞬間完成的；同步語言的語義被要求具有確定性。同步假設以及確定性可以極大地簡化實時系統的驗證。另外，同步語言通常有嚴格且可靠的數學定義，對于同步范型有友好的工程設計方法，因此它在實時嵌入式應用的建模、規范描述、驗證以及實現等各個層面都已成為重要的技術選項。20世紀80年代，人們就開始了同步范型的理論研究工作隨即又出現了許多基于同步假設的語言，并且這些語言都得到了廣泛的應用。Esteel,Lustre和Signal是最著名的幾種有代表性的同步語言。其中，Esterel是命令式語言；Lustre和Signal是陳述式語言，具有數據流特征，常被稱為同步數據流語言。Lustre是函數風格的語言，而Sig-nal是關系型的語言。除Esterel,Lustre和Signal外，學術界和工業界還有其他具有同步特征的語言：LucidSynchrone是對早期數據流語言Lucid的同步化，并采納了Lustre的許多語言特征；Quartz是一種基于Esterel的面向響應式系統的規范、驗證以及實現的同步語言；Argos是State-chats（一種著名的響應式系統的形式化圖形語言）的同步化；Synccharts是一種具有Statecharts風格和Esterel語義的圖形語言；Grafcet是一種基于有同步特征的Petri網的建模/仿真工具。 這些同步語言各自的特點有利于進行一些實質性的靜態檢查，甚至形式化分析和驗證，從而有益于產生安全的代碼。在基于同步語言的開發工具中，最著名的是Scade,其代碼生成器KCG將一種基于Lustre的建模語言翻譯成C語言。KCG應該是獲得民用航空軟件生產許可（DO-178B/C）的第一個商用代碼生成器。目前，Scade工具已滲透到我國航空航天、軌道交通及核電等安全關鍵領域。 雖然同步語言的發展已經相當成熟，并在安全關鍵的嵌入式實時系統中極具影響力，但一直以來，人們對安全關鍵系統的可信性要求日益提高，期待在各個環節上都達到最高程度的安全可信。同步語言實現工具（各階段的編譯器、代碼生成器）本身的安全性，近年來已引起了學術界和工業界的極大關注和興趣。 本文主要關注同步數據流語言的代碼生成工具，Lustre,Signal以及LucidSynchrone是此類語言的典型代表。上面提到的其余同步語言與本文話題關系不大，僅簡單提及。此外，LucidSynchrone項目所積累的有關編譯器驗證的基礎研究，均由同一課題組人員轉化為對Lustre編譯器的驗證工作。事實上，關于同步數據流語言編譯器的驗證工作，從目前學術界和工業界的進展來看，僅需關注與Lustre和Signal相關的工作即可。 同步數據流語言具有時鐘同步、并發、流數據對象等特征。例如,Lustre語言中，所有的數據都是流（stream），對應于無窮多個邏輯時鐘周期，每個周期有一個取值。所有的運算都作用于流。每個邏輯時鐘周期都執行同樣的計算（即相同的代碼），并假設在邏輯時鐘周期內計算一定可以完成，即滿足所謂的同步假設。各個周期內的計算由多個計算節點（node）組成，每個計算節點內部是一個等式的集合，每個等式都定義流上的運算，等式之間并發執行，是數據驅動的計算過程。時態運算和時鐘運算是Lustre語言（以及其他同步數據流語言）中具有特色的流運算。基本的時態運算包括pre,fby和arow（f）等，其中pre和fby可用于訪問歷史信息；基本的時鐘運算包括when,current和merge等算子，可用于改變時鐘的快慢。

3代碼生成工具的構造途徑

如何才能保證編譯器的安全和可信？對于編譯器來說，安全和可信的具體指標就是其正確性，要保證從源程序到目標程序的翻譯過程正確，即保證源語言的行為特征能夠在目標語言中被正確地體現，杜絕“誤編譯”。目前保證可信性的方法主要有兩類：1）非形式化的方法（或傳統的方法），如采用測試和過程管理;2）采用形式化的方法，主要包括直接對編譯器本身進行驗證和翻譯確認，以及混合使用這些方法。

3.1 通過測試和過程管理實現編譯器的可信性

為了保證編譯器實現的正確性，普遍的做法是采用大量的測試用例對編譯器進行測試。例如，GCC的torture測試集包含幾千個C源程序用例，商用的PlumHallStandardValidationSuiteforC有幾萬個用例,LustreV6的開源軟件包中含幾百個源程序用例，等等。還有一些Bug-hunting工具，例如Csmith，它可以產生更多或更獨特的源程序用例，從而擴大覆蓋范圍，發現更多的編譯器缺陷。 盡管如此，采用測試的手段仍是不完善的，如果測試用例的覆蓋范圍不夠廣泛，則可能會遺漏編譯器中的錯誤。即便是通過測試發現了錯誤并且做了修改，也無法保證編譯器自身的正確性。實際上，僅編譯器自動測試工具Csmith（截至2011年2月）以及EMI/SPE（截至2017年10月）就發現了GCC和LLVM的近1700個編譯錯誤。 Scade工具的代碼生成器KCG經過了嚴格的V&V過程，符合民航電子系統的國際標準DO-178B/C，并且在空客公司的多款客機如A340和A380中成功應用。然而，DO-178B/C主要是以過程質量控制為主的標準，不足以說明Scade的編譯器不存在“誤編譯”。KCG并沒有通過形式化的方法加以嚴格驗證，雖然DO-178C中包含了一些非強制的形式化相關條款，但經調研，業界的用戶仍會不時發現ScadeKCG的某些翻譯漏洞。

3.2 通過對翻譯過程本身進行形式化驗證實現代碼生成工具

為增加編譯器的安全和可信程度，僅通過測試和嚴格的過程管理都是不夠的。對編譯器進行正確性驗證，是解決問題的根本途徑。最嚴格的驗證手段莫過于采用形式化方法。工業界也早已意識到形式化軟件開發的潛力，在一些安全攸關領域的安全級軟件開發標準中也逐步新增了與形式化方法相關的目標或者相應的補充說明。CC（CommonCriteria）安全評估標準［6］中將可信性分為7個級別（EAL1到EAL7），可信性級別越高，其采用形式化規范和驗證的程度就越高。航空無線電委員會（RTCA）近期也已推出民航電子系統的國際標準DO-178C,其在DO-178B的基礎上增加了對形式化規范和驗證的要求，如DO-178C和DO-333等補充說明。 近年來，有關編譯器形式化驗證的研究工作取得了長足的進步，達到了實用化水平，為未來制定新的工業標準奠定了強有力的基礎。CompCert28］編譯器是經過形式化驗證的代碼生成工具的杰出代表。該編譯器將C的一個重要子集Clight翻譯為PowerPC匯編代碼（后來也支持IA32和ARM后端，目前已擴展至可支持64位處理器以及開源的RISCV體系結構），其編譯過程劃分為多個階段，前端解析過程之后每個階段的翻譯正確性都借助輔助工具Coq進行了證明，且這些證明可由獨立的證明檢查器檢查。這是迄今最強的形式化驗證手段，達到了人們所能期望的最高可信程度客］。由于其目標是對主體翻譯過程本身進行驗證（如圖2所示），因此稱此類代碼生成工具為經過驗證的編譯器。Yang等關于Csmith的研究工作表明：CompCert在正確性方面的表現明顯優于常用的開源或商用C編譯器。因CompCert編譯器具有的杰出成就,其代表性論文的作者Leroy獲得了2016年度的“十年前最有影響POPL論文獎”（MostInfluentialPOPLPaperAward）。

圖2 經過驗證的編譯器(以CompCert為例)

3.3 通過翻譯確認技術實現代碼生成工具

盡管對編譯器的翻譯過程本身進行形式化驗證是一種比較完美的保證可信性的辦法，但是其難度高，工作量大，并且無法擴展（一旦編譯器需要修改，那么證明就需要重做）。于是，Pnueli等最早提出了翻譯確認的方案［1］。翻譯確認的方法不是直接驗證翻譯程序，而是用統一的語義框架為翻譯過程的源和目標代碼建模，兩個模型之間定義一種特定的語義等價關系/模擬等價關系，設計一種可自動證明二者等價性的確認程序（返回成功與否，成功時或給出證明腳本，不成功時或給出反例）。根據不同的語義模型，確認程序可以通過自動求解或證明、符號計算、模型檢查、靜態分析等方式來實現模型間的等價性確認。 如圖3所示的翻譯確認過程中，在發現前后中間表示的語義不等價時，會使編譯器停下來。若非主體翻譯階段，比如某類中間代碼的優化，則可以不必讓編譯器停下來，不做這一優化即可，如圖4所示。

圖4翻譯確認（針對某個中間表示上的優化）

早期,Necula和Lee提出了PCC（proofcarryingcode）機制，并帶動了關于確認式編譯器（certifyingcompiler）的研究。可以認為Pnueli的翻譯確認是比PCC更通用的機制。PCC機制主要被用來對編譯結果進行安全性檢查，而不是對編譯器進行驗證。 對于翻譯確認來說，如果翻譯前后的語義保持性的確認過程比較容易構造，或者說源語言與目標語言的語義模擬等價性關系比較容易定義，則證明也會相對容易，那么驗證該等價關系是一個不錯的選擇。因為該方法最大的優點就是可以不放棄現有的編譯框架，其可擴展性較好。一些大型編譯器也有類似的工作。但是當源語言與目標語言差異較大（類似于將同步數據流語言翻譯成串行語言）時，兩種語言的語義等價性關系是很難定義的，其證明過程也會更加困難。 相比較而言，當源語言和目標語言的語義定義達到認可的程度時，對翻譯過程進行驗證是一種徹底的做法，原理上可以保證源程序的一般性質都可以保持到目標程序上。而翻譯確認的做法往往只是關注部分性質的保持性（當然，也可以逐步逼近一般性質），因而有可能會存在“虛假預警”（falsealarms）。因此，直接驗證翻譯過程與翻譯確認兩種方案各有利弊。目前看來，針對一個完整的編譯過程，根據各個翻譯的特點，將這兩種方案混合使用是一種十分有益的做法。比如，一些針對優化算法的翻譯確認工作可以很好地融合到CompCert編譯器中。

4 同步數據流語言的代碼生成工具

同步數據流語言是應用較為廣泛的建模語言，比如著名工具Scade所使用的建模語言是在同步數據流語言Lustre基礎上定義的。如圖1所示，像Scade和Simulink這樣的建模工具，往往是先將建模語言變換到領域語言（許多安全關鍵領域均采用傳統C語言），然后從C這樣的領域語言編譯到目標語言。 對于C語言的可信編譯研究近年來已經取得了不錯的進展，如前面所提到的Leroy等開發的C編譯器Comp-Cert，其原理圖參見圖2。 近年來，針對圖1中所示的從高級建模語言到C語言之間的可信編譯研究已成為人們的聚焦點⑵。比如，Michael和Strichman采用了翻譯確認的方法對從Simulink到C的代碼生成器Real-TimeWorkshop（RTW）的編譯過程進行了形式化驗證。Simulink是MATLAB中的一種基于塊狀圖設計環境的可視化仿真工具，可實現動態系統建模、仿真和分析，被廣泛應用于線性系統、非線性系統、數字控制及數字信號處理的建模和仿真中。模型在Simulink中被認為是可執行的描述,借助于RTW代碼生成器，這些模型可以生成C代碼。 這一節主要介紹以Lustre和Signal為代表的同步數據流語言的代碼生成工具的研究現狀。就目前的進展情況而言，Lustre代碼生成工具的代表性研究主要集中于對翻譯過程進行驗證，即采用圖2所示的方法;而Signal代碼生成工具的代表性研究則是以翻譯確認的方法為主，即采用圖3和圖4所示的方法。4.1節介紹Lustre代碼生成工具的代表性研究，4.2節介紹Signal代碼生成工具的代表性研究，4.3節介紹一些相關的基礎性研究。

4.1 對翻譯過程進行形式化驗證的方法

對翻譯過程進行形式化驗證，通常需要對翻譯前后語言的語法和語義以及翻譯過程進行嚴格的形式化描述，然后對翻譯前后的語義保持關系進行機器證明。這其中涉及到許多相關的基礎性研究，本文為了更好地聚焦，不對這些方面的研究工作展開討論，僅列舉某些關系比較密切的內容，參見4.3節。 關于同步數據流語言編譯器，這方面最早的工作或許是Gimenez等于1999年試圖采用Coq針對ScadeV3進行翻譯過程的形式化驗證，但這項工作似乎沒有堅持下來，因相關資料不詳，這里不多述。 關于對翻譯過程進行驗證的同步數據流語言代碼生成工具的研究，在國際上較有代表性的長線項目主要是兩個團隊的工作：一個是法國INRIA的Pouzet團隊，另一個是清華大學計算機系的L2C項目組。 受CompCert項目的啟發，Paulin和Pouzet于2006年啟動了一個有關同步數據流語言編譯器驗證的長線項目，其源語言接近Scade的Lustre語言且具有LucidSynchro-ne的特征。據了解，該項目初期的工作集中于前端，完成了類型檢查和時鐘演算相關過程的驗證；后續又開展了因果性分析程序的驗證工作。后來，Biernacki等描述了該項目的一些相關工作細節，他們將Lustre語言的一個較早版本翻譯至Java和C代碼，采用了一種基于對象的中間語言。再后來，該團隊的Auger在其博士論文和技術論文中對該項目進行了較完整的表述（特別是理論基礎的論述方面）。從中可進一步了解到，Pouzet團隊的工作是針對一種小的但具有全部Lustre語言關鍵特征的語言MiniLS，并在此基礎上實現了同步數據流語言代碼生成工具的原型系統句。最近，該團隊的Bourke等又基于Biernacki和Auger等的工作，實現了從上述基于對象的中間語言Obc到CompCett的前端中間語言Clight的翻譯與驗證，從而得到一個核心Lustre子集的代碼生成工具Velus。 清華大學計算機系的L2C項目組于2010年開始了一項Lustre語言核心子集到C語言的可信翻譯器的研究（簡稱L2C項目）該項工作的原理與CompCert項目一致，工作目標和上述Pouzet團隊的項目相似。L2C項目組創立時主要是面向國內核電領域的實際需求，先是實現了單一時鐘情形下的一個完整翻譯過程的形式化驗證，后來又升級到一個可以支持多個嵌套時鐘的版本。L2C項目所定義的源語言Lustre綜合參考了Scade工具的Lustre語言版本和LustreV6，能夠體現同步數據流語言的主要特征。目前，該項目組正在開發和維護一個兼顧學術界和企業界的開源L2C版本。 上述兩個項目和CompCert項目一樣，源語言、目標語言和各階段中間語言的語法、語義、翻譯過程的定義以及語義保持性證明都在交互式輔助定理證明工具Coq中實現。然而，二者在許多方面存在不同。首先是源語言的差異，L2C編譯器立項時是出于國內某安全關鍵領域的實際需求，因此企業版的源語言最終定格為ScadeLustre語言的一個核心子集，而開源版的源語言則是將其中的高階迭代算子（9個）替換為了LustreV6中的高階迭代算子（5個）與L2C相比，Pouzet團隊的工作目前主要是面向學術研究，其源語言（包括最新版編譯器V§lus的源語言）不支持許多數組和結構體上的操作，尚未支持任何高階運算，并且對時態和時鐘算子的支持也略少于前者。其次，L2C項目代碼生成工具的目標語言C從一開始就借用了CompCert編譯器中Clight的語法和語義定義或］,語義定義中直接釆用了貫穿CompCert編譯器幾個階段的底層存儲模型；而Veins是從中間語言Obc翻譯到Clight，語義定義中的存儲模型有明顯的跨度。另外一個明顯的差異在于編譯器結構丄2C編譯器在Clight之前的核心中間層超過10層，而Veins編譯器在Clight之前的核心中間層僅有2層翻譯過程分散為多個階段，有利于簡化各翻譯階段的正確性證明，且具有更好的可擴展性。對于實現工業級的代碼生成工具來說，可擴展性是非常重要的；但同時翻譯過程也不應過多，否則會加重實現和維護的負擔。

4.2翻譯確認的方法

1998年，Pnueli第一次提出了翻譯確認的設計思想。Pnueii所給示范例子的源語言就是Signal特征的多時鐘同步數據流語言，其目標語言是C隨后，Pnueii在原有工作的基礎上繼續實現了對兩種同步數據流語言到C的編譯器的翻譯確認（這兩個編譯器中包含了大約100個優化規則），證明了翻譯確認方法也適用于優化編譯器，同時實現了一個翻譯確認器CVT（codevalidationtool），其可對編譯器每一次執行所產生的代碼進行檢測，通過模型檢驗判定與源代碼是否等價。這一技術用到編譯器可追溯的信息，如狀態變量是如何翻譯的。 近年來，Ngo和Talpin等基于翻譯確認的思想，也開展了同步數據流語言Signal到C的編譯器驗證工作。其主要工作包括：對源代碼和目標代碼使用統一的語義框架PDS（polynomialdynamicalsystems）建模，給出一種源和目標之間的抽象時鐘等價關系，通過對等價關系進行驗證來保證編譯器時鐘語義的一致性，其證明釆用SMT求解器自動完成；同時，也基于一種由一階邏輯公式定義的時鐘模型，開展了保持時鐘語義的翻譯確認工作,利用同步依賴圖（SDGs）對依賴關系的保持性進行確認；使用同步數據流求值圖（SDVGs）,對翻譯前后的求值語義保持性進行確認并基于這些技術，提出了一種大規模同步數據流語言編譯器驗證的擴展性良好的設計方案，該方案側重于對時鐘、數據依賴關系的保持性，以及變量的求值等價性等方面的翻譯確認。 如3.3節所述，翻譯確認方法不依賴于翻譯的具體過程，相比于對翻譯過程進行驗證的方法更具有可擴展性。然而,這種方法也有自身的缺陷，比如一般情況下難免存在某種程度的誤報（mis-alarm）率。總體來看，上述工作要達到工業級應用的要求，尚有較長的路要走。

4.3 —些相關的基礎性研究

與同步數據流語言編譯器驗證相關的研究有很多，它們都釆用了形式化的方法對同步數據流語言的語義進行定義，這對翻譯過程中的形式化驗證是很有幫助的。 Kahn將一類異步確定并行程序（現稱為Kahn網絡）描述為基于流變換（streamtransformation）的遞歸方程系統，并給出一種完全偏序集（CPO）語義。若將Kahn網絡限制到同步程序，則可以認為其是Lustre或其他同步語言的基礎。以Kahn網絡為出發點，人們也便于對同步數據流范型進行擴展叫。 無疑，對于同步數據流語言語義的形式化定義，Kahn網絡的CPO語義（指稱語義）是重要的參考之一。Paulin-Mo-hring基于Coq開發的KahnNetworksinCoq庫是這方面的一項重要工作，同時他們也開發了通用CPO庫，其比Kahn為Coq開發的CPO庫更加完善。 由于是一脈相承，針對Lucid或LucidSynchrone語義的一些研究。包括具體的操作或指稱語義定義以及這些工作在Coq環境中的實現，在Lustre語言代碼生成工具的研發中都可以借鑒。 借鑒上述工作，可以給出同步數據流語言的指稱語義，甚至使用Coq的描述語言給出精確的定義。然而，利用此類指稱語義來指導編譯器的實現以及完成翻譯過程的驗證有一定難度。 在Lustre語言的原始論文中，作者給出了Lustre語言的基本操作語義規則，涵蓋了時態算子的語義規則，也包含了時鐘演算的規則。在Caspi和Pouzet的研究其中也釆用類似方法來定義同步數據流語言的同步操作語義。這種操作語義的語義規則非常直觀且容易理解，然而若是要對應到編譯器的實現，還需要在面向實現方面進一步細化和改進。 還有許多與同步數據流語言相關的工作也值得關注。Cohen等于2005-2008年間提出了針對同步數據流系統更加寬松的同步和時鐘演算模型，如"。Delaval等提出了空間類型系統，以支持分布式系統上同步數據流語言的設計。 Schneider等開展了類Esterel的命令式同步語言的翻譯驗證工作，解決了Schizophrenia問題。輔助證明工具釆用HOL。Schizophrenia問題必須在因果分析（causalityanal-ysis）之前解決，因同步數據流語言不存在此類問題，故此處不贅述。 L2C課題組基于一個小的Lustre語言子集實現了一個時鐘歸一化過程的原型，可以將多時鐘流轉化為單一的時鐘流，并形式化驗證了變換過程的語義保持性然而，這一方法僅適用于傳統的fby算子（2個參數），在當前L2C項目?，財中未釆用。

結束語

現階段，與常規語言一樣，同步數據流語言編譯器（或代碼生成器）形式化驗證的方法可以大致分為兩大類：一類是針對編譯器本身的驗證（整體或部分），另一類是翻譯確認的方法（驗證目標代碼和源代碼之間的符合性，不驗證編譯器本身）前者是一種較完美的做法，但工作量大，不容易擴展；后者的擴展性較好，但只適合于解決局部問題。目前已有一些基于輔助定理證明器針對編譯器本身進行驗證的工作，比如本文提到的Pouzet項目組以及L2C項目組，二者的源語言均基于Lustre語言。關于翻譯確認，Pnueli等首先提出這一方案時，所釆用的示例就是基于同步數據流語言Signal;目前進展較好的工作有Ngo和Talpin等所開展的同步數據流語言Signal到C的編譯器驗證工作。 同步數據流語言與串行命令式語言的語義之間有很大差距，因而對同步數據流語言編譯器進行驗證（特別是針對編譯器本身進行驗證）的難度和工作量較大，但實際中存在此類需求，比如，花大力氣開發出的安全級產品一旦經過認證而投入使用后，允許再度更新的周期相當長。另外，也無需對編譯器的所有環節進行驗證，比如，目前很少有人特別重視lexer和parser部分的驗證工作。還有，為降低難度，在某些擴展和維護工作量過大的翻譯階段，我們可以選擇不對編譯器本身進行驗證，而選擇釆用翻譯確認的方法作為補充，比如Comp-Cert項目也有個別階段釆用了翻譯確認方案。用這種混合的方法能更好地平衡編譯器實現過程中的可信性、難度以及工作量之間的關系。 雖然經過形式化驗證的編譯器離商用尚有很長的路要走，但未來某些標準強制性地要求嚴格證明是極有可能的，工業界需要有一個逐漸適應的過程。對于代碼生成工具的開發，形式化驗證的方法無疑代表了一種未來新技術變革的趨勢。 現實中，可信編譯還有另外一層含義，即盡可能保障被編譯對象的可信。本文僅關注編譯過程的可信，不涉及這方面內容。

致謝

清華大學L2C項目組的師生為本研究提供了許多有價值的素材，在此表示感謝。 原文鏈接：

---

轉載于：http://www.digiproto.com/archives/2711

創作挑戰賽新人創作獎勵來咯，堅持創作打卡瓜分現金大獎

總結

以上是生活随笔為你收集整理的同步数据流语言代码生成工具的研究进展的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。