1、核心翻譯步驟示例

本節(jié)我們以第2節(jié)提到的Lustre語(yǔ)言的主要特性為線索來(lái)解釋L2C在翻譯過(guò)程中的關(guān)鍵節(jié)點(diǎn)是如何處理的, 并以圖 1的實(shí)例來(lái)解釋Lustre程序是如何被一步步地翻譯到Clight語(yǔ)言的.

1.1 數(shù)據(jù)流并發(fā)性

Lustre程序具有數(shù)據(jù)流并發(fā)性, 而Clight程序卻是串行執(zhí)行的.因此, 翻譯過(guò)程中的一大難題就是要將Lustre語(yǔ)句串行化.現(xiàn)在一般采用的因果分析和排序大多采用測(cè)試或翻譯確認(rèn)的方法, 未進(jìn)行形式化驗(yàn)證.對(duì)于L2C構(gòu)建經(jīng)過(guò)形式化證明的可信編譯器的目標(biāo), 對(duì)排序做嚴(yán)格證明是必要的.我們首先定義Lustre*中的因果關(guān)系.支持國(guó)產(chǎn)處理器仿真的全數(shù)字實(shí)時(shí)仿真平臺(tái)SkyEye與可信編譯器L2C的核心翻譯步驟

(1) 如果一個(gè)等式A的左值出現(xiàn)在等式B的右值中, 則說(shuō)等式B依賴于等式A.

(2) 如果一個(gè)節(jié)點(diǎn)A的左值出現(xiàn)在等式B的時(shí)鐘中, 則說(shuō)等式B依賴于等式B.

然后, 我們定義拓?fù)渑判虻男再|(zhì), 并且定義拓?fù)渑判虻葍r(jià)性定理, 即任意兩個(gè)滿足拓?fù)渑判蛐再|(zhì)的程序在串行執(zhí)行語(yǔ)義中是等價(jià)的, 以此來(lái)保證串行化方案的正確性.最后利用Coq實(shí)現(xiàn)拓?fù)渑判蛩惴? 將并行的LustreS串行化, 并以此算法完成之前定義的拓?fù)渑判蛐再|(zhì)和語(yǔ)義等價(jià)性證明.

實(shí)際翻譯效果以圖 1中的第7行~第8行為例, 按照第1條因果關(guān)系的定義,?圖 1中第8行的左值出現(xiàn)在了第7行的右值中, 所以第7行語(yǔ)句依賴于第8行.圖 4顯示了拓?fù)渑判蚝驦ustreS程序中與圖 1第7行~第8行對(duì)應(yīng)的代碼片段, 在排序后,?圖 1的第7行被翻譯為圖 4中的第4行,?圖 1中的第8行被對(duì)應(yīng)到圖 4中的第2行, 可見(jiàn)排序后的語(yǔ)句滿足因果關(guān)系的定義.

1.2 高階算子

Lustre提供了10多個(gè)高階算子 (涵蓋了LustreV6支持的所有高階算子), 包括map, red等.圖 1第10行使用了map算子, 本節(jié)以map為例來(lái)介紹高階算子消去.Lustre中map算子的形式為map《op; size》(a1,?a2, …,?an), 其中,?a1~an是n個(gè)輸入數(shù)組, size為數(shù)組的大小; 而op為一個(gè)操作, 可以是運(yùn)算符或一個(gè)節(jié)點(diǎn), 擁有n個(gè)輸入?yún)?shù).map算子運(yùn)算的結(jié)果為一個(gè)數(shù)組, 記為res, 其中, res[i]=op (a1[i],?a2[i], …,?an[i]).圖 1中的p值展示了圖 1第10行map算子運(yùn)算的結(jié)果, 可見(jiàn)高階算子簡(jiǎn)化了對(duì)數(shù)組的循環(huán)操作.

由于目標(biāo)語(yǔ)言Clight不支持高階運(yùn)算, 所以在翻譯過(guò)程中, 需要消去Lustre*中的高階算子.基于高階算子對(duì)數(shù)組處理的特點(diǎn), 我們最終在LustreS到LustreR1階段將所支持的各個(gè)高階算子按其語(yǔ)義特性展開(kāi)為Clight支持的語(yǔ)法結(jié)構(gòu), 主體為for循環(huán)結(jié)構(gòu).

圖 5展示了圖 1中第10行的map運(yùn)算在LustreS這一層的中間表示, 可見(jiàn), 在LustreS這一層L2C不會(huì)對(duì)map高階算子做翻譯.

經(jīng)過(guò)LustreRGen過(guò)程, L2C會(huì)將map高階表達(dá)式轉(zhuǎn)換成for循環(huán), 如圖 6所示.

通過(guò)設(shè)計(jì)翻譯算法將LustreS中的高階復(fù)雜運(yùn)算分解成LustreR1中多個(gè)基礎(chǔ)運(yùn)算的循環(huán), 我們消除了Lustre*程序中的所有高階算子.

1.3 時(shí)態(tài)和時(shí)鐘算子

Lustre支持如LustreV6的一些可以操作流數(shù)據(jù)的時(shí)態(tài)算子, 如fby, 以及操作變量時(shí)鐘的時(shí)鐘算子, 如when算子.在Lustre程序中, 每個(gè)變量均有自己的時(shí)鐘, 默認(rèn)情況下為一個(gè)全局基本時(shí)鐘, 該時(shí)鐘在每個(gè)時(shí)鐘周期都為True.如圖 2中擁有全局基本時(shí)鐘的x3, 在每個(gè)時(shí)鐘周期都有值.而Lustre提供的when算子則可以用來(lái)改變某個(gè)變量的時(shí)鐘, 如圖 2中的y1,?b為True的周期有值且與x3當(dāng)前周期值相同, 但b為False的周期的值則是未定義.再如Lustre提供的fby算子, 可以用來(lái)訪問(wèn)流數(shù)據(jù)的歷史值, 它不改變時(shí)鐘, 返回值相當(dāng)于向右shift流數(shù)據(jù)的值, 如圖 2中的s, 它的值在y1上整體向右shift了一位, 并且在shift產(chǎn)生的空缺值中補(bǔ)上了fby函數(shù)指定的默認(rèn)值5.支持國(guó)產(chǎn)處理器仿真的全數(shù)字實(shí)時(shí)仿真平臺(tái)SkyEye與可信編譯器L2C的核心翻譯步驟

L2C在LustreS到LustreR1階段會(huì)處理所有時(shí)鐘算子, 在LustreR3到LustreF1階段會(huì)處理所有的時(shí)態(tài)算子.以fby算子為例, 在LustreF1中,?圖 1中Stay節(jié)點(diǎn)內(nèi)的第27行和第28行, fby算子會(huì)被最終翻譯成如圖 7所示的LustreF1代碼, 其中a為Stay節(jié)點(diǎn)的輸入?yún)?shù).

L2C引入acg_init變量來(lái)標(biāo)識(shí)當(dāng)前周期是否為第1個(gè)周期, 如果是第1個(gè)周期, 那么將對(duì)變量m和n賦初值, 賦初值時(shí)會(huì)根據(jù)fby指定的周期數(shù)來(lái)初始化存儲(chǔ)m和n的數(shù)組大小, 并在數(shù)組中對(duì)每個(gè)值賦予fby指定的默認(rèn)值, 然后在之后的周期依次循環(huán)遍歷數(shù)組的值, 并在每次讀取值之后在數(shù)組當(dāng)前位置記錄變量在fby之前當(dāng)前周期的值.以圖 2的輸入值為例, 我們將圖 7中n對(duì)應(yīng)的fby相關(guān)參數(shù)acg_fby2前4個(gè)周期的變化過(guò)程展示出來(lái), 如圖 8所示, 便于更好地理解圖 7的翻譯結(jié)果.

1.4 翻譯至Clight

經(jīng)過(guò)前面幾個(gè)核心步驟后, 已經(jīng)消除了Lustre中最顯著的同步數(shù)據(jù)流特征, 程序已經(jīng)十分接近常規(guī)的串行命令式語(yǔ)言.又經(jīng)過(guò)后續(xù)若干個(gè)關(guān)鍵步驟 (包含初始化函數(shù)生成ResetfunGen) 到LustreC, 已經(jīng)十分接近Clight, 經(jīng)由最后兩個(gè)步驟實(shí)現(xiàn)與CompCert完全對(duì)接 (如圖 3所示).從LustreC到Clight的翻譯過(guò)程中, 在語(yǔ)法上幾乎沒(méi)有太大的變化, 但在語(yǔ)義環(huán)境上差異較大, 證明工作繁重.圖 9展示了L2C翻譯圖 1所示Lustre程序中Main節(jié)點(diǎn)的最終結(jié)果, 具體翻譯驗(yàn)證的難點(diǎn)我們將在下一節(jié)詳細(xì)描述.

1.5 流數(shù)據(jù)對(duì)象

如圖 1所示, 主節(jié)點(diǎn)Main的輸入和輸出都是無(wú)窮長(zhǎng)的流數(shù)據(jù), 簡(jiǎn)單來(lái)說(shuō), 每個(gè)時(shí)鐘周期, Lustre*程序以輸入流數(shù)據(jù)當(dāng)前時(shí)鐘周期的值傳入Main節(jié)點(diǎn)作為輸入, 執(zhí)行得到輸出流中當(dāng)前時(shí)鐘周期的值.

由于程序獲取輸入和處理輸出的方式不盡相同, 所以L2C只會(huì)翻譯Lustre*程序中的節(jié)點(diǎn), 并不會(huì)給最終的Clight程序中加入C語(yǔ)言的入口函數(shù)Main函數(shù).在實(shí)際使用中, 如圖 10所示, 我們會(huì)編寫C語(yǔ)言的main函數(shù)循環(huán)調(diào)用調(diào)用生成Main函數(shù), 以此來(lái)處理流數(shù)據(jù).

高性能嵌入式仿真軟件SkyEye

隨著科技的發(fā)展，系統(tǒng)工程的設(shè)計(jì)體量逐漸龐大起來(lái)，尤其是對(duì)于軌道交通、航空航天、核電站等安全關(guān)鍵領(lǐng)域中，如何在復(fù)雜度逐年變大的同時(shí)保證其安全性和可靠性，是近年來(lái)各大公司需要研究的課題。最近比較火熱的基于模型的系統(tǒng)工程（MBSE）技術(shù)則給大家提供了一種全新的技術(shù)方向，分享一種全數(shù)字實(shí)時(shí)仿真的安全關(guān)鍵領(lǐng)域解決方案，提供一種新的解決思路。支持國(guó)產(chǎn)處理器仿真的全數(shù)字實(shí)時(shí)仿真平臺(tái)SkyEye與可信編譯器L2C的核心翻譯步驟，提供高效的運(yùn)算速度，提高研發(fā)效率和安全性。

新一代全數(shù)字仿真平臺(tái)SkyEye

基于模型的全數(shù)字研發(fā)解決方案MBSE工具軟件SkyEye是能夠滿足模擬或仿真外部硬件行為進(jìn)行軟件運(yùn)行和測(cè)試需求的工具。該工具運(yùn)用國(guó)際流行的仿真、測(cè)試腳本語(yǔ)言來(lái)編寫外部硬件邏輯行為所產(chǎn)生外部激勵(lì)事件以構(gòu)成嵌入式軟件的外部信號(hào)激勵(lì)或數(shù)據(jù)輸入，從而滿足軟件在全數(shù)字仿真運(yùn)行環(huán)境下無(wú)須人的干預(yù)而閉環(huán)運(yùn)行的要求。支持國(guó)產(chǎn)處理器仿真的全數(shù)字實(shí)時(shí)仿真平臺(tái)SkyEye與可信編譯器L2C的核心翻譯步驟

作為基于嵌入式應(yīng)用的特點(diǎn)，嵌入式軟件全數(shù)字仿真測(cè)試支撐平臺(tái)SkyEye要為嵌入式系統(tǒng)提供全數(shù)字仿真測(cè)試環(huán)境或測(cè)試平臺(tái)，實(shí)現(xiàn)對(duì)嵌入式系統(tǒng)進(jìn)行實(shí)時(shí)、閉環(huán)的系統(tǒng)測(cè)試。在該平臺(tái)上完成被測(cè)軟件的分析、運(yùn)行和測(cè)試，最重要的是要實(shí)現(xiàn)嵌入式系統(tǒng)外部事件的全數(shù)字仿真平臺(tái)，使得嵌入式軟件就像在真實(shí)硬件環(huán)境下連續(xù)不中斷地運(yùn)行。

---

本文標(biāo)題：支持國(guó)產(chǎn)處理器仿真的全數(shù)字實(shí)時(shí)仿真平臺(tái)SkyEye與可信編譯器L2C的核心翻譯步驟

本文鏈接：http://www.digiproto.com

總結(jié)

以上是生活随笔為你收集整理的支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。