安 鑫，夏近偉，楊海嬌，歐陽一鳴，任福繼

（1.合肥工業(yè)大學(xué)計(jì)算機(jī)與信息學(xué)院，合肥 230601；2.情感計(jì)算與先進(jìn)智能機(jī)器安徽省重點(diǎn)實(shí)驗(yàn)室（合肥工業(yè)大學(xué)），合肥 230601）

（?通信作者電子郵箱xin.an@hfut.edu.cn）

0 引言

異構(gòu)多核處理器（Heterogeneous Multi-Core Processor，HMP）現(xiàn)今已被廣泛應(yīng)用于嵌入式系統(tǒng)以及云計(jì)算等多種領(lǐng)域。這種處理器除了具有傳統(tǒng)同構(gòu)多核處理器的并行性特征以外，還可以根據(jù)應(yīng)用的不同類型和需求選擇使用最合適的處理核，從而進(jìn)一步優(yōu)化系統(tǒng)對高性能和低功耗的需求。此外，當(dāng)今的異構(gòu)多核處理器通常配備了動態(tài)電壓和頻率調(diào)整（Dynamic Voltage and Frequency Scaling，DVFS）技術(shù)，這是由于現(xiàn)代處理器的功耗與處理核的頻率及其執(zhí)行的任務(wù)的行為密切相關(guān)［1］，允許系統(tǒng)根據(jù)其運(yùn)行狀態(tài)（如負(fù)載情況）來動態(tài)調(diào)整處理器平臺的電壓和/或頻率可以進(jìn)一步在提高性能和降低功耗之間進(jìn)行權(quán)衡。ARM（Advanced RISC Machines）處理器的big.LITTLE 架構(gòu)就是這樣一種典型的異構(gòu)多核系統(tǒng)，可以將不同類型的處理核組織為不同的簇，并以處理核簇為單位進(jìn)行DVFS控制［2］。

現(xiàn)在典型的異構(gòu)多核系統(tǒng)往往需要在并行運(yùn)行多個應(yīng)用的同時滿足每個應(yīng)用的性能和服務(wù)質(zhì)量等方面的需求。而一些復(fù)雜應(yīng)用還可以以多線程的方式被執(zhí)行，從而可以被映射到多個不同的處理核上并行運(yùn)行以達(dá)到提高性能、降低單個處理器核功耗過大等目的。

因此，要充分發(fā)揮異構(gòu)多核系統(tǒng)在提高性能和降低功耗等方面的潛能，需要解決的很重要的一個問題就是異構(gòu)多核系統(tǒng)的資源管理問題，也就是如何根據(jù)系統(tǒng)運(yùn)行狀態(tài)動態(tài)地為應(yīng)用分配執(zhí)行資源從而滿足系統(tǒng)性能、功耗等方面的需求［3-4］。然而隨著異構(gòu)多核系統(tǒng)中資源數(shù)目和種類的不斷增加，其資源管理部件的設(shè)計(jì)也變得越來越復(fù)雜。設(shè)計(jì)人員往往面臨著一個（非常）大的選擇空間（例如應(yīng)用劃分的線程數(shù)、使用的處理核類型和數(shù)量等），為了提高效率，現(xiàn)有的在線資源管理方法大部分采用啟發(fā)式的方法來對選擇空間進(jìn)行評估和搜索［5-9］。然而這些方法對所設(shè)計(jì)的系統(tǒng)資源管理部件均缺少可靠性的支持，對于那些對可靠性要求比較高的場景，這類方法往往不被采用。鑒于此，一些形式化的方法和技術(shù)（比如模型檢測）被提出［10-11］，然而形式化的方法雖然可以確?？煽啃?，卻往往需要經(jīng)歷一個對設(shè)計(jì)方案進(jìn)行手動建模和編碼，當(dāng)出錯時定位錯誤再進(jìn)行修正直至不再出錯為止的一個迭代過程。隨著問題規(guī)模的變大，相對于這類方法，能夠自動化進(jìn)行設(shè)計(jì)方案生成的方法無疑更加可取。

本文提出了一種基于離散控制器合成（Discrete Controller Synthesis，DCS）技術(shù)的通用模型和方法來解決異構(gòu)多核系統(tǒng)的在線資源管理問題，該方法將離線分析和在線資源分配結(jié)合，通過有限狀態(tài)自動機(jī)（Finite State Automaton，F(xiàn)SA）模型對系統(tǒng)進(jìn)行建模描述，并使用離散控制器合成（DCS）技術(shù)自動生成無需形式化驗(yàn)證的控制部件代碼。相比文中提及的其他基于形式化的資源管理方法，該方法的特點(diǎn)是可以使設(shè)計(jì)者僅需通過描述系統(tǒng)行為模型及其需要滿足的控制目標(biāo)便可以使用現(xiàn)有的合成工具和算法來進(jìn)行自動的設(shè)計(jì)空間探索從而合成一個正確可靠的、滿足系統(tǒng)控制目標(biāo)的控制部件。

本文的主要工作有以下兩點(diǎn)：

1）將異構(gòu)多核系統(tǒng)的資源管理問題分解為硬件執(zhí)行平臺行為、應(yīng)用資源分配行為和資源管理策略/目標(biāo)三部分，并將其建模為一個可以根據(jù)管理目標(biāo)對應(yīng)用的資源分配和執(zhí)行平臺的DVFS等級進(jìn)行管理控制的離散控制問題。

2）采用現(xiàn)有的離散控制器合成技術(shù)和工具對示例異構(gòu)多核系統(tǒng)的資源管理部件進(jìn)行了自動、可靠的生成和模擬驗(yàn)證，并對所采用技術(shù)的可擴(kuò)展性進(jìn)行了評估。

1 相關(guān)工作

目前大多數(shù)涉及多核系統(tǒng)資源管理的研究都是針對應(yīng)用任務(wù)在多核系統(tǒng)上的動態(tài)調(diào)度問題。由于需要在線進(jìn)行調(diào)度，這些方法大部分采用啟發(fā)式的方法來產(chǎn)生一個快速、高效的解決方案［4-9，12］。然而這些方法大都針對事先未知的情況或狀態(tài)，通常只是通過模擬驗(yàn)證來評估方案的一般性能，而無法確保解決方案達(dá)到最優(yōu)或者嚴(yán)格滿足可靠性需求。

近些年來，基于機(jī)器學(xué)習(xí)技術(shù)進(jìn)行性能預(yù)測和動態(tài)調(diào)度的方法引起了越來越多的關(guān)注并取得了良好效果。這類工作主要可以分為兩類：一類是使用機(jī)器學(xué)習(xí)技術(shù)預(yù)測不同調(diào)度方案的性能或功耗［13-16］，然后在此基礎(chǔ)上再結(jié)合某種搜索策略選來擇調(diào)度方案；另一類則是針對調(diào)度目標(biāo)和系統(tǒng)狀態(tài)對調(diào)度方案進(jìn)行學(xué)習(xí)來獲得調(diào)度模型用于預(yù)測符合條件的調(diào)度方案［17-20］。然而，基于機(jī)器學(xué)習(xí)的方法同樣面臨著無法提供嚴(yán)格的可靠性保證的問題，往往通過模擬以一定概率來確保目標(biāo)達(dá)成。

相對于以上兩類基于模擬來進(jìn)行設(shè)計(jì)可靠性驗(yàn)證的方法，用基于形式化的方法（比如模型檢測）來解決多核系統(tǒng)的資源調(diào)度或分配問題顯然更有吸引力，特別是針對那些對可靠性要求比較高的場景。在文獻(xiàn)［10］中，作者提出了一種基于遺傳算法改進(jìn)的靜態(tài)任務(wù)映射算法來解決云環(huán)境下靜態(tài)任務(wù)調(diào)度問題。為了驗(yàn)證其設(shè)計(jì)的可靠性，作者通過建立形式化標(biāo)簽傳遞系統(tǒng)（Labeled Transition System，LTS）模型，并采用模型檢查工具NuSMV 和PAT 進(jìn)行了驗(yàn)證。文獻(xiàn)［11］采用了具有時間拓展的狀態(tài)機(jī)對周期性的實(shí)時任務(wù)進(jìn)行系統(tǒng)建模，然后采用模型檢測方法對硬實(shí)時系統(tǒng)的調(diào)度可行性進(jìn)行了分析。這類方法為了采用基于模型檢測的方法來對設(shè)計(jì)進(jìn)行驗(yàn)證，往往需要在已經(jīng)實(shí)現(xiàn)算法編碼的基礎(chǔ)上對設(shè)計(jì)方案進(jìn)行手動建模并形式化驗(yàn)證，當(dāng)出錯時進(jìn)行錯誤定位并再進(jìn)行修正直至不再出現(xiàn)未知的迭代過程，這個過程往往是枯燥費(fèi)時的。并且隨著問題規(guī)模的變大，其工作量將更加艱巨。

與本文更接近的是采用控制理論及其方法和技術(shù)來設(shè)計(jì)系統(tǒng)資源控制器部件的一些工作。在這類方法中，設(shè)計(jì)者能夠以系統(tǒng)化的方式對已知的知識和預(yù)期進(jìn)行量化，從而產(chǎn)生一個符合設(shè)計(jì)目標(biāo)的控制器。這方面的工作可以根據(jù)控制系統(tǒng)特征分為兩類：一類是在結(jié)構(gòu)上采用單輸入單輸出（Single-Input Single-Output，SISO）控制系統(tǒng)［21-24］，并在系統(tǒng)內(nèi)部采用某種控制技術(shù)（如PID（Proportion-Integral-Derivative）控制）來實(shí)現(xiàn)對某一個系統(tǒng)參數(shù)的控制；另一類則是在SISO 控制系統(tǒng)的基礎(chǔ)上考慮多控制目標(biāo)的協(xié)同，使用多輸入多輸出（Multiple-Input Multiple-Output，MIMO）系統(tǒng)［25］。文獻(xiàn)［26］總結(jié)和比較了當(dāng)前主流的多核系統(tǒng)資源管理方法，并提出了一種將啟發(fā)式算法和監(jiān)督控制理論相結(jié)合的多核系統(tǒng)資源管理框架。

相比以上的動態(tài)資源管理方法，使用離散控制器合成技術(shù)的自動化設(shè)計(jì)方法無疑更加合適，特別是針對高可靠性要求的場景。該方法的主要優(yōu)勢在于：1）提供了形式化的可靠性保證；2）提出的控制器可以在設(shè)計(jì)時由DCS工具自動生成，用戶無需關(guān)注和理解控制理論細(xì)節(jié)。據(jù)調(diào)研所知，目前還沒有使用離散控制器合成技術(shù)來自動生成用于異構(gòu)多核系統(tǒng)的可靠資源管理部件的相關(guān)工作。在文獻(xiàn)［27］的工作中已經(jīng)成功地使用基于DCS 的方法來處理現(xiàn)場可編程門陣列（Field-Programmable Gate Array，F(xiàn)PGA）系統(tǒng)上的可重配置資源的管理問題，本文針對異構(gòu)多核處理器平臺，并將平臺的DVFS 特性及其管理作為一個設(shè)計(jì)因素。

2 建模方法和離散控制器合成技術(shù)

本文采用離散控制器合成技術(shù)（DCS）來解決異構(gòu)多核系統(tǒng)的資源管理問題，在介紹DCS之前，本部分首先介紹對問題進(jìn)行形式化描述的有限狀態(tài)自動機(jī)（FSA）模型。

2.1 有限狀態(tài)自動機(jī)

本文采用文獻(xiàn)［28-29］中定義的自動機(jī)來對系統(tǒng)進(jìn)行建模。

定義1一個有限狀態(tài)自動機(jī)可以描述為一個元組：

其中：Q是一個有限的狀態(tài)集；q0∈Q是S的初始狀態(tài)；I是一個有限的輸入事件集；O是一個有限的輸出事件集；T是一個變遷關(guān)系集合，它是Q×Bool(I) ×O*×Q的子集，其中Bool(I)是I的布爾表達(dá)式集合，O*是O的冪集。

將兩個并行的自動機(jī)進(jìn)行組合的操作稱之為同步合成（synchronous composition），由“‖”表示。給定兩個自動機(jī)：，i=1，2，Q1∩Q2=?。它們的合成定義如下：

式中：

合成狀態(tài)(q1，q2)被稱為宏?duì)顟B(tài)，其中q1和q2是其兩個分狀態(tài)。

封裝操作［28］用于對組合到一起的兩個自動機(jī)進(jìn)行同步，它通過一個定義到兩個自動機(jī)上的同步變量來達(dá)到這個目的，并且這個同步變量需要在其中一個狀態(tài)機(jī)中作為輸入，而在另一個自動機(jī)作為輸出。設(shè)為一個自動機(jī)，Γ?I∪O為S的輸入和輸出變量的集合，那么Γ對于S的封裝就可以定義為：

式中T'定義為：

其中：g+是單項(xiàng)式g中作為正元素出現(xiàn)的變量集，即g+={x∈g|(x∧g)=g}；g-是在單項(xiàng)式g中以負(fù)數(shù)形式出現(xiàn)的一組變量，即g-={x∈g|?(x∧g)=g}。圖1 給出了一個使用變量b封裝來使兩個自動機(jī)A和B強(qiáng)制同步的例子。

此外，還可以在自動機(jī)的狀態(tài)上定義權(quán)重來表示與狀態(tài)相關(guān)的數(shù)值信息。為此，可以通過定義一個代價函數(shù)C：Q→N+將自動機(jī)的每個狀態(tài)映射到一個正整數(shù)。在此基礎(chǔ)上，可以進(jìn)一步為自動機(jī)的路徑定義權(quán)重，例如，路徑p的權(quán)重可以定義為其所經(jīng)過的所有狀態(tài)的權(quán)重總和。當(dāng)合成自動機(jī)時，全局狀態(tài)或者路徑的權(quán)重值則可以被定義為構(gòu)成全局狀態(tài)或路徑的所有局部狀態(tài)權(quán)值的和或最大/最小值。

圖1 使用封裝同步兩個自動機(jī)的例子Fig.1 An example of synchronization of two automata by encapsulation

給定一個使用以上自動機(jī)模型所描述的系統(tǒng)后，就可以應(yīng)用一些形式化的分析和驗(yàn)證技術(shù)，下面介紹本文所采用的離散控制器合成技術(shù)。

2.2 離散控制器合成

離散控制器合成（DCS）［30］于20 世紀(jì)80 年代被提出，用于解決離散事件系統(tǒng)的控制與協(xié)同問題。離散事件系統(tǒng)（Discrete Event System，DES）［31］是一個由離散狀態(tài)構(gòu)成、事件驅(qū)動的動態(tài)系統(tǒng)，這些離散事件發(fā)生的時機(jī)可以是隨機(jī)的、沒有固定的時間間隔。例如，事件可能是系統(tǒng)中某個應(yīng)用的調(diào)用或完成，亦或者是處理器發(fā)生的某個故障。這類系統(tǒng)出現(xiàn)在我們?nèi)粘Ｉ畹母鱾€領(lǐng)域，如制造業(yè)、運(yùn)輸、汽車、嵌入式系統(tǒng)和醫(yī)療保健等。這些系統(tǒng)都有自己的設(shè)計(jì)需求，并需要在運(yùn)行中進(jìn)行相應(yīng)的管理和控制來確保系統(tǒng)能夠正確可靠地運(yùn)行。

DCS 理論的主要優(yōu)點(diǎn)是將目標(biāo)離散事件系統(tǒng)（DES）與反饋控制分離開來，并允許針對給定的特定控制目標(biāo)對目標(biāo)系統(tǒng)進(jìn)行自動化的、可靠的分析和控制。DCS 是一種可以應(yīng)用于離散事件系統(tǒng)（比如通過2.1 節(jié)的自動機(jī)等模型進(jìn)行描述的系統(tǒng)）的操作。為了能夠?qū)δ繕?biāo)離散事件系統(tǒng)（DES）進(jìn)行控制，也就是控制DES系統(tǒng)運(yùn)行行為的演化或變化，需要為這類系統(tǒng)定義可控制的事件。因此，DES 的事件集合Y可以被劃分為兩個子集：Yuc和Yc，分別表示不可控制的事件集和可控制的事件集。圖2 展示了DCS 的工作原理，DCS 的使用需要結(jié)合一個給定的控制目標(biāo)：也就是由控制器去遵循實(shí)施、從而讓被控系統(tǒng)滿足的目標(biāo)，控制目標(biāo)一般通過系統(tǒng)的輸出（狀態(tài)）X表示。給定系統(tǒng)模型S 和控制目標(biāo)后，控制器C 就可以通過相應(yīng)的綜合算法自動得到?？刂破骶C合算法的基本原理與模型檢測技術(shù)類似，它通過遍歷系統(tǒng)的狀態(tài)空間來自動計(jì)算對可控變量Yc的約束（即控制器，可以看作是輸出X和不可控輸入Yuc的函數(shù)），從而控制系統(tǒng)的狀態(tài)轉(zhuǎn)移使其總是滿足給定控制目標(biāo)。

當(dāng)然，可能存在有多個控制器均可以使系統(tǒng)滿足同樣控制目標(biāo)的情況。在極端情況下，控制器可以禁止任何狀態(tài)轉(zhuǎn)換從而避免系統(tǒng)進(jìn)入不合法的狀態(tài)，但這顯然是不可取的。用戶往往對最大允許的控制器感興趣，也就是能夠保留原始不受控制系統(tǒng)中的最大可能正確行為集的控制器，本文所采用的合成算法和工具就是基于這個原則?？傮w而言，DCS 的優(yōu)勢體現(xiàn)在：可以進(jìn)行高層的控制策略描述和聲明，自動可靠地合成滿足控制目標(biāo)的控制器，以及在所有可能正確行為中進(jìn)行最優(yōu)化。相對于其他形式的驗(yàn)證技術(shù)（如模型檢測），DCS 面臨同樣的可擴(kuò)展性問題。然而，DCS 更有建設(shè)性，也就是能夠自動產(chǎn)生一個正確的解決方案，而不需要像模型檢測一樣需要一個可能易錯的手工編碼階段，然后再進(jìn)行冗長的驗(yàn)證［32］。

圖2 離散控制器合成的工作原理Fig.2 Principle of discrete controller synthesis

本文主要使用兩類不同合成算法相對應(yīng)的DCS操作來合成控制器［33］：一類是確保系統(tǒng)始終處于狀態(tài)空間中的一個子集中（即始終處于安全狀態(tài)中）；另一類是控制系統(tǒng)根據(jù)系統(tǒng)狀態(tài)所關(guān)聯(lián)的開銷進(jìn)行單步最優(yōu)的演化，也就是讓系統(tǒng)在進(jìn)行狀態(tài)轉(zhuǎn)換時選擇可達(dá)系統(tǒng)中相應(yīng)開銷最小或最大的那個狀態(tài)。這兩類操作已在DCS工具BZR［31］和ReaX［33］中實(shí)現(xiàn)，它們可以使用2.1 節(jié)介紹的自動機(jī)形式來描述系統(tǒng)行為，并使用一個專用的結(jié)構(gòu)（稱之為合約contract）來描述系統(tǒng)所要滿足的控制目標(biāo)，最后BZR的編譯過程就可以自動調(diào)用ReaX工具中的算法來合成一個正確的控制器（以C 或者Java 源代碼的形式從而可以方便地在實(shí)際系統(tǒng)中部署使用）。

3 基于DCS的異構(gòu)多核系統(tǒng)資源管理方法

首先通過一個示例系統(tǒng)描述了本文所針對的異構(gòu)多核系統(tǒng)的資源管理問題，然后介紹如何通過第2 章介紹的自動機(jī)和DCS 技術(shù)來將該問題建模為一個DCS 問題，最后介紹了如何使用現(xiàn)有的DCS工具BZR來對該模型進(jìn)行代碼描述。

3.1 問題描述

本文從硬件執(zhí)行平臺、系統(tǒng)應(yīng)用及其資源分配、資源分配目標(biāo)三個方面描述所針對的異構(gòu)多核系統(tǒng)的資源管理問題。

3.1.1 硬件執(zhí)行平臺

考慮一個由若干個簇構(gòu)成的異構(gòu)多核平臺，每個簇由若干個（架構(gòu)）相同的處理核構(gòu)成。圖3 給出了一個這樣一個例子，它包含兩個處理核簇（大核簇和小核簇）和一個共享存儲器MEM，每個簇包含兩個相應(yīng)的大或者小處理核，每個處理核具有獨(dú)立的L1 緩存以及簇內(nèi)共享的L2 緩存?？紤]到節(jié)約能耗，每個簇在不用的時候都可以設(shè)置為睡眠模式，并且每個簇上的處理核在使用時均具有統(tǒng)一調(diào)節(jié)簇內(nèi)的電壓和頻率（DVFS）等級的能力來達(dá)到降低功耗或者提升執(zhí)行性能的目的。

另外，本文假設(shè)系統(tǒng)平臺是電池供電的，對于這類系統(tǒng)，用戶往往希望系統(tǒng)能夠根據(jù)電池電量狀態(tài)的變化來調(diào)整所運(yùn)行應(yīng)用的模式和服務(wù)質(zhì)量。

3.1.2 系統(tǒng)應(yīng)用及其資源分配

典型的異構(gòu)多核系統(tǒng)往往需要在多核系統(tǒng)平臺上同時運(yùn)行多個應(yīng)用，并同時滿足每個應(yīng)用的性能等方面的需求。而這些應(yīng)用往往又是多線程的，從而具有充分利用多個處理核來提高其性能的潛力。另外需要指出的是，為了確保應(yīng)用執(zhí)行的可預(yù)測性和系統(tǒng)穩(wěn)定，同大部分異構(gòu)多核系統(tǒng)的資源管理和調(diào)度研究［13，34］一樣，本文約定每個處理核在同一時刻只能執(zhí)行一個線程。

圖3 平臺架構(gòu)Fig.3 Architecture of platform

在本文的研究方案中，假定每個應(yīng)用的執(zhí)行過程中有如下的控制點(diǎn)（事件）。

1）被請求：應(yīng)用請求被執(zhí)行。

2）被執(zhí)行：應(yīng)用被調(diào)度到執(zhí)行資源上開始執(zhí)行。

3）執(zhí)行結(jié)束：應(yīng)用執(zhí)行完畢后發(fā)出結(jié)束通知。

在這些控制事件中的請求和結(jié)束事件的發(fā)生時機(jī)是不可控的，而當(dāng)應(yīng)用被執(zhí)行時選擇使用什么的執(zhí)行資源則是由系統(tǒng)資源管理部件依據(jù)系統(tǒng)的管理策略或者目標(biāo)來確定的。

當(dāng)某個應(yīng)用被啟動時，其執(zhí)行可以有多種不同的資源分配方案，而不同的資源分配方案所導(dǎo)致的應(yīng)用性能和功耗也不一樣。圖4 展示了將一個來自PARSEC benchmark 的Blackscholes 應(yīng)用映射到一個包含兩種類型的處理核（大核B和小核L）的異構(gòu)多核架構(gòu)的運(yùn)行情況［34］。圖4 中，橫軸給出了不同的資源分配情況，橫坐標(biāo)中的組數(shù)（1，2，…，8）為所分配處理核資源總數(shù)目，即B和L的和。

圖4 不同資源分配情況下的性能和能耗值Fig.4 Performance and power consumption under different resource distributions

3.1.3 資源分配目標(biāo)

資源分配目標(biāo)定義了進(jìn)行資源管理和分配時需要實(shí)現(xiàn)的需求，下面給出本文所考慮的異構(gòu)多核系統(tǒng)的資源管理目標(biāo)。

1）資源數(shù)量約束：任何時刻系統(tǒng)運(yùn)行所分配的處理核的數(shù)量和種類不能多于硬件平臺相應(yīng)總數(shù)。

2）節(jié)能約束：當(dāng)簇內(nèi)的處理核上沒有線程運(yùn)行時，將簇的狀態(tài)設(shè)置為睡眠狀態(tài)。

3）功耗約束：系統(tǒng)運(yùn)行時的功耗受到平臺總功耗的限制。

4）電池電量狀態(tài)相關(guān)的運(yùn)行約束：為了延長系統(tǒng)運(yùn)行時間、延長系統(tǒng)使用壽命等，不同電量狀態(tài)對功耗值的限制額度不同。

5）功耗限制下的性能優(yōu)化：在系統(tǒng)當(dāng)前功耗限制情況下，最大化運(yùn)行應(yīng)用的性能或服務(wù)質(zhì)量。

3.2 離散控制器合成

針對資源管理問題，本節(jié)介紹如何基于自動機(jī)來對系統(tǒng)行為及其控制進(jìn)行建模，并在此基礎(chǔ)上對系統(tǒng)目標(biāo)進(jìn)行定義，從而將其描述為一個DCS問題。

3.2.1 硬件執(zhí)行平臺

系統(tǒng)硬件執(zhí)行平臺由一個大處理核簇（A0、A1）和一個小處理核簇（A2、A3）以及為平臺供電的電池構(gòu)成。每個簇可以在睡眠狀態(tài)以及不同的電壓/頻率工作狀態(tài)進(jìn)行切換，這些狀態(tài)之間的切換是可控的。假定大核簇除了睡眠狀態(tài)（表示為SleB）外，還有高頻、中頻和低頻三個工作模式（分別表示為HB、MB和LB），那么其行為可以采用圖5 中的狀態(tài)機(jī)來表示。而小核簇模型與大核類似，這里假定小處理核簇有睡眠、高頻和低頻（SleL、HL、LL）三個狀態(tài)。

從圖5 中可以看出，出于節(jié)能考慮，大處理核簇的初始狀態(tài)為SleB，表示沒有被任何應(yīng)用使用。當(dāng)簇中某個核被分配給應(yīng)用時，選用簇的何種DVFS 等級進(jìn)行工作則受可控變量c1、c2、c3控制，例如當(dāng)c1有效時那么簇就進(jìn)入DVFS 為高的工作狀態(tài)HB。輸出變量F_levelB（被定義到狀態(tài)中）用于表示該簇所處的工作狀態(tài)或DVFS 等級。另外，考慮到簇在不同狀態(tài)下的靜態(tài)功耗是不同的，同時定義輸出變量S_powerB來表示其當(dāng)前狀態(tài)的靜態(tài)功耗。小處理核簇的行為可以用類似的狀態(tài)機(jī)來相應(yīng)地建模表示。

圖5 大核簇行為模型Fig.5 Model for big cluster behaviors

假定系統(tǒng)電池的電量由高、中、低三個等級（狀態(tài)）構(gòu)成，并且系統(tǒng)配備了可以檢測電量等級變化并發(fā)出等級上升up和下降事件down的電量傳感器，那么其行為就可以用圖6 的狀態(tài)機(jī)Battery 模型來描述。初始時，電池電量滿額處于H 狀態(tài)，隨著等級上升up和下降down事件的變化電池當(dāng)前的電量級別也產(chǎn)生相應(yīng)變化，輸出變量B_level、power_limit用來表示當(dāng)前的電池狀態(tài)和功耗限制。

圖6 電池行為模型Fig.6 Model for battery behaviors

3.2.2 應(yīng)用行為及其資源分配

當(dāng)系統(tǒng)收到一個應(yīng)用的執(zhí)行請求時，由于其在使用不同資源組合時的性能和功耗表現(xiàn)往往不同，資源管理模塊就需要根據(jù)當(dāng)前的系統(tǒng)可用資源情況和系統(tǒng)目標(biāo)為其選擇適宜的資源分配方案。圖7 給出了具有兩種資源分配方案的應(yīng)用APPA的行為模型。初始時應(yīng)用處于空閑狀態(tài)IdleA，當(dāng)應(yīng)用被請求（也就是接受到req信號）時，應(yīng)用可能進(jìn)入狀態(tài)V1A或V2A，分別表示APPA的兩種執(zhí)行狀態(tài)（資源使用方案）。而如何選擇應(yīng)用的執(zhí)行狀態(tài)則是資源管理部件通過可控變量c來進(jìn)行控制的，這里模型進(jìn)行定義：1）輸出變量num_big和num_little來表示所使用的大核和小核的數(shù)量；2）性能perf和功率power變量表示該應(yīng)用在運(yùn)行時的性能參數(shù)和功耗值。此外，在應(yīng)用的執(zhí)行過程中，由于系統(tǒng)運(yùn)行環(huán)境的變化，比如電池電量變低，應(yīng)用還可能在兩種執(zhí)行狀態(tài)之間進(jìn)行切換從而滿足功耗等方面需求，其轉(zhuǎn)換同樣由資源管理部件通過可控變量c來進(jìn)行控制。當(dāng)收到表示應(yīng)用執(zhí)行結(jié)束的end信號時，應(yīng)用再次回到IdleA狀態(tài)。

圖7 應(yīng)用執(zhí)行行為模型Fig.7 Model for application execution behaviors

需要指出的是，獲取可行的資源方案及其性能指標(biāo)可以通過類似3.1.2 節(jié)中的探索方式得到，本文假定選取的均是滿足應(yīng)用最低性能要求的方案，并且這些方案及其性能和功率指標(biāo)均是通過將各個簇運(yùn)行在最低頻率值情況下模擬獲得的。

3.2.3 系統(tǒng)全局行為及控制目標(biāo)定義

由于系統(tǒng)資源分配的目標(biāo)（見3.1.3 節(jié)）往往是針對整個全局系統(tǒng)而言的，因此需首先構(gòu)建系統(tǒng)全局行為模型。通過把本部分描述的各個模型進(jìn)行并行組合就可以得到系統(tǒng)的全局行為模型S：

全局行為模型定義了系統(tǒng)所有可能的運(yùn)行狀態(tài)和行為，包括在外部事件發(fā)生時（例如某個應(yīng)用被啟動、電池電量變化）可能引起的運(yùn)行狀態(tài)和行為變化，其所有可能狀態(tài)可以表示為Qf：

其中，q(·)表示相關(guān)狀態(tài)機(jī)的任意狀態(tài)。

基于第2 章描述的DCS 技術(shù)，在以上系統(tǒng)模型基礎(chǔ)上定義控制目標(biāo)后便可以采用合成工具和算法來自動地合成一個正確的資源管理控制模塊。由于系統(tǒng)目標(biāo)涉及一些運(yùn)行時狀態(tài)的開銷，因而首先需要基于前面各個模塊模型上定義的局部開銷來定義整個系統(tǒng)模型的全局（總）開銷。給定一個系統(tǒng)全局狀態(tài)q，其由一系列的局部狀態(tài)(q1，q2，…，qn)組成，那么可以定義全局開銷如下（如果開銷變量未在局部模型上定義那么就為0）。

1）統(tǒng)計(jì)已分配的大（或者相應(yīng)?。┨幚砗藗€數(shù)：

2）系統(tǒng)性能，即系統(tǒng)正在執(zhí)行的所有應(yīng)用性能值的和：

3）系統(tǒng)功耗，即系統(tǒng)硬件平臺的靜態(tài)功耗（大核簇和小核簇靜態(tài)功耗的和）和所執(zhí)行應(yīng)用的動態(tài)功耗的和：

基于以上定義的系統(tǒng)自動機(jī)模型以及系統(tǒng)開銷，下面對3.1.3 節(jié)給出的系統(tǒng)資源分配目標(biāo)進(jìn)行定義。結(jié)合DCS 合成算法，這里區(qū)分了兩種類型合成目標(biāo)：邏輯控制和單步最優(yōu)控制。

1）邏輯控制。對于任意的系統(tǒng)狀態(tài)q，需滿足：

①資源約束。系統(tǒng)分配的大處理器核或小處理器核數(shù)目不能超出平臺相應(yīng)總的處理器數(shù)量：

其中numbig表示系統(tǒng)總的大核數(shù)量。

其中numlittle表示系統(tǒng)總的小核數(shù)量。

②節(jié)能約束。

a）當(dāng)簇內(nèi)的處理核上沒有線程運(yùn)行時，將簇的狀態(tài)設(shè)置為睡眠狀態(tài)：

b）當(dāng)簇內(nèi)的處理核上有線程運(yùn)行時，將簇的狀態(tài)設(shè)置為工作狀態(tài)：

③功耗約束。

其中，power_limit表示系統(tǒng)當(dāng)前的功耗約束。

④在電池電量狀態(tài)不同的情況下限制不同的平臺功耗：

2）單步最優(yōu)控制。在滿足邏輯控制目標(biāo)的系統(tǒng)狀態(tài)中選擇能使某個開銷最大或最小化的狀態(tài)。

⑤功率限制下的性能優(yōu)化。

其中：q'表示q可能達(dá)到的下一個狀態(tài)；max(perf(q'))表示從可能狀態(tài)中選擇性能值最大的那個狀態(tài)。

3.3 BZR代碼描述和離散控制器合成

給定3.2 節(jié)定義的系統(tǒng)行為模型和系統(tǒng)目標(biāo)后，就可以直接使用DCS 工具和語言BZR（http：//bzr.inria.fr）中的語法和語義來分別對它們進(jìn)行代碼描述。BZR是一種同步數(shù)據(jù)流（synchronous data-flow）編程語言，屬于同步語言（synchronous language）［35］的一種，它使用node（節(jié)點(diǎn)）作為基本編程單元，并定義了contract（合同）結(jié)構(gòu)來描述控制目標(biāo)。

3.3.1 系統(tǒng)行為描述

代碼1 為對圖7 的自動機(jī)也就是應(yīng)用執(zhí)行行為進(jìn)行BZR代碼描述的例子。如第1）行所示，該APPa 模塊被聲明為一個節(jié)點(diǎn)（node），其輸入變量c、req、ed（bool 型）被定義到節(jié)點(diǎn)名APPa后面的括號中，關(guān)鍵字returns用于給出該模塊（或節(jié)點(diǎn)）的輸出（也就是power、perf等）。第3）～17）行使用關(guān)鍵字let和tel定義了節(jié)點(diǎn)的主體部分，let后的automaton關(guān)鍵字指明了該節(jié)點(diǎn)是一個自動機(jī)。在自動機(jī)中使用關(guān)鍵字state 描述其狀態(tài)，關(guān)鍵字do指明與該狀態(tài)相關(guān)聯(lián)的行為，unless-then則指示狀態(tài)的轉(zhuǎn)換條件和目標(biāo)狀態(tài)。

代碼1 APPA的自動機(jī)代碼描述。

以第4）～7）行描述的Idle狀態(tài)及其轉(zhuǎn)換行為為例，當(dāng)處于Idle 狀態(tài)時，其功耗power、使用的大核數(shù)目num_big等變量被賦值為0；一旦有請求信號req到達(dá)，那么取決于可控變量c的取值，自動機(jī)可以轉(zhuǎn)換到V1 或者V2 狀態(tài)。狀態(tài)V1 和V2 的描述類似，在此不再贅述。

3.3.2 控制目標(biāo)描述

代碼2為使用BZR中的contract結(jié)構(gòu)對3.2.3節(jié)中系統(tǒng)的資源約束控制目標(biāo)進(jìn)行代碼描述的例子。contract 結(jié)構(gòu)使用contract關(guān)鍵字進(jìn)行聲明（第1）行），與控制目標(biāo)相關(guān)而系統(tǒng)模型中未定義的變量需要通過緊隨其后的關(guān)鍵字var 給出。這里第2）行定義了與資源約束控制目標(biāo)相關(guān)、表示系統(tǒng)中已分配的大、小處理核數(shù)目的局部變量num_big和num_little。關(guān)鍵字let和tel之間的部分用于將這些局部變量與系統(tǒng)模型（也就是自動機(jī)模型）中定義的變量進(jìn)行關(guān)聯(lián)，比如這里的num_big就是系統(tǒng)當(dāng)前所執(zhí)行應(yīng)用A 和應(yīng)用B 所分配的大處理核數(shù)目（表示為num_bigA和num_bigB）之和，見代碼第4）行。第5）行的num_little定義類似。關(guān)鍵字enforce 用于聲明DCS 所要執(zhí)行的控制目標(biāo)，這里確保使用的大小核數(shù)均不超過2 個（即小于3 個），見代碼第7）行。第8）行的with 關(guān)鍵字給出DCS 為了確保系統(tǒng)能夠滿足enforce 聲明的控制目標(biāo)所能夠控制的控制變量列表。

對3.2節(jié)中所有系統(tǒng)行為模型和控制目標(biāo)進(jìn)行BZR 代碼描述后，使用BZR 工具進(jìn)行編譯就可以自動調(diào)用其所關(guān)聯(lián)ReaX 工具中的DCS 算法來自動生成一個滿足控制目標(biāo)的控制器，而且用戶還可根據(jù)需要選擇采用C 或者Java 作為所生成控制器的源代碼。

代碼2 contract結(jié)構(gòu)描述。

4 模擬驗(yàn)證和評估實(shí)驗(yàn)

本章首先使用BZR 工具對文中的展示系統(tǒng)和模型進(jìn)行模擬驗(yàn)證，然后對本文采用的DCS 方法進(jìn)行可拓展性（scalability）評估。

4.1 模擬驗(yàn)證

在DCS 工具BZR 自動生成一個滿足系統(tǒng)需求的控制器后，為了展示所合成的控制器的正確性，該工具還提供了將合成的控制器與原先系統(tǒng)進(jìn)行整合并對控制后的系統(tǒng)行為進(jìn)行模擬驗(yàn)證的部件。通過該部件，設(shè)計(jì)者可以通過交互的方式在任意時刻對外部不可控變量進(jìn)行隨機(jī)賦值，從而驗(yàn)證目標(biāo)系統(tǒng)行為是否進(jìn)行相應(yīng)變化從而滿足系統(tǒng)需求。

圖8 給出了其中一個模擬場景的模擬結(jié)果截圖，這里假設(shè)在電池電量處于高、中和低狀態(tài)時系統(tǒng)的功率約束分別為30、25 和15。圖中最左邊第1 列是系統(tǒng)的輸入變量r_A、r_B、e_A、e_B、up、down（分別表示：應(yīng)用A請求、應(yīng)用B請求、應(yīng)用A結(jié)束、應(yīng)用B結(jié)束、電池狀態(tài)提高、電池狀態(tài)降低）和輸出變量num_bigA、num_littleA、num_bigB、num_littleB、f_levelb、f_levell、b_lv、power_limit、power_sum、perf_sum（分別表示：A 分配大核數(shù)、A 分配小核數(shù)、B 分配大核數(shù)、B 分配小核數(shù)、大核簇DVFS 等級、小核簇DVFS 等級、電池電量等級、系統(tǒng)功耗限制、系統(tǒng)功耗、系統(tǒng)總體性能）。從第2 列開始分別代表當(dāng)前時刻系統(tǒng)的輸入和輸出值。

可以看到，初始時刻（第2列）變量num_bigA、num_littleA、num_bigB、num_littleB均為0，表示系統(tǒng)的處理核都沒有被使用，系統(tǒng)還沒有應(yīng)用啟動。因此此時大核簇和小核簇均被設(shè)置為睡眠狀態(tài)，即f_levelb、f_levell均為0，滿足3.2.3節(jié)定義的目標(biāo)2；另外，電池狀態(tài)初始是滿額，處于高狀態(tài)，即b_lv是3，此時power_limit限額是30。

在下一時刻（第3 列），r_A、r_B均為1，表示應(yīng)用A 和應(yīng)用B 同時請求執(zhí)行，控制器的b_lv為3（電池高電量），相應(yīng)的平臺功耗限制power_limit此時為30?？梢钥吹剑藭r控制部件為應(yīng)用的資源分配情況（如標(biāo)簽1 所示）：應(yīng)用A 使用一個小核，應(yīng)用B使用一個大核和一個小核，系統(tǒng)分配的大核和小核總數(shù)沒有超出總的可用數(shù)量，滿足3.2.3 節(jié)定義的資源限制（目標(biāo)1）。另外，此時平臺功耗為27，滿足功耗限制（目標(biāo)3和4），而且此時系統(tǒng)性能perf_sum和滿足功耗約束的大小核簇的DVFS等級也均為最高，滿足目標(biāo)5。

圖8 模擬驗(yàn)證Fig.8 Simulation and verification

接下來的第4 列的時刻，系統(tǒng)收到表示電池電量下降的事件down有效（即為1），從而導(dǎo)致電池的電量等級b_lv降低到2，此時相應(yīng)的功耗限制power_limit變?yōu)?5。此時，控制器通過優(yōu)先降低兩個處理核簇的DVFS 等級f_levelb和f_levell到1從而滿足系統(tǒng)功耗限制25（目標(biāo)3和4）。

在第5 列表示的時刻，電量進(jìn)一步降低（down為1，b_lv降到1），此時的功耗限制power_limit為15，而目前兩個簇的DVFS等級已經(jīng)降到最低，此時控制器通過對兩個應(yīng)用所用資源資源進(jìn)行了重分配（如標(biāo)簽5中所示），將應(yīng)用B第4列所在時刻使用的一個大核和一個小核調(diào)整為僅使用1 個小核來滿足功率限制。值得指出的是這個時候小核簇的DVFS 被提高為2，其原因在于控制部件在當(dāng)前功耗額度下可以進(jìn)一步提高小核簇的功率來達(dá)到系統(tǒng)當(dāng)前約束下性能的最優(yōu)（目標(biāo)5）。

在最后兩列對應(yīng)的兩個時刻，隨著電量增加信號up變量的值為1，電池的電量水平b_lv也依次提升到2和3，同時系統(tǒng)的功率限制也相應(yīng)提高，最終又達(dá)到了第3 列時刻對應(yīng)的性能最佳分配方案。

圖9 不同狀態(tài)下系統(tǒng)性能和功率變化情況Fig.9 Change of system performance and power under different states

圖9 更直觀地展示了所設(shè)計(jì)生成的控制器部件可以在保證系統(tǒng)滿足性能約束前提下達(dá)到最好的性能。從圖9 中可以看出，系統(tǒng)在不同時刻（狀態(tài)）下的功率值（power_sum）始終滿足功率約束（power_limit），并且各個狀態(tài)下系統(tǒng)達(dá)到的性能值（perf_sum）均為最優(yōu)值（perf_max）。

4.2 可拓展性評估

跟其他形式化方法（比如模型檢測）一樣，離散控制器合成算法同樣是通過遍歷系統(tǒng)所有狀態(tài)空間來確保設(shè)計(jì)的正確性和可靠性，因而對于本文方法，另外一個需要考慮的問題就是所使用合成算法（工具）的可拓展性（scalability）。在本文所提出的模型的基礎(chǔ)上，通過不斷增加多核平臺核數(shù)和允許并行執(zhí)行的應(yīng)用數(shù)來對其可拓展性進(jìn)行評估。特別的，由于所使用的BZR 和ReaX 工具支持同時定義多個目標(biāo)并進(jìn)行整體控制器綜合，因而本文所做的評估實(shí)驗(yàn)是將邏輯和優(yōu)化目標(biāo)綜合算法的時間開銷同時考慮在內(nèi)的。

所有實(shí)驗(yàn)是在一臺配備了Intel Core I5 6500 CPU 和16 GB 內(nèi)存的PC 上進(jìn)行的，表1 中給出了針對不同系統(tǒng)規(guī)模進(jìn)行控制器合成所統(tǒng)計(jì)的合成時間。從表1 中可以看出，當(dāng)處理核的數(shù)目和任務(wù)數(shù)目都為8 時，系統(tǒng)狀態(tài)空間達(dá)到了2.8×106，此時合成時間需要7 200 s以上。為了處理具有更多處理核和應(yīng)用數(shù)的系統(tǒng)、提高本文方法的可擴(kuò)展性，用戶除了可以使用性能更加強(qiáng)大的計(jì)算機(jī)、花費(fèi)更多時間外，還可以提高合成算法的效率或者使用模塊化合成技術(shù)［31］。

表1 不同系統(tǒng)規(guī)模的合成時間Tab.1 Synthesis time for different system sizes

5 結(jié)語

針對異構(gòu)多核系統(tǒng)的資源管理問題，本文提出了一個將該問題形式化描述為一個離散控制問題的通用模型，并在此基礎(chǔ)上采用離散控制器合成技術(shù)自動生成一個滿足系統(tǒng)需求的資源管理部件，并為其提供了可靠性保證。此外，本文還通過使用現(xiàn)有的離散控制器綜合（DCS）工具和算法對文中的示例系統(tǒng)進(jìn)行了設(shè)計(jì)和模擬驗(yàn)證。最后，針對DCS 技術(shù)所面臨的系統(tǒng)狀態(tài)空間遍歷問題，通過對不同規(guī)模的系統(tǒng)進(jìn)行控制部件綜合實(shí)驗(yàn)對其可擴(kuò)展性進(jìn)行了評估。

相較于其他形式化的方法，本文提供了一種形式化的、自動構(gòu)建式的解決方案來對異構(gòu)多核系統(tǒng)的資源管理模塊進(jìn)行可靠設(shè)計(jì)。然而，目前我們的工作還缺乏實(shí)際系統(tǒng)和環(huán)境的部署和驗(yàn)證，下一步希望一方面將本文方法在一個實(shí)際的硬件平臺中進(jìn)行實(shí)現(xiàn)和驗(yàn)證，另一方面采用模塊化合成技術(shù)［31］來進(jìn)一步提升本文方法的可擴(kuò)展性。