楊志斌 , 袁勝浩 , 謝 健 , 周 勇 , 陳 哲 , 薛 壘 , Jean-Paul BODEVEIX, Mamoun FILALI

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,江蘇 南京 211106)

2(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心,江蘇 南京 210093)

3(上海航天電子技術(shù)研究所,上海 201109)

4(IRIT-University of Toulouse, Toulouse 31062, France)

安全關(guān)鍵軟件(safety-critical software)[1]是指應(yīng)用于航空、航天、交通、能源等領(lǐng)域的安全關(guān)鍵系統(tǒng)中,且其運(yùn)行情況可能引起系統(tǒng)處于危險(xiǎn)狀態(tài),從而導(dǎo)致財(cái)產(chǎn)損失、環(huán)境破壞或者人員傷害的一類軟件.隨著功能需求的發(fā)展,能夠提供更強(qiáng)計(jì)算能力而又能減少電子設(shè)備的體積、重量和功耗(size,weight and power,即SWaP特性)的多核處理器將在安全關(guān)鍵領(lǐng)域得到廣泛應(yīng)用.例如,在航空領(lǐng)域,風(fēng)河公司(WindRiver)提出了支持多核處理器的 Vxworks 653操作系統(tǒng) V3.0版本[2];而為了滿足將來(lái)航天應(yīng)用的復(fù)雜需求,歐空局(European Space Agency,簡(jiǎn)稱ESA)開(kāi)發(fā)了基于四核LEON4的下一代微處理器試驗(yàn)板(LEON4-N2X)[3].

近年來(lái),模型驅(qū)動(dòng)(model-driven),尤其是采用形式化模型驅(qū)動(dòng)的安全關(guān)鍵軟件設(shè)計(jì)與開(kāi)發(fā)方法逐漸受到重視,并被工業(yè)界認(rèn)為是切實(shí)可行的重要手段.例如,國(guó)際民航領(lǐng)域使用的機(jī)載系統(tǒng)適航審定中的軟件開(kāi)發(fā)標(biāo)準(zhǔn)DO-178C[4]就將模型驅(qū)動(dòng)和形式化方法(即 DO-331[5]和 DO-333[6])作為其核心標(biāo)準(zhǔn)的重要技術(shù)補(bǔ)充.模型驅(qū)動(dòng)開(kāi)發(fā)方法將模型作為整個(gè)軟件開(kāi)發(fā)過(guò)程的核心元素,在設(shè)計(jì)階段就建立軟件模型,并盡早進(jìn)行驗(yàn)證和分析.同時(shí),模型的重用以及基于模型的自動(dòng)代碼生成,都有助于降低軟件開(kāi)發(fā)時(shí)間和成本.

安全關(guān)鍵系統(tǒng),是一類反應(yīng)式系統(tǒng)(reactive system),它不斷地和環(huán)境進(jìn)行交互,即從環(huán)境中得到輸入,經(jīng)過(guò)計(jì)算,然后輸出給環(huán)境,并重復(fù)這一過(guò)程.其中環(huán)境包括:被系統(tǒng)控制的物理設(shè)備、系統(tǒng)的操作人員或其他的反應(yīng)式系統(tǒng).同步語(yǔ)言基于同步假設(shè)理論(synchronous hypothesis)來(lái)表達(dá)系統(tǒng)的功能行為.目前,有 ESTEREL[7]、LUSTRE[8]、SCADE[9]、SIGNAL[10]、QUARTZ[11]等同步語(yǔ)言,這些同步語(yǔ)言可以看作是對(duì)同步假設(shè)理論的不同實(shí)現(xiàn),而且同步語(yǔ)言在安全關(guān)鍵系統(tǒng)領(lǐng)域得到實(shí)際應(yīng)用.例如,空客使用 SCADE對(duì) A350、A380的飛控子系統(tǒng)[12]進(jìn)行建模和代碼生成.ESTEREL、LUSTRE和QUARTZ語(yǔ)言使用perfect synchrony模式(即純同步模式),即存在一個(gè)全局時(shí)鐘,而SIGNAL語(yǔ)言使用Polychrony模式(即多態(tài)同步模式),可能不存在一個(gè)全局時(shí)鐘,可以更加自然地表達(dá)分布式系統(tǒng).現(xiàn)有的SIGNAL編譯器Polychrony目前主要支持串行代碼生成和仿真分析,較少考慮在多核處理器上的多線程代碼生成.

在同步語(yǔ)言多線程代碼生成方面[13-15],目前研究主要考慮基于全局異步局部同步(globally asynchronous locally synchronous,簡(jiǎn)稱GALS)的多線程代碼生成,即系統(tǒng)由具有不同時(shí)鐘的多個(gè)進(jìn)程組成,而每個(gè)進(jìn)程是單時(shí)鐘的.然而,在同步語(yǔ)言模型中,單個(gè)進(jìn)程內(nèi)部也往往存在潛在的并行執(zhí)行信息.尤其是可以自然表達(dá)分布式系統(tǒng)的SIGNAL語(yǔ)言,其語(yǔ)法的基本結(jié)構(gòu)中包含多時(shí)鐘操作,可以比較自然地支持在進(jìn)程內(nèi)部描述并行執(zhí)行操作.

本文研究基于 SIGNAL語(yǔ)言表達(dá)的單進(jìn)程程序的多線程代碼生成方法,并給出一種基于函數(shù)式編程語(yǔ)言O(shè)CAML實(shí)現(xiàn)的同步語(yǔ)言 SIGNAL多線程代碼生成工具.該工具是 SIGNAL串行代碼生成工具 Min SIGNAL[16-18]在多線程代碼生成方面的擴(kuò)展.整個(gè)生成器分為前端和后端:首先,已有 MinSIGNAL編譯器前端對(duì)輸入的 SIGNAL程序進(jìn)行用戶程序標(biāo)準(zhǔn)化,轉(zhuǎn)換為中間表達(dá)式即同步多時(shí)鐘衛(wèi)式動(dòng)作(synchronous clocked guarded actions,簡(jiǎn)稱S-CGA),并進(jìn)行時(shí)鐘演算,生成S-CGA中間程序.其次,基于擴(kuò)展的代碼生成器后端輸出可執(zhí)行的多線程C/Java代碼.擴(kuò)展的代碼生成器后端延續(xù)MinSIGNAL的模塊化設(shè)計(jì)思想,主要包括:構(gòu)建時(shí)鐘數(shù)據(jù)依賴圖(clock data dependency graph,簡(jiǎn)稱CDDG),以分析S-CGA程序中變量(全局的時(shí)鐘變量和數(shù)據(jù)變量)之間的依賴關(guān)系;在使用拓?fù)渑判騽澐炙惴ǚ治鯟DDG的基礎(chǔ)上,分別提出拓?fù)渑判騼?yōu)化算法和基于流水線方式的任務(wù)劃分方法以提高最終目標(biāo)代碼執(zhí)行速度;基于劃分結(jié)果生成虛擬多線程代碼,進(jìn)一步生成可執(zhí)行多線程C/Java程序,并在多核處理器上進(jìn)行實(shí)驗(yàn).

本文第1節(jié)簡(jiǎn)要介紹SIGNAL語(yǔ)言的基本概念和我們的一些前期研究.第2節(jié)給出同步語(yǔ)言多線程代碼生成方法的總體研究框架.第 3節(jié)介紹同步語(yǔ)言多線程代碼生成方法和步驟,包括多線程代碼生成器前端、構(gòu)造時(shí)鐘數(shù)據(jù)依賴圖、任務(wù)劃分算法和多線程代碼生成.第 4節(jié)給出基于 OCAML的工具實(shí)現(xiàn),并基于案例進(jìn)行可執(zhí)行多線程代碼實(shí)驗(yàn)和分析.第5節(jié)給出相關(guān)工作比較.第6節(jié)是本文的總結(jié)和展望.

1 研究背景

1.1 同步語(yǔ)言SIGNAL

SIGNAL是由Le Guernic、Benveniste和Gautier等人提出的一種聲明式數(shù)據(jù)流同步語(yǔ)言.基于同步假設(shè)理論,SIGNAL語(yǔ)言中定義了一類對(duì)象,稱為信號(hào)(signal),是一種帶類型的無(wú)限長(zhǎng)的值序列.在給定邏輯時(shí)刻下,信號(hào)可以是“存在”狀態(tài)并具有對(duì)應(yīng)的數(shù)值,或者是“缺失”狀態(tài),記為⊥.信號(hào)處于存在狀態(tài)對(duì)應(yīng)邏輯時(shí)刻組成的集合構(gòu)成信號(hào)對(duì)應(yīng)的邏輯時(shí)鐘(簡(jiǎn)稱時(shí)鐘).在SIGNAL中,兩個(gè)信號(hào)同步當(dāng)且僅當(dāng)其邏輯時(shí)鐘相同.

SIGNAL語(yǔ)言通過(guò)數(shù)據(jù)流等式進(jìn)行建模,它提供 4類基本的數(shù)據(jù)流等式結(jié)構(gòu):(1) 瞬時(shí)函數(shù)(y:=f(x1,x2,…,xn));(2) 延遲(y:=x1$init c);(3) 條件采樣(y:=x1whenx2);(4) 確定性合并(y:=x1defaultx2).

此外,按照時(shí)鐘關(guān)系劃分,4類基本結(jié)構(gòu)可以被分為單時(shí)鐘操作(瞬時(shí)函數(shù)和延遲)和多時(shí)鐘操作(條件采樣和確定性合并):前者要求所有信號(hào)都是同步的,而后者允許信號(hào)可以不同步.例如,在確定性合并中,給定邏輯時(shí)刻下x1或者x2處于存在狀態(tài)即可以保證y處于存在狀態(tài).

SIGNAL不僅提供基本結(jié)構(gòu),還提供一些擴(kuò)展結(jié)構(gòu)以支持顯式的時(shí)鐘操作.例如,時(shí)鐘同步:x1^=x2;時(shí)鐘并運(yùn)算x:=x1^+x2、時(shí)鐘交運(yùn)算x:=x1^*x2、時(shí)鐘補(bǔ)運(yùn)算x:=x1^-x2;時(shí)鐘小于運(yùn)算x1^x2.本質(zhì)上,擴(kuò)展結(jié)構(gòu)是由基本結(jié)構(gòu)進(jìn)行復(fù)合操作來(lái)定義[19].

進(jìn)程是SIGNAL的編程單元(programming unit),由輸入、輸出以及數(shù)據(jù)流等式組合起來(lái)構(gòu)成.進(jìn)程包含組合(composition)與局部聲明(local declaration).

另外,SIGNAL語(yǔ)言具有多種形式語(yǔ)義,如基于蹤跡的指稱語(yǔ)義[19,20]、基于標(biāo)簽?zāi)Ｐ偷闹阜Q語(yǔ)義[19]以及基于同步變遷系統(tǒng)[21]的操作語(yǔ)義等.在文獻(xiàn)[22]中,我們基于定理證明器 Coq[23]證明了 SIGNAL語(yǔ)言的蹤跡語(yǔ)義和標(biāo)簽?zāi)Ｐ驼Z(yǔ)義的等價(jià)性.

我們給出一個(gè)同步語(yǔ)言SIGNAL示例:Count進(jìn)程.該進(jìn)程的第2行、第3行聲明輸入信號(hào)y1,x1和x2;第4行聲明輸出信號(hào)y;第5行、第6行數(shù)據(jù)流等式屬于擴(kuò)展結(jié)構(gòu),第7行～第11行數(shù)據(jù)流等式屬于基本結(jié)構(gòu);第13行是局部聲明.我們將此程序貫穿全文用于介紹整個(gè)多線程代碼生成器的工作過(guò)程.

Example 1 Count process in SIGNAL例1 Count進(jìn)程

1.2 前期研究

在分析SIGNAL語(yǔ)言的已有編譯器Polychrony的基礎(chǔ)上,我們基于OCAML實(shí)現(xiàn)了一種新的SIGNAL串行代碼生成工具M(jìn)inSIGNAL[16-18],其編譯步驟如圖1所示.

相比Polychrony,MinSIGNAL具有的特征包括:

(1) MinSIGNAL支持的輸入為SIGNAL的子集(稱為MinSIGNAL),包括SIGNAL語(yǔ)言中的基本結(jié)構(gòu)、擴(kuò)展結(jié)構(gòu)、組合、局部聲明等,不包括Polychrony工具庫(kù);

(2) 考慮將來(lái)支持多種同步語(yǔ)言的集成,提出了一種新的中間表達(dá)式,即同步多時(shí)鐘衛(wèi)式動(dòng)作S-CGA;

(3) 基于Coq完成代碼生成器前端SIGNAL到S-CGA之間的語(yǔ)義保持證明.

本文是MinSIGNAL在多線程代碼生成方面的擴(kuò)展,而MinSIGNAL的最終目標(biāo)是生成一個(gè)新的SIGNAL驗(yàn)證編譯器(verified compiler),即在定理證明器 Coq中規(guī)約并證明編譯規(guī)則的語(yǔ)義保持,然后從證明中自動(dòng)抽取編譯器的OCAML實(shí)現(xiàn).目前基于OCAML的工具實(shí)現(xiàn)是在定理證明器Coq中進(jìn)行規(guī)約的基礎(chǔ),并將和自動(dòng)生成的驗(yàn)證編譯器進(jìn)行對(duì)比分析.

2 MinSIGNAL多線程代碼生成研究框架

同步語(yǔ)言SIGNAL多線程代碼生成器的總體框架如圖2所示.整個(gè)生成器包括前端和后端兩個(gè)部分:編譯器前端對(duì)輸入的SIGNAL程序進(jìn)行用戶程序標(biāo)準(zhǔn)化、轉(zhuǎn)換為S-CGA程序、進(jìn)行時(shí)鐘演算等步驟生成S-CGA中間程序.其次,基于擴(kuò)展的代碼生成器后端輸出可執(zhí)行的多線程 C/Java代碼.擴(kuò)展的代碼生成器后端延續(xù)MinSIGNAL的模塊化設(shè)計(jì)思想,主要包括:

(1) 定義并構(gòu)建時(shí)鐘數(shù)據(jù)依賴圖 CDDG,以分析 S-CGA程序中變量(全局的時(shí)鐘變量和數(shù)據(jù)變量)之間的依賴關(guān)系;

(2) 在使用拓?fù)渑判騽澐炙惴ǚ治鯟DDG的基礎(chǔ)上,分別提出拓?fù)渑判騼?yōu)化算法和基于流水線方式的任務(wù)劃分方法,以提高最終目標(biāo)代碼執(zhí)行速度;

(3) 基于劃分結(jié)果生成虛擬多線程代碼(平臺(tái)無(wú)關(guān)),進(jìn)一步生成可執(zhí)行多線程C/Java程序(平臺(tái)相關(guān)).

串行代碼生成過(guò)程主要由時(shí)鐘樹(shù)驅(qū)動(dòng)完成,多線程代碼生成過(guò)程主要由數(shù)據(jù)依賴圖驅(qū)動(dòng)完成.即在串行代碼生成過(guò)程中,通過(guò)分析時(shí)鐘樹(shù)上包含的時(shí)鐘關(guān)系得到串行代碼的控制結(jié)構(gòu),分析數(shù)據(jù)依賴圖中包含的數(shù)據(jù)依賴關(guān)系確定控制結(jié)構(gòu)中語(yǔ)句的執(zhí)行順序;在多線程代碼生成過(guò)程中,還需要定義CDDG以便同時(shí)顯式地考慮時(shí)鐘和數(shù)據(jù)之間的依賴關(guān)系.

3 MinSIGNAL多線程代碼生成方法和步驟

MinSIGNAL多線程代碼生成器由前端和后端兩部分組成.首先簡(jiǎn)要介紹代碼生成器前端,即已有 Min SIGNAL串行代碼生成器前端及時(shí)鐘演算.然后,按照編譯步驟依次介紹時(shí)鐘數(shù)據(jù)依賴圖、任務(wù)劃分和多線程代碼生成.

3.1 多線程代碼生成器前端

由于此代碼生成器前端主要是重用已有的MinSIGNAL串行代碼生成器前端(參見(jiàn)文獻(xiàn)[16-18]),這里,我們僅簡(jiǎn)要給出其主要步驟:用戶程序標(biāo)準(zhǔn)化、中間語(yǔ)言S-CGA和時(shí)鐘演算.

(1) 用戶程序標(biāo)準(zhǔn)化

如第1.1節(jié)和第1.2節(jié)所述,MinSIGNAL支持的輸入為SIGNAL子集(稱為MinSIGNAL),包括SIGNAL語(yǔ)言中的基本結(jié)構(gòu)、擴(kuò)展結(jié)構(gòu)、組合、局部聲明等,不包括Polychrony工具庫(kù).所謂用戶程序標(biāo)準(zhǔn)化,即代碼生成器在對(duì)用戶程序進(jìn)行詞法和語(yǔ)法分析之后,將用戶程序中使用的擴(kuò)展結(jié)構(gòu)轉(zhuǎn)換為 SIGNAL語(yǔ)言的基本結(jié)構(gòu).我們稱基本結(jié)構(gòu)為kSIGNAL(kernel SIGNAL).kSIGNAL的抽象語(yǔ)法如下所示.

我們?cè)谖墨I(xiàn)[16-18]中給出了用戶程序標(biāo)準(zhǔn)化的轉(zhuǎn)換規(guī)則.這里,針對(duì)例1給出部分轉(zhuǎn)換示例.

對(duì)于擴(kuò)展結(jié)構(gòu),如時(shí)鐘同步操作x1^=x2,首先分別定義x1和x2的時(shí)鐘變量C___1和C___2,然后通過(guò)兩個(gè)時(shí)鐘變量相等表示時(shí)鐘同步操作^=.

時(shí)鐘同步操作 標(biāo)準(zhǔn)化后結(jié)果x1^=x2 C___1=x1==x1 C___2=x2==x2 C___3=C___1==C___2

另外,還需對(duì)復(fù)合的基本結(jié)構(gòu)進(jìn)行處理,目的是為了降低源程序到中間語(yǔ)言的轉(zhuǎn)換難度.例如,y2:=(y1+1)$ init 2的標(biāo)準(zhǔn)化結(jié)構(gòu)如下.

(2) 中間表達(dá)式S-CGA

隨著同步語(yǔ)言的發(fā)展,學(xué)術(shù)界已提出多種同步語(yǔ)言,導(dǎo)致集成不同同步語(yǔ)言成為熱點(diǎn)研究問(wèn)題[24,25],因?yàn)檫@不僅可以更深刻地理解不同同步計(jì)算模型之間的區(qū)別,更重要的是,可以提供或重用統(tǒng)一的驗(yàn)證、仿真和代碼生成工具.集成的解決方案主要是給出一種通用的中間表達(dá)式.例如,Polychrony中使用HCDG[26]、L2C項(xiàng)目中使用S-Lustre*AST[27,28]、QUARTZ編譯器使用CGA[29,30]以及本文使用的S-CGA等中間語(yǔ)言.

定義1(同步多時(shí)鐘衛(wèi)式動(dòng)作(S-CGA)). 在S-CGA中衛(wèi)式動(dòng)作的形式為γ?A,其中,γ為衛(wèi)式,A為要執(zhí)行的動(dòng)作.其直觀語(yǔ)義為,如果衛(wèi)式γ為真,則執(zhí)行動(dòng)作A.γ?A主要包括5種形式,見(jiàn)表1.

Table 1 Form of guarded actions表1 衛(wèi)式動(dòng)作形式

其中,

· 衛(wèi)式γ是定義在信號(hào)變量X(源 SIGNAL中的輸入、輸出和局部變量)、X的邏輯時(shí)鐘(x∈X,其時(shí)鐘為?)及其初始時(shí)鐘(init(x?))之上的布爾條件.

· 動(dòng)作A包括:立即賦值、延遲賦值、約束定義、輸入動(dòng)作和輸出動(dòng)作.其中,τ是定義在X上的表達(dá)式,σ則是定義在X及其邏輯時(shí)鐘上的布爾表達(dá)式.

(1) 立即賦值,給定邏輯時(shí)刻t,當(dāng)γ中所有信號(hào)變量都處于存在狀態(tài)且γ為true、x和τ都處于存在狀態(tài)時(shí),則將τ的取值賦給x;

(2) 延遲賦值,給定邏輯時(shí)刻t1,γ中所有信號(hào)變量都處于存在狀態(tài),且γ為 true,x和τ在t1時(shí)刻都處于存在狀態(tài),在下一邏輯時(shí)刻t2中,如果x處于存在狀態(tài),則在t2時(shí)刻將t1時(shí)刻τ的取值賦值給當(dāng)前時(shí)刻的x;

(3) 約束定義,如果γ中所有信號(hào)變量同時(shí)處于存在狀態(tài)且γ為 true,那么σ處于存在狀態(tài)并且為 true.所有S-CGA程序中的操作都需要滿足約束定義;

(4) 輸入動(dòng)作,當(dāng)γ=true時(shí),從環(huán)境中讀取輸入變量x;

(5) 輸出動(dòng)作,當(dāng)γ=true時(shí),將計(jì)算結(jié)果x輸出到環(huán)境.

多個(gè) S-CGA組合采用同步組合操作||.因此,S-CGA具有與 SIGNAL語(yǔ)言一致的表達(dá)確定性并發(fā)行為的能力.

表2給出kSIGNAL2S-CGA的轉(zhuǎn)換規(guī)則.基于轉(zhuǎn)換規(guī)則,SIGNAL語(yǔ)言中的基本結(jié)構(gòu)(即kSIGNAL)所表達(dá)的功能關(guān)系和時(shí)鐘關(guān)系一一映射為S-CGA中的對(duì)應(yīng)表示.SIGNAL到S-CGA之間具體的轉(zhuǎn)換規(guī)則解釋以及語(yǔ)義保持證明思路參考文獻(xiàn)[16].

Table 2 Rules of kSIGNAL2S-CGA表2 kSIGNAL到S-CGA的轉(zhuǎn)換規(guī)則

(3) 時(shí)鐘演算

同步模型除顯式地表達(dá)功能關(guān)系外,還隱式地表達(dá)了時(shí)鐘關(guān)系.因此,在代碼生成之前,一般同步語(yǔ)言編譯器都需要經(jīng)過(guò)時(shí)鐘演算,從而確定該同步模型可執(zhí)行,并優(yōu)化生成后的代碼.首先,根據(jù)S-CGA語(yǔ)義,從 S-CGA表達(dá)式中生成時(shí)鐘關(guān)系等式集合,其基本產(chǎn)生規(guī)則見(jiàn)表3.

Table 3 Rules of S-CGA2Clock equations表3 S-CGA到時(shí)鐘關(guān)系等式的轉(zhuǎn)換規(guī)則

針對(duì)例1給出部分轉(zhuǎn)換示例及其時(shí)鐘關(guān)系等式如下.

SIGNAL 部分S-CGA 部分時(shí)鐘關(guān)系等式s1:=y1 when x1 s2:=y2 when x2 x:= s1 default s2 sassume yx sassume yx xassume ss ?()? ?()1 11 2 22 12????? ????(?)xyxyx ???()()=??? 1122......

等式左側(cè)?x為時(shí)鐘變量,而右邊等式是對(duì)應(yīng)的定義,時(shí)鐘關(guān)系等式x→y和y→x可表示為x=y.在時(shí)鐘關(guān)系等式集合中,需要對(duì)具有相同時(shí)鐘的不同時(shí)鐘關(guān)系等式進(jìn)行優(yōu)化以保證生成后的代碼執(zhí)行效率更高.時(shí)鐘關(guān)系等式集合的消解原理為:將等式右側(cè)中的時(shí)鐘變量用其定義進(jìn)行替換,并不斷地迭代,最后檢查不同時(shí)鐘變量之間是否等價(jià)(基于BDD或SMT).如果等價(jià),則歸為同一個(gè)時(shí)鐘等價(jià)類,時(shí)鐘演算之后的程序中時(shí)鐘等價(jià)類用于替代S-CGA對(duì)應(yīng)的時(shí)鐘變量.

針對(duì)例1,代碼生成器前端生成的部分S-CGA程序如圖3所示.S-CGA程序中包括輸入動(dòng)作、輸出動(dòng)作、立即動(dòng)作和延遲動(dòng)作.此外,約束定義只用于時(shí)鐘演算,不參與之后的任務(wù)劃分等步驟.

3.2 時(shí)鐘數(shù)據(jù)依賴圖

SIGNAL程序中的所有信號(hào)變量可具有各自的時(shí)鐘,如果生成串行代碼,即需要確定性的執(zhí)行順序,編譯器基于時(shí)鐘等式和時(shí)鐘等價(jià)類,構(gòu)造出一棵時(shí)鐘樹(shù)(clock hierarchy).能夠構(gòu)造時(shí)鐘樹(shù),代表所有時(shí)鐘都隸屬于一個(gè)全局時(shí)鐘(master clock),即可以給出一個(gè)確定性的串行執(zhí)行順序,在同步語(yǔ)言中,稱其為Endochrony性質(zhì).在同步語(yǔ)言串行代碼生成中,根據(jù)時(shí)鐘等價(jià)類之間的時(shí)鐘蘊(yùn)含關(guān)系構(gòu)建時(shí)鐘樹(shù),基于遍歷時(shí)鐘樹(shù)結(jié)構(gòu),生成串行代碼的控制結(jié)構(gòu),并根據(jù)等式之間的讀寫(xiě)依賴關(guān)系生成執(zhí)行順序,依次填寫(xiě)到對(duì)應(yīng)的控制結(jié)構(gòu)中.而在多線程代碼生成中,需要進(jìn)一步構(gòu)造數(shù)據(jù)依賴圖,從而分析出更多的并行信息.

首先,使用時(shí)鐘等價(jià)類替換對(duì)應(yīng)的所有時(shí)鐘變量以簡(jiǎn)化程序.其次,基于 S-CGA表達(dá)式中的變量間讀寫(xiě)依賴關(guān)系構(gòu)建數(shù)據(jù)依賴圖.例如,對(duì)于衛(wèi)式動(dòng)作γ?x=τ,只有當(dāng)獲得γ和τ中變量的取值后,才可以執(zhí)行該衛(wèi)式動(dòng)作對(duì)x進(jìn)行賦值,此時(shí),γ和τ為讀依賴變量,x為寫(xiě)依賴變量.RdVars/RdActs用于表示讀依賴變量/動(dòng)作集合,WrVars/WrActs用于表示寫(xiě)依賴變量/動(dòng)作集合.

定義2(讀寫(xiě)依賴).設(shè)FV(τ)為表達(dá)式τ中的自由變量的集合.S-CGA等式中的動(dòng)作到變量的依賴定義為

·RdVars(γ?x=τ):=FV(γ)∪FV(τ)

·WrVars(γ?x=τ) :={x}

而變量到動(dòng)作的讀寫(xiě)依賴定義如下.

·RdActs(x):={γ?A|x∈RdVars(γ?A)}

·WrActs(x):={γ?A|x∈WrVars(γ?A)}

MinSIGNAL多線程代碼生成器采用基于周期的目標(biāo)代碼執(zhí)行方式:(1) 初始化程序;(2) 計(jì)算程序體;(3) 更新變量.然后進(jìn)入下一個(gè)周期,迭代執(zhí)行(2)和(3).我們主要分析程序體中的依賴關(guān)系.含有初始時(shí)鐘值init(x?)的立即動(dòng)作主要用于程序初始化,而延遲動(dòng)作用于更新變量,γ?assume(σ)則主要用于定義時(shí)鐘約束關(guān)系,因此,這3類衛(wèi)式動(dòng)作不用于構(gòu)造數(shù)據(jù)依賴圖.

在數(shù)據(jù)依賴圖中,只有當(dāng)一個(gè)動(dòng)作的所有讀變量都有取值時(shí),該動(dòng)作才可以被執(zhí)行.類似地,只有當(dāng)一個(gè)變量的所有寫(xiě)動(dòng)作都已經(jīng)完成計(jì)算后,該變量才能夠有取值.例如,在上述 S-CGA 程序中,ID_4?ID_5=x1依賴于ID_4?readx1獲得的x1值.

定義 3(時(shí)鐘數(shù)據(jù)依賴圖(CDDG)).時(shí)鐘數(shù)據(jù)依賴圖 CDDG 為一個(gè)有向圖〈V,DR〉,V代表衛(wèi)式動(dòng)作集合,DR?V×V代表衛(wèi)式動(dòng)作之間的依賴關(guān)系集合.

時(shí)鐘數(shù)據(jù)依賴圖的構(gòu)造規(guī)則如下.對(duì)任意的動(dòng)作a∈A以及變量x∈RdVars(a),在WrActs(x)對(duì)應(yīng)的衛(wèi)式動(dòng)作到a對(duì)應(yīng)的衛(wèi)式動(dòng)作之間增加一條有向邊.

圖4為Count進(jìn)程對(duì)應(yīng)的S-CGA程序依據(jù)構(gòu)造規(guī)則生成的時(shí)鐘數(shù)據(jù)依賴圖CDDG.

我們使用 S-CGA 程序中的行號(hào)表示對(duì)應(yīng)的衛(wèi)式動(dòng)作,使用不同的形狀區(qū)分衛(wèi)式動(dòng)作.其中,橢圓表示輸入動(dòng)作,矩形表示輸出動(dòng)作,圓形表示立即動(dòng)作.而箭頭→表示依賴關(guān)系,例如,22→23表示ID_4?ID_8=ID_4 andID_7依賴ID_4?ID_7=x2獲得的ID_7值.

3.3 任務(wù)劃分

任務(wù)劃分用于分析CDDG中包含的并行執(zhí)行信息,直接影響目標(biāo)代碼的并行度,是多線程代碼生成器的核心步驟.首先,CDDG是一個(gè)有向圖,根據(jù)拓?fù)渑判蛩枷雽?duì) CDDG進(jìn)行任務(wù)劃分;其次,基于劃分結(jié)果分別提出優(yōu)化算法和基于流水線方式的任務(wù)劃分,其中前者用于處理劃分結(jié)果中可能存在丟失依賴關(guān)系和線程數(shù)目過(guò)多的問(wèn)題,后者用于嘗試尋找劃分中更大的并行度.

3.3.1 基于拓?fù)渑判虻娜蝿?wù)劃分

多線程代碼生成是基于已經(jīng)融合時(shí)鐘關(guān)系的數(shù)據(jù)依賴圖,并需要在數(shù)據(jù)依賴圖中進(jìn)行任務(wù)劃分(partition).CDDG是有向無(wú)環(huán)圖,我們基于拓?fù)渑判蚍椒▽?duì)CDDG進(jìn)行任務(wù)劃分.

劃分算法如圖5所示:算法輸入為時(shí)鐘數(shù)據(jù)依賴圖CDDG,輸出為任務(wù)劃分結(jié)果topoPartition.算法第1步分別對(duì)NodeSet、EdgeSet和topoPartition進(jìn)行初始化(第4行～第6行),然后進(jìn)入拓?fù)渑判騽澐值?第7行).迭代過(guò)程包含以下步驟:首先從 NodeSet中計(jì)算出所有入度為0的點(diǎn)組成的集合Pi,i表示迭代次數(shù)(第8行);其次,如果Pi不為空,則將Pi加入到topoPartition的末尾.如果Pi為空,表明CDDG中存在環(huán),則算法終止,輸出異常信息“CDDG中存在環(huán)”(第9行);最后將Pi中出現(xiàn)的點(diǎn)從NodeSet中移除以及從EdgeSet中移除與這些點(diǎn)有關(guān)的邊(第10行、第11行).當(dāng)NodeSet為空時(shí)迭代終止.

例1對(duì)應(yīng)的CDDG生成劃分結(jié)果topoPartition如下所示.

其中,Pi=id1||id2…||idn為一個(gè)劃分,表示id1,id2,…,idn可以并行執(zhí)行,id代表CDDG中對(duì)應(yīng)節(jié)點(diǎn)的行號(hào).以P1為例,1||2||3||8表示衛(wèi)式動(dòng)作ID_4?ready1,ID_4?readx1,ID_4?readx2和ID_4?C___4=y2==y2彼此可以并行執(zhí)行.Pi;Pi+1表示兩者之間串行執(zhí)行.即當(dāng)Pi中衛(wèi)式動(dòng)作執(zhí)行結(jié)束,開(kāi)始執(zhí)行Pi+1中衛(wèi)式動(dòng)作.

然而,這種劃分方法得到的劃分結(jié)果可能存在以下問(wèn)題.

首先,劃分結(jié)果可能導(dǎo)致在最后代碼生成的線程調(diào)度時(shí),增加多余的同步開(kāi)銷.以P2中衛(wèi)式動(dòng)作ID_4?C___1=x1==x1為例,根據(jù) topoPartition,該衛(wèi)式動(dòng)作開(kāi)始執(zhí)行需要等待P1中所有衛(wèi)式動(dòng)作執(zhí)行結(jié)束.但根據(jù)CDDG可知,ID_4?C___1=x1==x1開(kāi)始執(zhí)行依賴ID_4?readx1執(zhí)行結(jié)束.劃分結(jié)果導(dǎo)致生成的線程之間也存在多余的通信信息,增加了線程之間的同步開(kāi)銷時(shí)間.在實(shí)際執(zhí)行目標(biāo)代碼過(guò)程中,原本可以執(zhí)行的線程必須等待其他額外的線程執(zhí)行結(jié)束才可以開(kāi)始執(zhí)行,從而可能影響目標(biāo)代碼的執(zhí)行效率.

其次,由于使用基于拓?fù)渑判虻膭澐址椒?劃分結(jié)果中的每個(gè)衛(wèi)式動(dòng)作在代碼生成時(shí)將對(duì)應(yīng)轉(zhuǎn)換為一個(gè)線程.以P4中17(對(duì)應(yīng)圖3中ID_6?s1=y1)為例,其轉(zhuǎn)換對(duì)應(yīng)生成的線程的步驟包括:17對(duì)應(yīng)生成線程名Thread_17;衛(wèi)式動(dòng)作轉(zhuǎn)換為線程的計(jì)算部分;該線程開(kāi)始執(zhí)行依賴獲得P3對(duì)應(yīng)的所有線程的執(zhí)行結(jié)束信息;當(dāng)該線程執(zhí)行結(jié)束,則將結(jié)束信息通知P5對(duì)應(yīng)的所有線程.因此,當(dāng)衛(wèi)式動(dòng)作數(shù)目過(guò)多時(shí),導(dǎo)致線程數(shù)目過(guò)多,可能會(huì)增加線程間的資源競(jìng)爭(zhēng),從而影響目標(biāo)程序的執(zhí)行效率.

3.3.2 劃分優(yōu)化

針對(duì)劃分結(jié)果 topoPartition可能存在的問(wèn)題,我們給出基于拓?fù)渑判騽澐值膬?yōu)化算法,即記錄時(shí)鐘數(shù)據(jù)依賴圖CDDG中的依賴關(guān)系以及嘗試減少目標(biāo)線程數(shù)目.

首先,我們給出如下定義.

特別地,當(dāng)WAITS(b)={a},即|WAITS(b)|=1 時(shí),記為WAITS(b)={a}.同樣地,當(dāng)NOTIFYS(a)=時(shí),記為NOTIFYS(a)=.根據(jù)定義4和定義5,遍歷CDDG中依賴關(guān)系計(jì)算出所有衛(wèi)式動(dòng)作對(duì)應(yīng)的等待和通知,并將其加入到優(yōu)化劃分結(jié)果topoOptimization中,從而在topoOptimization中記錄時(shí)鐘依賴圖的依賴關(guān)系.此外,定義4和定義5也便于在后續(xù)步驟中找出可以合并的線程以及處理目標(biāo)代碼中線程之間的同步.

其次,給出嘗試減少目標(biāo)線程數(shù)目的方法.

如果衛(wèi)式動(dòng)作a和b滿足WAIT(b)={a}&&NOTIFY(a)=,則合并a和b為一個(gè)特殊的“衛(wèi)式動(dòng)作”,記為Ma=[a;b],其中,WAITS(Ma)=WAITS(a),NOTIFYS(Ma)=NOTIFYS(b).Ma表示衛(wèi)式動(dòng)作a和b在生成目標(biāo)代碼中將合并為一個(gè)線程.

圖 6給出基于拓?fù)渑判騽澐謨?yōu)化算法.首先,計(jì)算出所有衛(wèi)式動(dòng)作對(duì)應(yīng)的等待和通知并加入到優(yōu)化結(jié)果中(第4行～第6行);其次,在原有并行執(zhí)行部分的基礎(chǔ)上進(jìn)行線程合并(第7行).

我們對(duì)第3.3.1節(jié)給出的劃分結(jié)果進(jìn)行優(yōu)化,得到優(yōu)化劃分結(jié)果topoOptimization如下所示.

其中,劃分P2的[15;16]、[22;23],P4的[17;18]和P6的[26;4]為合并后的衛(wèi)式動(dòng)作.例如,[17;18]表示在目標(biāo)代碼生成時(shí),衛(wèi)式動(dòng)作ID_6?s1=y1和ID_6?x=s1將會(huì)被分配到一個(gè)線程中順序執(zhí)行.同時(shí),等待和通知記錄依賴關(guān)系,例如WAITS(22)={3}表示衛(wèi)式動(dòng)作ID_4?ID_7=x2依賴于輸入動(dòng)作ID_4?readx2得到的x2值.

3.3.3 基于流水線方式的任務(wù)劃分

當(dāng)基于拓?fù)渑判颢@得的任務(wù)劃分存在并行度不高(即大部分Pi中可并行執(zhí)行的衛(wèi)式動(dòng)作數(shù)目都較少)的情況下,我們提出基于流水線方式(pipeline style)對(duì)劃分結(jié)果進(jìn)行再劃分,嘗試提高執(zhí)行并行度.考慮一個(gè)特殊情況為劃分結(jié)果中所有Pi中都只有一個(gè)衛(wèi)式動(dòng)作,則經(jīng)過(guò)任務(wù)劃分生成的多線程代碼執(zhí)行情況實(shí)際上“等同”于串行程序執(zhí)行,而通過(guò)引入流水線方式劃分支持多條流水線并行執(zhí)行,從而提高目標(biāo)程序的執(zhí)行效率.

本文的流水線方式的任務(wù)劃分算法(如圖7所示)包括3個(gè)步驟:首先,根據(jù)劃分結(jié)果定義流水線階段;其次,針對(duì)各流水線階段增加流水線中間變量;最后,針對(duì)不同流水線以及同一流水線下不同流水線階段之間增加通信函數(shù).

(1) 定義流水線階段(算法第4行、第5行)

首先將劃分結(jié)果topoPartition中每個(gè)劃分Pi對(duì)應(yīng)于一個(gè)流水線階段Stage(i).由于topoPartition中并未考慮延遲動(dòng)作γ?next(x)=τ,在確定流水線階段的同時(shí)需要將所有延遲動(dòng)作γ?next(x)=τ加入到相應(yīng)的 Stage中,便于之后處理不同流水線間的通信,并保證不同流水線執(zhí)行結(jié)果的正確性.例如,對(duì)于延遲動(dòng)作ID_4?next(y2)=F___7,將其加入到ID_4?F___7=y1+K___8所在的Stage中.

每個(gè)Stage(i)有兩種不同的狀態(tài):激活狀態(tài)和阻塞狀態(tài).一個(gè)Stage(i)稱為阻塞狀態(tài)當(dāng)且僅當(dāng)該流水線階段中存在需延遲動(dòng)作寫(xiě)入的值未被更新.只有處于激活狀態(tài)的流水線階段才可以被執(zhí)行.在定義流水線階段時(shí),每個(gè)流水線階段默認(rèn)為激活狀態(tài).

(2) 增加流水線中間變量(算法第6行～第9行)

得到流水線階段后,需要考慮如何在每條流水線的各個(gè)流水線階段之間加入流水線中間變量.因?yàn)槊織l流水線的每個(gè)階段同時(shí)處理不同邏輯時(shí)刻的數(shù)據(jù),所以需要一些中間變量來(lái)存儲(chǔ)各個(gè)流水線階段中生成的臨時(shí)結(jié)果.為此,需要確定流水線中間變量在流水線階段中加入的確切位置.

對(duì)Stage(i)中任意的衛(wèi)式動(dòng)作a,如果變量x∈WrVars(a),則在Stage(i)和Stage(i+1)之間,增加變量x對(duì)應(yīng)的流水線中間變量.需要注意的是:一個(gè)流水線中間變量只適用于一條流水線.對(duì)于多條流水線,通過(guò)根據(jù)流水線條數(shù)N將流水線中間變量調(diào)整為一維流水線中間變量數(shù)組,從而保證各條流水線之間不產(chǎn)生數(shù)據(jù)沖突.例如,對(duì)于變量x以及流水線條數(shù)N,需要增加的流水線中間變量數(shù)組為m_x[N],其中,m_x[0]表示第0條流水線中x對(duì)應(yīng)的流水線中間變量.

(3) 增加通信函數(shù)(算法第10行和第13行)

增加流水線中間變量后,需要在流水線中間變量與S-CGA變量之間建立起數(shù)據(jù)通信的映射關(guān)系,包括兩種數(shù)據(jù)通信函數(shù):數(shù)據(jù)輸入函數(shù)inp_exchange,負(fù)責(zé)將流水線中間變量值傳輸?shù)綄?duì)應(yīng)的S-CGA變量;數(shù)據(jù)輸出函數(shù)outp_exchange,負(fù)責(zé)將已經(jīng)更新的S-CGA變量值傳輸?shù)綄?duì)應(yīng)的流水線中間變量中.例如,對(duì)于立即動(dòng)作γ?(x)=τ,對(duì)γ、τ調(diào)用inp_exchange函數(shù),當(dāng)衛(wèi)式動(dòng)作執(zhí)行結(jié)束,調(diào)用outp_exchange函數(shù)更新x.若變量x在某條流水線中需要的流水線中間變量為k個(gè),設(shè)置N條流水線,則對(duì)于變量x來(lái)說(shuō),共需要中間變量為k×N個(gè).

最后,需要考慮不同流水線之間的數(shù)據(jù)延遲通信問(wèn)題.在多條流水線中,S-CGA 程序中延遲動(dòng)作γ?next(x)=τ會(huì)影響相鄰兩條流水線之間的數(shù)據(jù)通信.因此,為了保證基本流水線的正確信息流,對(duì)于那些由延遲動(dòng)作寫(xiě)入的變量(稱為更新值),在每個(gè)流水線中必須保證觸發(fā)一個(gè)動(dòng)作來(lái)完成延遲動(dòng)作.如果當(dāng)前流水線中具有延遲動(dòng)作中的節(jié)點(diǎn)對(duì)應(yīng)的所有衛(wèi)式動(dòng)作的衛(wèi)式都為false,則需要增加一個(gè)衛(wèi)式動(dòng)作來(lái)保存更新值,使之保證:如果當(dāng)前流水線相鄰的下個(gè)流水線中需要使用延遲動(dòng)作中的變量,則這個(gè)變量的值等于前個(gè)流水線中的對(duì)應(yīng)的值.同時(shí)設(shè)置標(biāo)志符update表示當(dāng)前流水線中涉及更新值的階段是否已被更新,update為真,表示更新值已被更新,否則,該階段處于阻塞狀態(tài).假設(shè)更新值的個(gè)數(shù)為t,設(shè)置N條流水線,則一共需要t×(N-1)個(gè)通信函數(shù),在實(shí)際情況下,通信函數(shù)的個(gè)數(shù)可能會(huì)小于上述數(shù)值.因?yàn)閷?duì)于更新前后的值始終不變的更新值,即由源 SIGNAL程序中常量生成的變量,其對(duì)應(yīng)的不同流水線之間的通信函數(shù)可以進(jìn)行優(yōu)化而被去掉.

這里,我們給出針對(duì)第3.3.2節(jié)中topoOptimization進(jìn)行流水線方式的任務(wù)劃分,默認(rèn)采用3條流水線.首先定義流水線階段并添加延遲動(dòng)作,例如 Stage(2)中添加兩個(gè)延遲動(dòng)作(序號(hào) 12和序號(hào) 14);其次定義流水線中間變量,如圖8所示,Stage(1)和Stage(2)之間增加流水線中間變量數(shù)組y1、x1、x2和C__4;最后添加通信函數(shù),包括數(shù)據(jù)通信函數(shù)(outp_exchange/inp_exchange)和延遲通信函數(shù)(f_y2),如圖9所示.

Pipeline1中Stage(4)的更新值y2默認(rèn)由init函數(shù)激活,所以設(shè)置為激活狀態(tài),而Pipeline2和Pipeline3中Stage(4)分別由前一個(gè)Pipeline中的Stage(2)觸發(fā),所以后者設(shè)置為阻塞狀態(tài)(灰色).此外,序號(hào)12和序號(hào)27對(duì)應(yīng)的衛(wèi)式動(dòng)作ID_4?next(K___8)=K___8和ID_4?next(K___9)=K___9是根據(jù)源SIGNAL程序中的常量而生成,可以優(yōu)化其對(duì)應(yīng)的延遲通信函數(shù),因此不需要修改更新值.

3.4 多線程代碼生成

本文將多線程代碼生成過(guò)程分為平臺(tái)相關(guān)和平臺(tái)無(wú)關(guān)兩個(gè)層次:首先,根據(jù)劃分結(jié)果生成基于 Wait/Notify機(jī)制的虛擬多線程VMT(virtual multi-thread)代碼;其次,從虛擬多線程代碼中生成具體的可執(zhí)行多線程代碼,如C或者Java.

3.4.1 虛擬多線程代碼

優(yōu)化劃分中每個(gè)衛(wèi)式動(dòng)作或合并的衛(wèi)式動(dòng)作對(duì)應(yīng)一個(gè)線程,如圖10右側(cè)線程所示,本文采用串行調(diào)度方式來(lái)確保線程間通信保持同步語(yǔ)義,根據(jù)優(yōu)化劃分結(jié)果中WAITS和NOTIFYS信息實(shí)現(xiàn)基于Wait/Notify機(jī)制的虛擬多線程代碼.主函數(shù)首先執(zhí)行初始化(例如,y2=2),然后進(jìn)入主循環(huán),等待所有線程完成執(zhí)行,最后處理延遲賦值操作(更新y2取值).而在主循環(huán)中,每個(gè)線程(thread1,…,thread26)都執(zhí)行一個(gè)循環(huán):等待(wait)輸入、測(cè)試衛(wèi)式、產(chǎn)生輸出、通知(notify)其他線程.

另外,針對(duì)基于流水線方式的任務(wù)劃分結(jié)果生成虛擬多線程結(jié)構(gòu),則需要對(duì)圖10所示結(jié)構(gòu)做出如下調(diào)整.

(1) 保留虛擬多線程的通用結(jié)構(gòu),即初始化、主函數(shù)和線程組.主函數(shù)中的call_threads()函數(shù)修改為call_threads(PN),即在主循環(huán)中調(diào)用PN條流水線下的線程.延遲賦值操作從主函數(shù)轉(zhuǎn)移到特定的線程中,具體線程是根據(jù)流水線階段中延遲動(dòng)作加入的位置加以確定.

(2) 增加數(shù)據(jù)交換和數(shù)據(jù)通信.數(shù)據(jù)交換用于處理單個(gè)流水線中線程與流水線中間變量的數(shù)據(jù)交換.數(shù)據(jù)通信用于處理不同流水線之間線程間的通信.

生成虛擬多線程代碼的目的是方便對(duì)多線程代碼進(jìn)行形式化驗(yàn)證和仿真分析,如使用模型檢測(cè)工具UPPAAL對(duì)多線程代碼的無(wú)死鎖性等性質(zhì)進(jìn)行驗(yàn)證,以及在仿真工具Simulink上進(jìn)行仿真實(shí)驗(yàn).同時(shí),支持生成多種目標(biāo)代碼,增加代碼生成器后端的可擴(kuò)展性.

3.4.2 多線程C代碼

在多線程C代碼自動(dòng)生成過(guò)程中,使用POSIX的同步機(jī)制來(lái)實(shí)現(xiàn)Wait/Notify.首先,所使用的同步結(jié)構(gòu)由互斥量(pthread mutex)、條件變量(pthread condition variable)以及一個(gè)線程所等待事件的數(shù)量(value)組成.例如,thread13需要等待thread1的事件,因此,其value為1.

counter_wait用于表示 Wait機(jī)制,即,當(dāng)前線程的value值大于 0(意味著該線程的一些等待事件還沒(méi)有到達(dá)),則將當(dāng)前線程設(shè)為等待.

counter_notify用于表示Notify機(jī)制,用于喚醒等待線程隊(duì)列中的某個(gè)線程.

以圖 10中虛擬多線程為例,我們給出對(duì)應(yīng)多線程 C代碼中部分線程:thread_15和thread_17,如圖 11所示.thread_15開(kāi)始執(zhí)行需要等待thread_2的事件發(fā)生,即讀取輸入信號(hào)x1.條件語(yǔ)句中順序執(zhí)行語(yǔ)句ID_5=x1和ID_6=ID_4 &&ID_5是根據(jù)劃分結(jié)果 topoOptimization中P2對(duì)應(yīng)的[15;16]生成.當(dāng)完成計(jì)算后,通知線程thread_17,thread_19和thread_21.如果thread_1已經(jīng)執(zhí)行完成,則下一步可以執(zhí)行thread_17.

3.4.3 多線程Java代碼

在生成多線程Java代碼階段,我們使用線程同步柵欄的方式完成線程之間的同步,生成的Java文件主要包括如下兩個(gè)Java類.

(1) 輸入輸出類.對(duì)于 S-CGA中每一個(gè)輸入動(dòng)作,對(duì)應(yīng)生成一個(gè) read方法,每個(gè)輸出動(dòng)作則對(duì)應(yīng)生成一個(gè)write方法.在線程類執(zhí)行前,調(diào)用 read方法讀取輸入數(shù)據(jù),在線程類執(zhí)行結(jié)束后,調(diào)用 write方法寫(xiě)入輸出數(shù)據(jù).通過(guò)單獨(dú)生成輸入輸出類,保證不同任務(wù)劃分算法生成的線程類可以重用輸入輸出類.

(2) 線程類.線程類中包含了若干子類,如classthread_15等.子類實(shí)現(xiàn)了Runnable方法,對(duì)應(yīng)于虛擬多線程中單個(gè)線程.在子類中重寫(xiě)run函數(shù):等待所依賴的事件發(fā)生,執(zhí)行條件語(yǔ)句,通知其他線程.

以圖10中虛擬多線程為例,我們給出對(duì)應(yīng)多線程Java代碼中部分線程:thread_15和thread_17,如圖12所示.首先thread_15調(diào)用Wait方法,進(jìn)入阻塞狀態(tài),當(dāng)所依賴的線程全部執(zhí)行完之后,解除thread_15的阻塞狀態(tài).if語(yǔ)句執(zhí)行結(jié)束后,調(diào)用countDown方法通知其他線程thread_15已執(zhí)行結(jié)束.類似地,如果thread_1已經(jīng)執(zhí)行完成,則下一步可以執(zhí)行thread_17.

4 工具和實(shí)例分析

MinSIGNAL多線程代碼生成器基于OCAML編程實(shí)現(xiàn),代碼生成器采用模塊化思想,包括已有串行代碼生成器前端和擴(kuò)展多線程代碼生成器后端.本節(jié)將主要介紹MinSIGNAL多線程代碼生成器的工具設(shè)計(jì)與實(shí)現(xiàn)以及多線程代碼在多核處理器上的實(shí)驗(yàn)分析.

4.1 工具實(shí)現(xiàn)和分析

多線程代碼生成器的主要編譯步驟及其對(duì)應(yīng)的OCAML代碼數(shù)量統(tǒng)計(jì)見(jiàn)表4.

Table 4 Main steps of MinSIGNAL parallel code generator表4 MinSIGNAL多線程代碼生成器主要步驟

工具開(kāi)發(fā)環(huán)境為基于Eclipse平臺(tái)的OcaIDE插件環(huán)境.如圖13所示,左側(cè)為文檔結(jié)構(gòu),每個(gè)文件對(duì)應(yīng)一個(gè)執(zhí)行功能.我們?cè)趍ain.ml文件中配置MinSIGNAL代碼生成器執(zhí)行步驟,并通過(guò)配置文件設(shè)置同步語(yǔ)言源文件路徑、代碼生成器執(zhí)行文件路徑等參數(shù),運(yùn)行配置文件(如圖14所示),從而生成多線程代碼.

如圖15所示,目標(biāo)程序通過(guò)從輸入信號(hào)對(duì)應(yīng)的文件Input.txt中讀取數(shù)據(jù),執(zhí)行計(jì)算結(jié)束后將輸出信號(hào)保存到文件Output.txt中.

4.2 實(shí)驗(yàn)與分析

本實(shí)驗(yàn)的目的在于通過(guò)實(shí)驗(yàn)分析基于拓?fù)渑判騼?yōu)化算法和基于流水線方式的任務(wù)劃分是否提高目標(biāo)代碼的執(zhí)行效率,以支持比較基于不同劃分方法下自動(dòng)生成的程序的質(zhì)量.我們測(cè)試基于不同劃分算法生成的多線程代碼,具體包括:使用基于拓?fù)渑判騽澐稚傻亩嗑€程代碼(C_1/JAVA_1),以及在拓?fù)渑判騽澐值幕A(chǔ)上分別使用基于優(yōu)化拓?fù)渑判騽澐稚傻亩嗑€程代碼(C_2/JAVA_2)和基于流水線劃分方式的多線程代碼(C_3_i/JAVA_3_i),其中,流水線條數(shù)i分別設(shè)置為 3/4/6/12條.C_1/JAVA_1的運(yùn)行結(jié)果作為基準(zhǔn),用于和后兩種劃分方式進(jìn)行比較.整個(gè)測(cè)試環(huán)境參數(shù)包括操作系統(tǒng)Win10 64bit、8核core i7-6700 CPU 3.40GHz、8G RAM、C編譯環(huán)境Dev_C++(TDM-GCC 4.8.1)和Java編譯環(huán)境Eclipse Oxygen(JDK1.8).

實(shí)驗(yàn)選取3個(gè)SIGNAL測(cè)試程序:測(cè)試程序1為例1中Count程序;測(cè)試程序2為數(shù)學(xué)中冪運(yùn)算計(jì)算程序,輸入兩個(gè)整型(integer)參數(shù)分別是底數(shù)和指數(shù),輸出冪運(yùn)算的結(jié)果;測(cè)試程序 3為模擬采樣,對(duì)輸入的波形(整型值序列),根據(jù)設(shè)置不同的采樣要求(假設(shè)有兩種布爾條件),分別輸出對(duì)應(yīng)的波形.實(shí)驗(yàn)通過(guò)在不同CPU核數(shù)下運(yùn)行不同SIGNAL測(cè)試程序生成的多線程C和Java代碼,計(jì)算其循環(huán)執(zhí)行1 000次的平均執(zhí)行時(shí)間,見(jiàn)表5.

平均執(zhí)行時(shí)間反映多線程代碼執(zhí)行效率.圖16給出表5((1)～(3),共3張表)對(duì)應(yīng)的折線圖,橫軸為CPU核數(shù),縱軸為不同目標(biāo)代碼在給定CPU核數(shù)下的平均執(zhí)行時(shí)間.如圖16所示,在CPU核心數(shù)相同的情況下,基于流水線方式的劃分算法生成的多線程代碼(C/Java)執(zhí)行效率最高,而采用基于拓?fù)渑判騽澐謨?yōu)化算法次之,但仍比基于拓?fù)渑判騽澐炙惴▽?duì)應(yīng)的執(zhí)行效率要高.同時(shí),由圖16可知,在給定任務(wù)劃分算法和CPU核數(shù)的情況下,生成的多線程C程序的執(zhí)行效率高于生成的多線程Java程序.這可能是因?yàn)槎叩亩嗑€程機(jī)制存在差異,C程序直接調(diào)用Windows底層程序,而Java程序是借助于JVM實(shí)現(xiàn)多線程機(jī)制.因此,不同目標(biāo)語(yǔ)言的選取也會(huì)影響多線程代碼自動(dòng)生成方法所生成目標(biāo)程序的執(zhí)行效率.

此外,通過(guò)分析四核CPU和八核CPU下對(duì)應(yīng)的平均執(zhí)行時(shí)間可知,四核CPU對(duì)應(yīng)的執(zhí)行時(shí)間更快,即并不是 CPU核心數(shù)越高,程序執(zhí)行速度越快.這可能是由于隨著 CPU核數(shù)的提升,不同核之間調(diào)度和數(shù)據(jù)交換花費(fèi)的時(shí)間更多,并且Cache訪問(wèn)沖突也會(huì)造成執(zhí)行時(shí)間的增加.因此,在嵌入式系統(tǒng)的設(shè)計(jì)過(guò)程中,在考慮軟件建模的同時(shí),也需要考慮適配硬件平臺(tái),避免造成資源浪費(fèi).

Table 5 Testing results on multi-core platform (1)表5 多核執(zhí)行平臺(tái)下的測(cè)試結(jié)果(1)

Table 5 Testing results on multi-core platform (2)表5 多核執(zhí)行平臺(tái)下的測(cè)試結(jié)果(2)

Table 5 Testing results on multi-core platform (3)表5 多核執(zhí)行平臺(tái)下的測(cè)試結(jié)果(3)

綜上所述,通過(guò)分析基于不同劃分算法生成的多線程 C/Java代碼在多核平臺(tái)上實(shí)驗(yàn)的數(shù)據(jù),可以得出以下結(jié)論.

(1) 基于拓?fù)渑判騼?yōu)化算法和基于流水線方式的任務(wù)劃分算法縮短了目標(biāo)代碼執(zhí)行時(shí)間,其中,流水線劃分算法較為明顯地提高了執(zhí)行速度.

(2) 不同目標(biāo)語(yǔ)言的多線程代碼執(zhí)行速度存在差異,在實(shí)際生成代碼時(shí)需要綜合考慮目標(biāo)語(yǔ)言以及多線程機(jī)制等因素.

(3) 當(dāng)考慮同步模型生成多線程代碼時(shí),需要考慮部署在哪種多核平臺(tái)上,以保證資源的合理利用.

本文基于OCMAL實(shí)現(xiàn)同步語(yǔ)言SIGNAL的多線程代碼自動(dòng)生成工具.在已有SIGNAL編譯器研究工作中:例如,與原有SIGNAL編譯器Polychrony[26]相比,本文的S-CGA能夠支持多種同步語(yǔ)言的集成;文獻(xiàn)[14]主要考慮基于GALS的多線程代碼生成,生成的線程粒度較大,本文主要考慮更細(xì)粒度的線程,以便尋找到更多的并行信息,目前已實(shí)現(xiàn)與體系結(jié)構(gòu)分析和設(shè)計(jì)語(yǔ)言 AADL的混合建模;與文獻(xiàn)[31]相比,該文獻(xiàn)主要考慮同步語(yǔ)言的跨平臺(tái)代碼生成,在任務(wù)劃分中僅使用拓?fù)渑判騽澐炙惴?且時(shí)鐘信息需要后期單獨(dú)增加,相比而言,本文考慮多種劃分算法,優(yōu)化目標(biāo)代碼的執(zhí)行效率.此外,本文的未來(lái)目標(biāo)是基于Coq多線程代碼生成器的驗(yàn)證工作.

5 相關(guān)工作

同步語(yǔ)言的串行代碼生成研究已經(jīng)比較成熟.隨著多核處理器的發(fā)展,同步語(yǔ)言的多線程代碼生成成為研究熱點(diǎn).已有研究大致可以分為如下3類.

· 基于 GALS的多線程代碼生成,即系統(tǒng)由具有不同時(shí)鐘的多個(gè)進(jìn)程組成,而每個(gè)進(jìn)程是單時(shí)鐘的,目前所有同步語(yǔ)言基本都支持此類的多線程代碼生成.

· 基于單進(jìn)程的多線程代碼生成,主要是針對(duì) SIGNAL語(yǔ)言以及其他單時(shí)鐘同步語(yǔ)言的擴(kuò)展,這是由于單個(gè)進(jìn)程中的所有信號(hào)變量也可以具有不同時(shí)鐘.

· 考慮硬件平臺(tái)特性,涉及到多核架構(gòu)或時(shí)間可預(yù)測(cè)處理器的執(zhí)行及程序最壞執(zhí)行時(shí)間分析.

(1) 基于GALS的多線程代碼生成

同步語(yǔ)言支持進(jìn)程間的并發(fā)操作,例如 QUARTZ和 ESTEREL提供同步并發(fā)運(yùn)算符‘||’以支持進(jìn)程間的并發(fā),LUSTRE使用‘;’表示不同節(jié)點(diǎn)的并行執(zhí)行,SIGNAL中不同進(jìn)程間的組合操作‘|’也隱含著并行執(zhí)行[32].同時(shí),在分布式系統(tǒng)上,由于進(jìn)程間通信受到物理載體的影響而產(chǎn)生不可預(yù)測(cè)的延遲[13],導(dǎo)致不同進(jìn)程間的時(shí)鐘可能不滿足同步關(guān)系,被稱為全局異步局部同步GALS系統(tǒng).

文獻(xiàn)[14]提出一種非侵入式的多線程代碼生成方法,即在不改變已有SINGAL編譯器Polychrony結(jié)構(gòu)的基礎(chǔ)上,利用其串行編譯功能生成多個(gè)獨(dú)立的進(jìn)程,并基于主控函數(shù)完成調(diào)度,實(shí)現(xiàn)進(jìn)程之間的并行執(zhí)行.文獻(xiàn)[15]提出從實(shí)際工業(yè)需求中導(dǎo)出功能行為等價(jià)的Heptagon程序[33](一種類Lustre同步語(yǔ)言)并進(jìn)一步生成多線程代碼.與文獻(xiàn)[14]所提方案類似,首先基于Heptagon編譯器生成多個(gè)串行節(jié)點(diǎn),然后在集成規(guī)約中描述任務(wù)間通信和同步.通過(guò)構(gòu)建節(jié)點(diǎn)間的依賴圖,利用串行調(diào)度來(lái)保證確定性并發(fā)語(yǔ)義.除功能需求外,該研究還考慮了非功能性需求(如周期等實(shí)時(shí)性質(zhì))的代碼生成.

此外,文獻(xiàn)[34]提出從高層建模語(yǔ)言(AADL,SysML,SystemC等)轉(zhuǎn)換為SIGNAL同步程序并進(jìn)一步生成多線程代碼的方法.其中,同步程序基于Weekly Endochronous理論[35]:即程序中允許多個(gè)根時(shí)鐘.在多線程生成過(guò)程中,采用符號(hào)化原子表達(dá)式和合并分支條件的策略約減線程數(shù)目.不過(guò),其同步程序中僅考慮有限的數(shù)據(jù)類型(事件、布爾和枚舉類型)和布爾操作(相等和取反操作).

多個(gè)進(jìn)程之間并行劃分的“粒度”相對(duì)較大[14],但在同步語(yǔ)言模型中,單個(gè)進(jìn)程內(nèi)部也往往存在潛在的并行執(zhí)行信息.尤其是可以自然表達(dá)分布式系統(tǒng)的SIGNAL語(yǔ)言,其語(yǔ)法的基本結(jié)構(gòu)中包含多時(shí)鐘操作,可以比較自然地支持在進(jìn)程內(nèi)部描述并行執(zhí)行操作.

(2) 基于單進(jìn)程的多線程代碼生成

文獻(xiàn)[26]中介紹了同步語(yǔ)言SIGNAL編譯器Polychrony中的代碼生成策略,在多線程生成方面分為靜態(tài)調(diào)度和動(dòng)態(tài)調(diào)度.靜態(tài)調(diào)度下的分簇(多線程)代碼生成:將生成的代碼劃分到簇中來(lái)模擬調(diào)度圖的結(jié)構(gòu).分簇的原則是:將調(diào)度圖劃分為對(duì)那些依賴于完全相同的輸入集合進(jìn)行計(jì)算.只要一個(gè)簇的所有輸入都有確定值,那么這個(gè)簇就可以被自動(dòng)執(zhí)行,一個(gè)簇的時(shí)鐘取決于簇中所有信號(hào)在時(shí)鐘樹(shù)上的公共父節(jié)點(diǎn).動(dòng)態(tài)調(diào)度下的分簇(多線程)代碼生成:按任務(wù)實(shí)現(xiàn)分簇,并生成任務(wù)之間的同步信息.任務(wù)由簇來(lái)生成,主要思想是使用信號(hào)量的方式并行執(zhí)行各個(gè)任務(wù).然而,這種方式下生成的多線程數(shù)目太多,并且使用特定的線程庫(kù)來(lái)生成仿真代碼.

文獻(xiàn)[29,30]是對(duì)純同步語(yǔ)言 Quartz編譯過(guò)程的多線程代碼的研究.文獻(xiàn)[29]提出同步衛(wèi)式動(dòng)作(clocked guarded action,簡(jiǎn)稱CGA)到基于OpenMP的多線程C程序的編譯方案.作者提出“垂直劃分”的概念,即從數(shù)據(jù)依賴圖中抽取出獨(dú)立的線程,并生成對(duì)應(yīng)的 C代碼.文獻(xiàn)[30]引入軟件流水線的概念,提到的軟件流水線方法包含:分析衛(wèi)式動(dòng)作之間的依賴關(guān)系、創(chuàng)建流水線變量存儲(chǔ)各階段之間的中間結(jié)果以及衛(wèi)式動(dòng)作到流水線之間的轉(zhuǎn)換.這種方法被稱為“水平劃分”.

文獻(xiàn)[31]對(duì) SIGNAL多線程代碼生成進(jìn)行了研究,提出基于方程依賴圖(equation dependency graph,簡(jiǎn)稱EDG)的OpenMP并行代碼生成方法.其中的并行代碼生成算法主要是對(duì)數(shù)據(jù)依賴圖進(jìn)行拓?fù)渑判?生成多個(gè)鏈表:多個(gè)鏈表之間順序執(zhí)行、單個(gè)鏈表內(nèi)部節(jié)點(diǎn)并行執(zhí)行.不過(guò),文獻(xiàn)[31]使用拓?fù)渑判蜃鳛槿蝿?wù)劃分算法,沒(méi)有考慮優(yōu)化工作,而且需要在劃分之后對(duì)劃分結(jié)果單獨(dú)加入時(shí)鐘信息.而本文使用的CDDG中包含時(shí)鐘依賴關(guān)系,即在劃分過(guò)程中已經(jīng)考慮時(shí)鐘信息.

本文主要考慮單進(jìn)程的多線程代碼生成方法,同時(shí)給出優(yōu)化策略和流水線方式的任務(wù)劃分方法,能夠較好地約減線程數(shù)目以及提高目標(biāo)多線程代碼執(zhí)行效率.

(3) 多核架構(gòu)執(zhí)行及WCET分析

ITEA 3計(jì)劃中的(affordable safe & secure mobility evolution,簡(jiǎn)稱ASSUME)項(xiàng)目[15,36]提出一種用于在多核/眾核架構(gòu)上提供可信的嵌入式軟件工程方法,包括從LUSTRE同步模型到自動(dòng)生成并行代碼并在多核/眾核平臺(tái)上執(zhí)行.ASSUME項(xiàng)目擴(kuò)展了SCADE工具的KCG編譯器,以支持生成面向MPPA眾核架構(gòu)[37]的并行代碼,但是當(dāng)前的并行信息是通過(guò)用戶來(lái)驅(qū)動(dòng)的,即用戶指定程序中并行執(zhí)行區(qū)域.此外,在代碼生成過(guò)程中提供每個(gè)任務(wù)在實(shí)時(shí)調(diào)度期間所需的屬性(如WCET、內(nèi)存訪問(wèn)的最壞次數(shù)等).

法國(guó)國(guó)家航天航空研究中心ONERA的SchedMCore環(huán)境[38,39]為形式化多處理器調(diào)度分析和實(shí)驗(yàn)性多核運(yùn)行時(shí)基礎(chǔ)架構(gòu)提供了一套驗(yàn)證和執(zhí)行工具.SchedMCore將同步語(yǔ)言Prelude[40]編譯生成一組相互通信的周期任務(wù)(包含信息有:任務(wù)的周期、WCET、首次到達(dá)時(shí)間和 Deadline),并基于工具自帶的不同多核調(diào)度策略實(shí)現(xiàn)任務(wù)在多核架構(gòu)上的調(diào)度.文獻(xiàn)[41]中給出一個(gè)基于 SchedMCore設(shè)計(jì)并運(yùn)行在多核/眾核架構(gòu)上的航空經(jīng)度控制器案例.

德國(guó)Kaiserslautern工業(yè)大學(xué)嵌入式系統(tǒng)小組(http://es.cs.uni-kl.de/)基于同步語(yǔ)言QUARTZ開(kāi)發(fā)了一個(gè)用于并行嵌入式系統(tǒng)的規(guī)約、驗(yàn)證和實(shí)現(xiàn)的框架AVEREST(http://www.averest.org/).該框架可同時(shí)生成硬件電路邏輯代碼和多線程代碼,并且支持軟硬件分析[42].此外,他們還研究了基于指令集并行(instruction level parallelism,簡(jiǎn)稱 ILP)的同步語(yǔ)言 SCAD 最優(yōu)化代碼生成,包括使用回答集編程(answer set programming,簡(jiǎn)稱ASP)處理 SCAD代碼生成過(guò)程中的最優(yōu)資源/時(shí)間約束調(diào)度問(wèn)題[43],以及利用 SMT求解器生成實(shí)現(xiàn)最大化指令級(jí)并行(給定處理器單元數(shù)目)的最優(yōu)化代碼[44]等.

綜上所述,同步語(yǔ)言多線程代碼生成涉及到多核硬件執(zhí)行平臺(tái)以及考慮WCET分析.我們?cè)谝延泄ぷ鱗18]中給出在同步語(yǔ)言代碼生成過(guò)程中的時(shí)間可預(yù)測(cè)多核體系結(jié)構(gòu)模型及軟硬件映射方法.而本文主要側(cè)重同步語(yǔ)言多線程代碼生成方法及其實(shí)現(xiàn),提出任務(wù)劃分優(yōu)化策略以及基于流水線方式的劃分以提高目標(biāo)代碼的執(zhí)行速度.

6 總結(jié)與展望

同步語(yǔ)言廣泛用于安全關(guān)鍵嵌入式系統(tǒng)建模與驗(yàn)證,近年來(lái),同步語(yǔ)言的多線程代碼生成成為學(xué)術(shù)界的一個(gè)研究熱點(diǎn).本文提出一種基于OCAML的同步語(yǔ)言SIGNAL多線程代碼生成方法和工具.首先將SIGNAL程序轉(zhuǎn)換為經(jīng)過(guò)時(shí)鐘演算的 S-CGA中間程序;之后將S-CGA中間程序轉(zhuǎn)換為時(shí)鐘數(shù)據(jù)依賴圖以分析依賴關(guān)系;然后對(duì)時(shí)鐘數(shù)據(jù)依賴圖進(jìn)行拓?fù)渑判騽澐?并針對(duì)劃分結(jié)果提出優(yōu)化算法和基于流水線方式的任務(wù)劃分方法;最后將劃分結(jié)果轉(zhuǎn)換為虛擬多線程結(jié)構(gòu),然后進(jìn)一步生成可執(zhí)行多線程 C/Java代碼.通過(guò)在多核處理器上的實(shí)驗(yàn)驗(yàn)證了本文提出方法的有效性.

編譯器的形式化驗(yàn)證是一項(xiàng)重要工作,例如:CompCert編譯器(C編譯器)[45]、清華大學(xué)L2C項(xiàng)目(LUSTRE編譯器)[27,28]以及Vélus編譯器(LUSTRE編譯器)[46].我們已經(jīng)給出SIGNAL多線程代碼生成器前端的語(yǔ)義保持證明,下一步工作將基于Coq完成代碼生成器后端的語(yǔ)義保持證明.其次,擴(kuò)展同步語(yǔ)言以支持描述實(shí)時(shí)性質(zhì),以及考慮在時(shí)間可預(yù)測(cè)多核處理器(如 Patmos[47])上執(zhí)行多線程代碼并進(jìn)行 WCET分析也是未來(lái)一項(xiàng)重要工作;最后,針對(duì)復(fù)雜嵌入式系統(tǒng),我們正在開(kāi)展嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言 AADL(描述系統(tǒng)架構(gòu))[48]和同步語(yǔ)言(描述AADL單構(gòu)件內(nèi)的功能)的混合建模方法研究.

致謝感謝匿名評(píng)審專家給予的寶貴意見(jiàn).另外,感謝法國(guó)法國(guó)國(guó)家信息與自動(dòng)化研究所(INRIA)Jean-Pierre Talpin教授給予了很多重要的建議.